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

Theorem bcmono 25859
 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 1189 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ∈ (ℤ𝐴))
2 simpl1 1188 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝑁 ∈ ℕ0)
3 eluzel2 12243 . . . . . 6 (𝐵 ∈ (ℤ𝐴) → 𝐴 ∈ ℤ)
433ad2ant2 1131 . . . . 5 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℤ)
54anim1i 617 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
6 elnn0z 11989 . . . 4 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
75, 6sylibr 237 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℕ0)
8 simpl3 1190 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ≤ (𝑁 / 2))
9 breq1 5056 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐴 ≤ (𝑁 / 2)))
10 oveq2 7154 . . . . . . . 8 (𝑥 = 𝐴 → (𝑁C𝑥) = (𝑁C𝐴))
1110breq2d 5065 . . . . . . 7 (𝑥 = 𝐴 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐴)))
129, 11imbi12d 348 . . . . . 6 (𝑥 = 𝐴 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
1312imbi2d 344 . . . . 5 (𝑥 = 𝐴 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))))
14 breq1 5056 . . . . . . 7 (𝑥 = 𝑘 → (𝑥 ≤ (𝑁 / 2) ↔ 𝑘 ≤ (𝑁 / 2)))
15 oveq2 7154 . . . . . . . 8 (𝑥 = 𝑘 → (𝑁C𝑥) = (𝑁C𝑘))
1615breq2d 5065 . . . . . . 7 (𝑥 = 𝑘 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝑘)))
1714, 16imbi12d 348 . . . . . 6 (𝑥 = 𝑘 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))
1817imbi2d 344 . . . . 5 (𝑥 = 𝑘 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)))))
19 breq1 5056 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑥 ≤ (𝑁 / 2) ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
20 oveq2 7154 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (𝑁C𝑥) = (𝑁C(𝑘 + 1)))
2120breq2d 5065 . . . . . . 7 (𝑥 = (𝑘 + 1) → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
2219, 21imbi12d 348 . . . . . 6 (𝑥 = (𝑘 + 1) → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
2322imbi2d 344 . . . . 5 (𝑥 = (𝑘 + 1) → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
24 breq1 5056 . . . . . . 7 (𝑥 = 𝐵 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐵 ≤ (𝑁 / 2)))
25 oveq2 7154 . . . . . . . 8 (𝑥 = 𝐵 → (𝑁C𝑥) = (𝑁C𝐵))
2625breq2d 5065 . . . . . . 7 (𝑥 = 𝐵 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐵)))
2724, 26imbi12d 348 . . . . . 6 (𝑥 = 𝐵 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))
2827imbi2d 344 . . . . 5 (𝑥 = 𝐵 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵)))))
29 bccl 13685 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ∈ ℕ0)
3029nn0red 11951 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ∈ ℝ)
3130leidd 11200 . . . . . . . 8 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ≤ (𝑁C𝐴))
3231a1d 25 . . . . . . 7 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))
3332expcom 417 . . . . . 6 (𝐴 ∈ ℤ → (𝑁 ∈ ℕ0 → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
3433adantrd 495 . . . . 5 (𝐴 ∈ ℤ → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
35 eluzelz 12248 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ𝐴) → 𝑘 ∈ ℤ)
36353ad2ant1 1130 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ∈ ℤ)
3736zred 12082 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ∈ ℝ)
3837lep1d 11565 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ≤ (𝑘 + 1))
39 peano2re 10807 . . . . . . . . . . . 12 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
4037, 39syl 17 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ)
41 nn0re 11901 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
42413ad2ant2 1131 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑁 ∈ ℝ)
4342rehalfcld 11879 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁 / 2) ∈ ℝ)
44 letr 10728 . . . . . . . . . . 11 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑁 / 2) ∈ ℝ) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2)))
4537, 40, 43, 44syl3anc 1368 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2)))
4638, 45mpand 694 . . . . . . . . 9 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → 𝑘 ≤ (𝑁 / 2)))
4746imim1d 82 . . . . . . . 8 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))
48 eluznn0 12312 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴)) → 𝑘 ∈ ℕ0)
49413ad2ant2 1131 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℝ)
50 nn0re 11901 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
51503ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℝ)
52 nn0p1nn 11931 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
53523ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ)
5453nnnn0d 11950 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ0)
5554nn0red 11951 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℝ)
5653nncnd 11648 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℂ)
57562timesd 11875 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) = ((𝑘 + 1) + (𝑘 + 1)))
58 simp3 1135 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 / 2))
59 2re 11706 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℝ
60 2pos 11735 . . . . . . . . . . . . . . . . . . . . . 22 0 < 2
6159, 60pm3.2i 474 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℝ ∧ 0 < 2)
6261a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 ∈ ℝ ∧ 0 < 2))
63 lemuldiv2 11515 . . . . . . . . . . . . . . . . . . . 20 (((𝑘 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
6455, 49, 62, 63syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
6558, 64mpbird 260 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) ≤ 𝑁)
6657, 65eqbrtrrd 5077 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ≤ 𝑁)
6751lep1d 11565 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑘 + 1))
6849, 51, 55, 55, 66, 67lesub3d 11252 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁𝑘))
69 nnre 11639 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ∈ ℝ)
70 nngt0 11663 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ ℕ → 0 < (𝑘 + 1))
7169, 70jca 515 . . . . . . . . . . . . . . . . . 18 ((𝑘 + 1) ∈ ℕ → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)))
7253, 71syl 17 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)))
73 nn0z 12000 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
74733ad2ant2 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℤ)
75 nn0z 12000 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
76753ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℤ)
7774, 76zsubcld 12087 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℤ)
7849rehalfcld 11879 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ∈ ℝ)
7949, 59jctir 524 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 ∈ ℝ ∧ 2 ∈ ℝ))
80 nn0ge0 11917 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)
81803ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑁)
82 1le2 11841 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 2
8381, 82jctir 524 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (0 ≤ 𝑁 ∧ 1 ≤ 2))
84 lemulge12 11497 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (0 ≤ 𝑁 ∧ 1 ≤ 2)) → 𝑁 ≤ (2 · 𝑁))
8579, 83, 84syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ≤ (2 · 𝑁))
86 ledivmul 11510 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑁 / 2) ≤ 𝑁𝑁 ≤ (2 · 𝑁)))
8749, 49, 62, 86syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 / 2) ≤ 𝑁𝑁 ≤ (2 · 𝑁)))
8885, 87mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ≤ 𝑁)
8955, 78, 49, 58, 88letrd 10791 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ 𝑁)
90 1red 10636 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈ ℝ)
9151, 90, 49leaddsub2d 11236 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁𝑘)))
9289, 91mpbid 235 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ≤ (𝑁𝑘))
93 elnnz1 12003 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ ↔ ((𝑁𝑘) ∈ ℤ ∧ 1 ≤ (𝑁𝑘)))
9477, 92, 93sylanbrc 586 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℕ)
95 nnre 11639 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ → (𝑁𝑘) ∈ ℝ)
96 nngt0 11663 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ → 0 < (𝑁𝑘))
9795, 96jca 515 . . . . . . . . . . . . . . . . . 18 ((𝑁𝑘) ∈ ℕ → ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)))
9894, 97syl 17 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)))
99 faccl 13646 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
100993ad2ant2 1131 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℕ)
101 nnm1nn0 11933 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑘) ∈ ℕ → ((𝑁𝑘) − 1) ∈ ℕ0)
102 faccl 13646 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁𝑘) − 1) ∈ ℕ0 → (!‘((𝑁𝑘) − 1)) ∈ ℕ)
10394, 101, 1023syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁𝑘) − 1)) ∈ ℕ)
104 faccl 13646 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
1051043ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℕ)
106103, 105nnmulcld 11685 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ)
107 nnrp 12395 . . . . . . . . . . . . . . . . . . . 20 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℝ+)
108 nnrp 12395 . . . . . . . . . . . . . . . . . . . 20 (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+)
109 rpdivcl 12409 . . . . . . . . . . . . . . . . . . . 20 (((!‘𝑁) ∈ ℝ+ ∧ ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
110107, 108, 109syl2an 598 . . . . . . . . . . . . . . . . . . 19 (((!‘𝑁) ∈ ℕ ∧ ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
111100, 106, 110syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
112111rpregt0d 12432 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 < ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)))))
113 lediv2 11524 . . . . . . . . . . . . . . . . 17 ((((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)) ∧ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 < ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))))) → ((𝑘 + 1) ≤ (𝑁𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))))
11472, 98, 112, 113syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ (𝑁𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))))
11568, 114mpbid 235 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))
116 facnn2 13645 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑘) ∈ ℕ → (!‘(𝑁𝑘)) = ((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)))
11794, 116syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁𝑘)) = ((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)))
118117oveq1d 7161 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁𝑘)) · (!‘𝑘)) = (((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)) · (!‘𝑘)))
119103nncnd 11648 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁𝑘) − 1)) ∈ ℂ)
120105nncnd 11648 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℂ)
12177zcnd 12083 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℂ)
122119, 120, 121mul32d 10844 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘)) = (((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)) · (!‘𝑘)))
123118, 122eqtr4d 2862 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁𝑘)) · (!‘𝑘)) = (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘)))
124123oveq2d 7162 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘))))
125 nn0ge0 11917 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ0 → 0 ≤ 𝑘)
1261253ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑘)
12751, 55, 49, 67, 89letrd 10791 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘𝑁)
128 0zd 11988 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ∈ ℤ)
129 elfz 12898 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘𝑘𝑁)))
13076, 128, 74, 129syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘𝑘𝑁)))
131126, 127, 130mpbir2and 712 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ (0...𝑁))
132 bcval2 13668 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))))
133131, 132syl 17 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))))
134100nncnd 11648 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℂ)
135106nncnd 11648 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℂ)
136106nnne0d 11682 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ≠ 0)
13794nnne0d 11682 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ≠ 0)
138134, 135, 121, 136, 137divdiv1d 11441 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘))))
139124, 133, 1383eqtr4d 2869 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)))
140 nn0cn 11902 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
1411403ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℂ)
142 nn0cn 11902 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
1431423ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℂ)
144 1cnd 10630 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈ ℂ)
145141, 143, 144subsub4d 11022 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁𝑘) − 1) = (𝑁 − (𝑘 + 1)))
146145eqcomd 2830 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − (𝑘 + 1)) = ((𝑁𝑘) − 1))
147146fveq2d 6663 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − (𝑘 + 1))) = (!‘((𝑁𝑘) − 1)))
148 facp1 13641 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0 → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
1491483ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
150147, 149oveq12d 7164 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = ((!‘((𝑁𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1))))
151119, 120, 56mulassd 10658 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)) = ((!‘((𝑁𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1))))
152150, 151eqtr4d 2862 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)))
153152oveq2d 7162 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))))
15454nn0ge0d 11953 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ (𝑘 + 1))
15553nnzd 12081 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℤ)
156 elfz 12898 . . . . . . . . . . . . . . . . . . 19 (((𝑘 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
157155, 128, 74, 156syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
158154, 89, 157mpbir2and 712 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ (0...𝑁))
159 bcval2 13668 . . . . . . . . . . . . . . . . 17 ((𝑘 + 1) ∈ (0...𝑁) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))))
160158, 159syl 17 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))))
16153nnne0d 11682 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≠ 0)
162134, 135, 56, 136, 161divdiv1d 11441 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))))
163153, 160, 1623eqtr4d 2869 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))
164115, 139, 1633brtr4d 5085 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))
1651643exp 1116 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))))
16648, 165syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴)) → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))))
1671663impia 1114 . . . . . . . . . . 11 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))
1681673coml 1124 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))
169 simp2 1134 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑁 ∈ ℕ0)
170 nn0z 12000 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℕ0𝐴 ∈ ℤ)
1711703ad2ant3 1132 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝐴 ∈ ℤ)
172169, 171, 29syl2anc 587 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝐴) ∈ ℕ0)
173172nn0red 11951 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝐴) ∈ ℝ)
174 bccl 13685 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → (𝑁C𝑘) ∈ ℕ0)
175169, 36, 174syl2anc 587 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝑘) ∈ ℕ0)
176175nn0red 11951 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝑘) ∈ ℝ)
17736peano2zd 12085 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 + 1) ∈ ℤ)
178 bccl 13685 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑁C(𝑘 + 1)) ∈ ℕ0)
179169, 177, 178syl2anc 587 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C(𝑘 + 1)) ∈ ℕ0)
180179nn0red 11951 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C(𝑘 + 1)) ∈ ℝ)
181 letr 10728 . . . . . . . . . . . 12 (((𝑁C𝐴) ∈ ℝ ∧ (𝑁C𝑘) ∈ ℝ ∧ (𝑁C(𝑘 + 1)) ∈ ℝ) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
182173, 176, 180, 181syl3anc 1368 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
183182expcomd 420 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
184168, 183syld 47 . . . . . . . . 9 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
185184a2d 29 . . . . . . . 8 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
18647, 185syld 47 . . . . . . 7 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
1871863expib 1119 . . . . . 6 (𝑘 ∈ (ℤ𝐴) → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
188187a2d 29 . . . . 5 (𝑘 ∈ (ℤ𝐴) → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))) → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
18913, 18, 23, 28, 34, 188uzind4 12301 . . . 4 (𝐵 ∈ (ℤ𝐴) → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))
1901893imp 1108 . . 3 ((𝐵 ∈ (ℤ𝐴) ∧ (𝑁 ∈ ℕ0𝐴 ∈ ℕ0) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
1911, 2, 7, 8, 190syl121anc 1372 . 2 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝑁C𝐴) ≤ (𝑁C𝐵))
192 simpl1 1188 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝑁 ∈ ℕ0)
1934adantr 484 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐴 ∈ ℤ)
194 animorrl 978 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝐴 < 0 ∨ 𝑁 < 𝐴))
195 bcval4 13670 . . . 4 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ ∧ (𝐴 < 0 ∨ 𝑁 < 𝐴)) → (𝑁C𝐴) = 0)
196192, 193, 194, 195syl3anc 1368 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) = 0)
197 simpl2 1189 . . . . . 6 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ (ℤ𝐴))
198 eluzelz 12248 . . . . . 6 (𝐵 ∈ (ℤ𝐴) → 𝐵 ∈ ℤ)
199197, 198syl 17 . . . . 5 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ ℤ)
200 bccl 13685 . . . . 5 ((𝑁 ∈ ℕ0𝐵 ∈ ℤ) → (𝑁C𝐵) ∈ ℕ0)
201192, 199, 200syl2anc 587 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐵) ∈ ℕ0)
202201nn0ge0d 11953 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 0 ≤ (𝑁C𝐵))
203196, 202eqbrtrd 5075 . 2 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) ≤ (𝑁C𝐵))
204 0re 10637 . . 3 0 ∈ ℝ
2054zred 12082 . . 3 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℝ)
206 lelttric 10741 . . 3 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 ≤ 𝐴𝐴 < 0))
207204, 205, 206sylancr 590 . 2 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (0 ≤ 𝐴𝐴 < 0))
208191, 203, 207mpjaodan 956 1 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   class class class wbr 5053  ‘cfv 6344  (class class class)co 7146  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536   < clt 10669   ≤ cle 10670   − cmin 10864   / cdiv 11291  ℕcn 11632  2c2 11687  ℕ0cn0 11892  ℤcz 11976  ℤ≥cuz 12238  ℝ+crp 12384  ...cfz 12892  !cfa 13636  Ccbc 13665 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4826  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-riota 7104  df-ov 7149  df-oprab 7150  df-mpo 7151  df-om 7572  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11695  df-n0 11893  df-z 11977  df-uz 12239  df-rp 12385  df-fz 12893  df-seq 13372  df-fac 13637  df-bc 13666 This theorem is referenced by:  bcmax  25860
 Copyright terms: Public domain W3C validator