MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bcmono Structured version   Visualization version   GIF version

Theorem bcmono 25222
Description: The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
Assertion
Ref Expression
bcmono ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))

Proof of Theorem bcmono
Dummy variables 𝑥 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl2 1228 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ∈ (ℤ𝐴))
2 simpl1 1226 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝑁 ∈ ℕ0)
3 eluzel2 11892 . . . . . 6 (𝐵 ∈ (ℤ𝐴) → 𝐴 ∈ ℤ)
433ad2ant2 1127 . . . . 5 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℤ)
54anim1i 594 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
6 elnn0z 11591 . . . 4 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
75, 6sylibr 224 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℕ0)
8 simpl3 1230 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ≤ (𝑁 / 2))
9 breq1 4787 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐴 ≤ (𝑁 / 2)))
10 oveq2 6800 . . . . . . . 8 (𝑥 = 𝐴 → (𝑁C𝑥) = (𝑁C𝐴))
1110breq2d 4796 . . . . . . 7 (𝑥 = 𝐴 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐴)))
129, 11imbi12d 333 . . . . . 6 (𝑥 = 𝐴 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
1312imbi2d 329 . . . . 5 (𝑥 = 𝐴 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))))
14 breq1 4787 . . . . . . 7 (𝑥 = 𝑘 → (𝑥 ≤ (𝑁 / 2) ↔ 𝑘 ≤ (𝑁 / 2)))
15 oveq2 6800 . . . . . . . 8 (𝑥 = 𝑘 → (𝑁C𝑥) = (𝑁C𝑘))
1615breq2d 4796 . . . . . . 7 (𝑥 = 𝑘 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝑘)))
1714, 16imbi12d 333 . . . . . 6 (𝑥 = 𝑘 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))
1817imbi2d 329 . . . . 5 (𝑥 = 𝑘 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)))))
19 breq1 4787 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑥 ≤ (𝑁 / 2) ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
20 oveq2 6800 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (𝑁C𝑥) = (𝑁C(𝑘 + 1)))
2120breq2d 4796 . . . . . . 7 (𝑥 = (𝑘 + 1) → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
2219, 21imbi12d 333 . . . . . 6 (𝑥 = (𝑘 + 1) → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
2322imbi2d 329 . . . . 5 (𝑥 = (𝑘 + 1) → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
24 breq1 4787 . . . . . . 7 (𝑥 = 𝐵 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐵 ≤ (𝑁 / 2)))
25 oveq2 6800 . . . . . . . 8 (𝑥 = 𝐵 → (𝑁C𝑥) = (𝑁C𝐵))
2625breq2d 4796 . . . . . . 7 (𝑥 = 𝐵 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐵)))
2724, 26imbi12d 333 . . . . . 6 (𝑥 = 𝐵 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))
2827imbi2d 329 . . . . 5 (𝑥 = 𝐵 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵)))))
29 bccl 13312 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ∈ ℕ0)
3029nn0red 11553 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ∈ ℝ)
3130leidd 10795 . . . . . . . 8 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ≤ (𝑁C𝐴))
3231a1d 25 . . . . . . 7 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))
3332expcom 398 . . . . . 6 (𝐴 ∈ ℤ → (𝑁 ∈ ℕ0 → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
3433adantrd 475 . . . . 5 (𝐴 ∈ ℤ → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
35 eluzelz 11897 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ𝐴) → 𝑘 ∈ ℤ)
36353ad2ant1 1126 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ∈ ℤ)
3736zred 11683 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ∈ ℝ)
3837lep1d 11156 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ≤ (𝑘 + 1))
39 peano2re 10410 . . . . . . . . . . . 12 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
4037, 39syl 17 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ)
41 nn0re 11502 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
42413ad2ant2 1127 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑁 ∈ ℝ)
4342rehalfcld 11480 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁 / 2) ∈ ℝ)
44 letr 10332 . . . . . . . . . . 11 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑁 / 2) ∈ ℝ) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2)))
4537, 40, 43, 44syl3anc 1475 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2)))
4638, 45mpand 667 . . . . . . . . 9 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → 𝑘 ≤ (𝑁 / 2)))
4746imim1d 82 . . . . . . . 8 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))
48 eluznn0 11959 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴)) → 𝑘 ∈ ℕ0)
49 nn0re 11502 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
50493ad2ant1 1126 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℝ)
51 nn0p1nn 11533 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
52513ad2ant1 1126 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ)
5352nnnn0d 11552 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ0)
5453nn0red 11553 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℝ)
5550, 54readdcld 10270 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ∈ ℝ)
5654, 54readdcld 10270 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ∈ ℝ)
57413ad2ant2 1127 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℝ)
5850lep1d 11156 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑘 + 1))
5950, 54, 54, 58leadd1dd 10842 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ≤ ((𝑘 + 1) + (𝑘 + 1)))
6052nncnd 11237 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℂ)
61602timesd 11476 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) = ((𝑘 + 1) + (𝑘 + 1)))
62 simp3 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 / 2))
63 2re 11291 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
64 2pos 11313 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
6563, 64pm3.2i 447 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
6665a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 ∈ ℝ ∧ 0 < 2))
67 lemuldiv2 11105 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
6854, 57, 66, 67syl3anc 1475 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
6962, 68mpbird 247 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) ≤ 𝑁)
7061, 69eqbrtrrd 4808 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ≤ 𝑁)
7155, 56, 57, 59, 70letrd 10395 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ≤ 𝑁)
7250, 54, 57leaddsub2d 10830 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁𝑘)))
7371, 72mpbid 222 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁𝑘))
74 nnre 11228 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ∈ ℝ)
75 nngt0 11250 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ ℕ → 0 < (𝑘 + 1))
7674, 75jca 495 . . . . . . . . . . . . . . . . . 18 ((𝑘 + 1) ∈ ℕ → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)))
7752, 76syl 17 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)))
78 nn0z 11601 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
79783ad2ant2 1127 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℤ)
80 nn0z 11601 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
81803ad2ant1 1126 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℤ)
8279, 81zsubcld 11688 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℤ)
8357rehalfcld 11480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ∈ ℝ)
8457, 63jctir 504 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 ∈ ℝ ∧ 2 ∈ ℝ))
85 nn0ge0 11519 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)
86853ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑁)
87 1le2 11442 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 2
8886, 87jctir 504 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (0 ≤ 𝑁 ∧ 1 ≤ 2))
89 lemulge12 11087 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (0 ≤ 𝑁 ∧ 1 ≤ 2)) → 𝑁 ≤ (2 · 𝑁))
9084, 88, 89syl2anc 565 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ≤ (2 · 𝑁))
91 ledivmul 11100 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑁 / 2) ≤ 𝑁𝑁 ≤ (2 · 𝑁)))
9257, 57, 66, 91syl3anc 1475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 / 2) ≤ 𝑁𝑁 ≤ (2 · 𝑁)))
9390, 92mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ≤ 𝑁)
9454, 83, 57, 62, 93letrd 10395 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ 𝑁)
95 1red 10256 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈ ℝ)
9650, 95, 57leaddsub2d 10830 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁𝑘)))
9794, 96mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ≤ (𝑁𝑘))
98 elnnz1 11604 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ ↔ ((𝑁𝑘) ∈ ℤ ∧ 1 ≤ (𝑁𝑘)))
9982, 97, 98sylanbrc 564 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℕ)
100 nnre 11228 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ → (𝑁𝑘) ∈ ℝ)
101 nngt0 11250 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ → 0 < (𝑁𝑘))
102100, 101jca 495 . . . . . . . . . . . . . . . . . 18 ((𝑁𝑘) ∈ ℕ → ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)))
10399, 102syl 17 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)))
104 faccl 13273 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
1051043ad2ant2 1127 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℕ)
106 nnm1nn0 11535 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑘) ∈ ℕ → ((𝑁𝑘) − 1) ∈ ℕ0)
107 faccl 13273 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁𝑘) − 1) ∈ ℕ0 → (!‘((𝑁𝑘) − 1)) ∈ ℕ)
10899, 106, 1073syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁𝑘) − 1)) ∈ ℕ)
109 faccl 13273 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
1101093ad2ant1 1126 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℕ)
111108, 110nnmulcld 11269 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ)
112 nnrp 12044 . . . . . . . . . . . . . . . . . . . 20 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℝ+)
113 nnrp 12044 . . . . . . . . . . . . . . . . . . . 20 (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+)
114 rpdivcl 12058 . . . . . . . . . . . . . . . . . . . 20 (((!‘𝑁) ∈ ℝ+ ∧ ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
115112, 113, 114syl2an 575 . . . . . . . . . . . . . . . . . . 19 (((!‘𝑁) ∈ ℕ ∧ ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
116105, 111, 115syl2anc 565 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
117116rpregt0d 12080 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 < ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)))))
118 lediv2 11114 . . . . . . . . . . . . . . . . 17 ((((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)) ∧ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 < ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))))) → ((𝑘 + 1) ≤ (𝑁𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))))
11977, 103, 117, 118syl3anc 1475 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ (𝑁𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))))
12073, 119mpbid 222 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))
121 facnn2 13272 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑘) ∈ ℕ → (!‘(𝑁𝑘)) = ((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)))
12299, 121syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁𝑘)) = ((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)))
123122oveq1d 6807 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁𝑘)) · (!‘𝑘)) = (((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)) · (!‘𝑘)))
124108nncnd 11237 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁𝑘) − 1)) ∈ ℂ)
125110nncnd 11237 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℂ)
12682zcnd 11684 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℂ)
127124, 125, 126mul32d 10447 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘)) = (((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)) · (!‘𝑘)))
128123, 127eqtr4d 2807 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁𝑘)) · (!‘𝑘)) = (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘)))
129128oveq2d 6808 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘))))
130 nn0ge0 11519 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ0 → 0 ≤ 𝑘)
1311303ad2ant1 1126 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑘)
13250, 54, 57, 58, 94letrd 10395 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘𝑁)
133 0zd 11590 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ∈ ℤ)
134 elfz 12538 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘𝑘𝑁)))
13581, 133, 79, 134syl3anc 1475 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘𝑘𝑁)))
136131, 132, 135mpbir2and 684 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ (0...𝑁))
137 bcval2 13295 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))))
138136, 137syl 17 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))))
139105nncnd 11237 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℂ)
140111nncnd 11237 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℂ)
141111nnne0d 11266 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ≠ 0)
14299nnne0d 11266 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ≠ 0)
143139, 140, 126, 141, 142divdiv1d 11033 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘))))
144129, 138, 1433eqtr4d 2814 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)))
145 nn0cn 11503 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
1461453ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℂ)
147 nn0cn 11503 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
1481473ad2ant1 1126 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℂ)
149 1cnd 10257 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈ ℂ)
150146, 148, 149subsub4d 10624 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁𝑘) − 1) = (𝑁 − (𝑘 + 1)))
151150eqcomd 2776 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − (𝑘 + 1)) = ((𝑁𝑘) − 1))
152151fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − (𝑘 + 1))) = (!‘((𝑁𝑘) − 1)))
153 facp1 13268 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0 → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
1541533ad2ant1 1126 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
155152, 154oveq12d 6810 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = ((!‘((𝑁𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1))))
156124, 125, 60mulassd 10264 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)) = ((!‘((𝑁𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1))))
157155, 156eqtr4d 2807 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)))
158157oveq2d 6808 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))))
15953nn0ge0d 11555 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ (𝑘 + 1))
16052nnzd 11682 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℤ)
161 elfz 12538 . . . . . . . . . . . . . . . . . . 19 (((𝑘 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
162160, 133, 79, 161syl3anc 1475 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
163159, 94, 162mpbir2and 684 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ (0...𝑁))
164 bcval2 13295 . . . . . . . . . . . . . . . . 17 ((𝑘 + 1) ∈ (0...𝑁) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))))
165163, 164syl 17 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))))
16652nnne0d 11266 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≠ 0)
167139, 140, 60, 141, 166divdiv1d 11033 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))))
168158, 165, 1673eqtr4d 2814 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))
169120, 144, 1683brtr4d 4816 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))
1701693exp 1111 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))))
17148, 170syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴)) → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))))
1721713impia 1108 . . . . . . . . . . 11 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))
1731723coml 1120 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))
174 simp2 1130 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑁 ∈ ℕ0)
175 nn0z 11601 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℕ0𝐴 ∈ ℤ)
1761753ad2ant3 1128 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝐴 ∈ ℤ)
177174, 176, 29syl2anc 565 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝐴) ∈ ℕ0)
178177nn0red 11553 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝐴) ∈ ℝ)
179 bccl 13312 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → (𝑁C𝑘) ∈ ℕ0)
180174, 36, 179syl2anc 565 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝑘) ∈ ℕ0)
181180nn0red 11553 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝑘) ∈ ℝ)
18236peano2zd 11686 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 + 1) ∈ ℤ)
183 bccl 13312 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑁C(𝑘 + 1)) ∈ ℕ0)
184174, 182, 183syl2anc 565 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C(𝑘 + 1)) ∈ ℕ0)
185184nn0red 11553 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C(𝑘 + 1)) ∈ ℝ)
186 letr 10332 . . . . . . . . . . . 12 (((𝑁C𝐴) ∈ ℝ ∧ (𝑁C𝑘) ∈ ℝ ∧ (𝑁C(𝑘 + 1)) ∈ ℝ) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
187178, 181, 185, 186syl3anc 1475 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
188187expcomd 402 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
189173, 188syld 47 . . . . . . . . 9 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
190189a2d 29 . . . . . . . 8 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
19147, 190syld 47 . . . . . . 7 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
1921913expib 1115 . . . . . 6 (𝑘 ∈ (ℤ𝐴) → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
193192a2d 29 . . . . 5 (𝑘 ∈ (ℤ𝐴) → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))) → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
19413, 18, 23, 28, 34, 193uzind4 11947 . . . 4 (𝐵 ∈ (ℤ𝐴) → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))
1951943imp 1100 . . 3 ((𝐵 ∈ (ℤ𝐴) ∧ (𝑁 ∈ ℕ0𝐴 ∈ ℕ0) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
1961, 2, 7, 8, 195syl121anc 1480 . 2 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝑁C𝐴) ≤ (𝑁C𝐵))
197 simpl1 1226 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝑁 ∈ ℕ0)
1984adantr 466 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐴 ∈ ℤ)
199 orc 847 . . . . 5 (𝐴 < 0 → (𝐴 < 0 ∨ 𝑁 < 𝐴))
200199adantl 467 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝐴 < 0 ∨ 𝑁 < 𝐴))
201 bcval4 13297 . . . 4 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ ∧ (𝐴 < 0 ∨ 𝑁 < 𝐴)) → (𝑁C𝐴) = 0)
202197, 198, 200, 201syl3anc 1475 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) = 0)
203 simpl2 1228 . . . . . 6 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ (ℤ𝐴))
204 eluzelz 11897 . . . . . 6 (𝐵 ∈ (ℤ𝐴) → 𝐵 ∈ ℤ)
205203, 204syl 17 . . . . 5 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ ℤ)
206 bccl 13312 . . . . 5 ((𝑁 ∈ ℕ0𝐵 ∈ ℤ) → (𝑁C𝐵) ∈ ℕ0)
207197, 205, 206syl2anc 565 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐵) ∈ ℕ0)
208207nn0ge0d 11555 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 0 ≤ (𝑁C𝐵))
209202, 208eqbrtrd 4806 . 2 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) ≤ (𝑁C𝐵))
210 0re 10241 . . 3 0 ∈ ℝ
2114zred 11683 . . 3 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℝ)
212 lelttric 10345 . . 3 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 ≤ 𝐴𝐴 < 0))
213210, 211, 212sylancr 567 . 2 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (0 ≤ 𝐴𝐴 < 0))
214196, 209, 213mpjaodan 939 1 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wo 826  w3a 1070   = wceq 1630  wcel 2144   class class class wbr 4784  cfv 6031  (class class class)co 6792  cc 10135  cr 10136  0cc0 10137  1c1 10138   + caddc 10140   · cmul 10142   < clt 10275  cle 10276  cmin 10467   / cdiv 10885  cn 11221  2c2 11271  0cn0 11493  cz 11578  cuz 11887  +crp 12034  ...cfz 12532  !cfa 13263  Ccbc 13292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-er 7895  df-en 8109  df-dom 8110  df-sdom 8111  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-div 10886  df-nn 11222  df-2 11280  df-n0 11494  df-z 11579  df-uz 11888  df-rp 12035  df-fz 12533  df-seq 13008  df-fac 13264  df-bc 13293
This theorem is referenced by:  bcmax  25223
  Copyright terms: Public domain W3C validator