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

Theorem bcmono 24983
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 1063 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ∈ (ℤ𝐴))
2 simpl1 1062 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝑁 ∈ ℕ0)
3 eluzel2 11677 . . . . . 6 (𝐵 ∈ (ℤ𝐴) → 𝐴 ∈ ℤ)
433ad2ant2 1081 . . . . 5 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℤ)
54anim1i 591 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
6 elnn0z 11375 . . . 4 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
75, 6sylibr 224 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℕ0)
8 simpl3 1064 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ≤ (𝑁 / 2))
9 breq1 4647 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐴 ≤ (𝑁 / 2)))
10 oveq2 6643 . . . . . . . 8 (𝑥 = 𝐴 → (𝑁C𝑥) = (𝑁C𝐴))
1110breq2d 4656 . . . . . . 7 (𝑥 = 𝐴 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐴)))
129, 11imbi12d 334 . . . . . 6 (𝑥 = 𝐴 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
1312imbi2d 330 . . . . 5 (𝑥 = 𝐴 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))))
14 breq1 4647 . . . . . . 7 (𝑥 = 𝑘 → (𝑥 ≤ (𝑁 / 2) ↔ 𝑘 ≤ (𝑁 / 2)))
15 oveq2 6643 . . . . . . . 8 (𝑥 = 𝑘 → (𝑁C𝑥) = (𝑁C𝑘))
1615breq2d 4656 . . . . . . 7 (𝑥 = 𝑘 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝑘)))
1714, 16imbi12d 334 . . . . . 6 (𝑥 = 𝑘 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))
1817imbi2d 330 . . . . 5 (𝑥 = 𝑘 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)))))
19 breq1 4647 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑥 ≤ (𝑁 / 2) ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
20 oveq2 6643 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (𝑁C𝑥) = (𝑁C(𝑘 + 1)))
2120breq2d 4656 . . . . . . 7 (𝑥 = (𝑘 + 1) → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
2219, 21imbi12d 334 . . . . . 6 (𝑥 = (𝑘 + 1) → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
2322imbi2d 330 . . . . 5 (𝑥 = (𝑘 + 1) → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
24 breq1 4647 . . . . . . 7 (𝑥 = 𝐵 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐵 ≤ (𝑁 / 2)))
25 oveq2 6643 . . . . . . . 8 (𝑥 = 𝐵 → (𝑁C𝑥) = (𝑁C𝐵))
2625breq2d 4656 . . . . . . 7 (𝑥 = 𝐵 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐵)))
2724, 26imbi12d 334 . . . . . 6 (𝑥 = 𝐵 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))
2827imbi2d 330 . . . . 5 (𝑥 = 𝐵 → (((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵)))))
29 bccl 13092 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ∈ ℕ0)
3029nn0red 11337 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ∈ ℝ)
3130leidd 10579 . . . . . . . 8 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝑁C𝐴) ≤ (𝑁C𝐴))
3231a1d 25 . . . . . . 7 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))
3332expcom 451 . . . . . 6 (𝐴 ∈ ℤ → (𝑁 ∈ ℕ0 → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
3433adantrd 484 . . . . 5 (𝐴 ∈ ℤ → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
35 eluzelz 11682 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ𝐴) → 𝑘 ∈ ℤ)
36353ad2ant1 1080 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ∈ ℤ)
3736zred 11467 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ∈ ℝ)
3837lep1d 10940 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑘 ≤ (𝑘 + 1))
39 peano2re 10194 . . . . . . . . . . . 12 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
4037, 39syl 17 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ)
41 nn0re 11286 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
42413ad2ant2 1081 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑁 ∈ ℝ)
4342rehalfcld 11264 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁 / 2) ∈ ℝ)
44 letr 10116 . . . . . . . . . . 11 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑁 / 2) ∈ ℝ) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2)))
4537, 40, 43, 44syl3anc 1324 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2)))
4638, 45mpand 710 . . . . . . . . 9 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → 𝑘 ≤ (𝑁 / 2)))
4746imim1d 82 . . . . . . . 8 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))
48 eluznn0 11742 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴)) → 𝑘 ∈ ℕ0)
49 nn0re 11286 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
50493ad2ant1 1080 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℝ)
51 nn0p1nn 11317 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
52513ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ)
5352nnnn0d 11336 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ0)
5453nn0red 11337 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℝ)
5550, 54readdcld 10054 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ∈ ℝ)
5654, 54readdcld 10054 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ∈ ℝ)
57413ad2ant2 1081 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℝ)
5850lep1d 10940 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑘 + 1))
5950, 54, 54, 58leadd1dd 10626 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ≤ ((𝑘 + 1) + (𝑘 + 1)))
6052nncnd 11021 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℂ)
61602timesd 11260 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) = ((𝑘 + 1) + (𝑘 + 1)))
62 simp3 1061 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 / 2))
63 2re 11075 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
64 2pos 11097 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
6563, 64pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
6665a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 ∈ ℝ ∧ 0 < 2))
67 lemuldiv2 10889 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
6854, 57, 66, 67syl3anc 1324 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
6962, 68mpbird 247 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) ≤ 𝑁)
7061, 69eqbrtrrd 4668 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ≤ 𝑁)
7155, 56, 57, 59, 70letrd 10179 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ≤ 𝑁)
7250, 54, 57leaddsub2d 10614 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁𝑘)))
7371, 72mpbid 222 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁𝑘))
74 nnre 11012 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ∈ ℝ)
75 nngt0 11034 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ ℕ → 0 < (𝑘 + 1))
7674, 75jca 554 . . . . . . . . . . . . . . . . . 18 ((𝑘 + 1) ∈ ℕ → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)))
7752, 76syl 17 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)))
78 nn0z 11385 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
79783ad2ant2 1081 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℤ)
80 nn0z 11385 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
81803ad2ant1 1080 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℤ)
8279, 81zsubcld 11472 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℤ)
8357rehalfcld 11264 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ∈ ℝ)
8457, 63jctir 560 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 ∈ ℝ ∧ 2 ∈ ℝ))
85 nn0ge0 11303 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)
86853ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑁)
87 1le2 11226 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 2
8886, 87jctir 560 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (0 ≤ 𝑁 ∧ 1 ≤ 2))
89 lemulge12 10871 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (0 ≤ 𝑁 ∧ 1 ≤ 2)) → 𝑁 ≤ (2 · 𝑁))
9084, 88, 89syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ≤ (2 · 𝑁))
91 ledivmul 10884 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑁 / 2) ≤ 𝑁𝑁 ≤ (2 · 𝑁)))
9257, 57, 66, 91syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 / 2) ≤ 𝑁𝑁 ≤ (2 · 𝑁)))
9390, 92mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ≤ 𝑁)
9454, 83, 57, 62, 93letrd 10179 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ 𝑁)
95 1red 10040 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈ ℝ)
9650, 95, 57leaddsub2d 10614 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁𝑘)))
9794, 96mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ≤ (𝑁𝑘))
98 elnnz1 11388 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ ↔ ((𝑁𝑘) ∈ ℤ ∧ 1 ≤ (𝑁𝑘)))
9982, 97, 98sylanbrc 697 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℕ)
100 nnre 11012 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ → (𝑁𝑘) ∈ ℝ)
101 nngt0 11034 . . . . . . . . . . . . . . . . . . 19 ((𝑁𝑘) ∈ ℕ → 0 < (𝑁𝑘))
102100, 101jca 554 . . . . . . . . . . . . . . . . . 18 ((𝑁𝑘) ∈ ℕ → ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)))
10399, 102syl 17 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)))
104 faccl 13053 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
1051043ad2ant2 1081 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℕ)
106 nnm1nn0 11319 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑘) ∈ ℕ → ((𝑁𝑘) − 1) ∈ ℕ0)
107 faccl 13053 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁𝑘) − 1) ∈ ℕ0 → (!‘((𝑁𝑘) − 1)) ∈ ℕ)
10899, 106, 1073syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁𝑘) − 1)) ∈ ℕ)
109 faccl 13053 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
1101093ad2ant1 1080 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℕ)
111108, 110nnmulcld 11053 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ)
112 nnrp 11827 . . . . . . . . . . . . . . . . . . . 20 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℝ+)
113 nnrp 11827 . . . . . . . . . . . . . . . . . . . 20 (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+)
114 rpdivcl 11841 . . . . . . . . . . . . . . . . . . . 20 (((!‘𝑁) ∈ ℝ+ ∧ ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
115112, 113, 114syl2an 494 . . . . . . . . . . . . . . . . . . 19 (((!‘𝑁) ∈ ℕ ∧ ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℕ) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
116105, 111, 115syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
117116rpregt0d 11863 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 < ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)))))
118 lediv2 10898 . . . . . . . . . . . . . . . . 17 ((((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ ((𝑁𝑘) ∈ ℝ ∧ 0 < (𝑁𝑘)) ∧ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 < ((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))))) → ((𝑘 + 1) ≤ (𝑁𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))))
11977, 103, 117, 118syl3anc 1324 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ (𝑁𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))))
12073, 119mpbid 222 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))
121 facnn2 13052 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑘) ∈ ℕ → (!‘(𝑁𝑘)) = ((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)))
12299, 121syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁𝑘)) = ((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)))
123122oveq1d 6650 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁𝑘)) · (!‘𝑘)) = (((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)) · (!‘𝑘)))
124108nncnd 11021 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁𝑘) − 1)) ∈ ℂ)
125110nncnd 11021 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℂ)
12682zcnd 11468 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ∈ ℂ)
127124, 125, 126mul32d 10231 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘)) = (((!‘((𝑁𝑘) − 1)) · (𝑁𝑘)) · (!‘𝑘)))
128123, 127eqtr4d 2657 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁𝑘)) · (!‘𝑘)) = (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘)))
129128oveq2d 6651 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘))))
130 nn0ge0 11303 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ0 → 0 ≤ 𝑘)
1311303ad2ant1 1080 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑘)
13250, 54, 57, 58, 94letrd 10179 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘𝑁)
133 0zd 11374 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ∈ ℤ)
134 elfz 12317 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘𝑘𝑁)))
13581, 133, 79, 134syl3anc 1324 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘𝑘𝑁)))
136131, 132, 135mpbir2and 956 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ (0...𝑁))
137 bcval2 13075 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))))
138136, 137syl 17 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁𝑘)) · (!‘𝑘))))
139105nncnd 11021 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℂ)
140111nncnd 11021 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ∈ ℂ)
141111nnne0d 11050 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) ≠ 0)
14299nnne0d 11050 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁𝑘) ≠ 0)
143139, 140, 126, 141, 142divdiv1d 10817 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑁𝑘))))
144129, 138, 1433eqtr4d 2664 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑁𝑘)))
145 nn0cn 11287 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
1461453ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℂ)
147 nn0cn 11287 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
1481473ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℂ)
149 1cnd 10041 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈ ℂ)
150146, 148, 149subsub4d 10408 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁𝑘) − 1) = (𝑁 − (𝑘 + 1)))
151150eqcomd 2626 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − (𝑘 + 1)) = ((𝑁𝑘) − 1))
152151fveq2d 6182 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − (𝑘 + 1))) = (!‘((𝑁𝑘) − 1)))
153 facp1 13048 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0 → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
1541533ad2ant1 1080 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
155152, 154oveq12d 6653 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = ((!‘((𝑁𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1))))
156124, 125, 60mulassd 10048 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)) = ((!‘((𝑁𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1))))
157155, 156eqtr4d 2657 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)))
158157oveq2d 6651 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))))
15953nn0ge0d 11339 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ (𝑘 + 1))
16052nnzd 11466 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℤ)
161 elfz 12317 . . . . . . . . . . . . . . . . . . 19 (((𝑘 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
162160, 133, 79, 161syl3anc 1324 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
163159, 94, 162mpbir2and 956 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ (0...𝑁))
164 bcval2 13075 . . . . . . . . . . . . . . . . 17 ((𝑘 + 1) ∈ (0...𝑁) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))))
165163, 164syl 17 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))))
16652nnne0d 11050 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≠ 0)
167139, 140, 60, 141, 166divdiv1d 10817 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)) = ((!‘𝑁) / (((!‘((𝑁𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))))
168158, 165, 1673eqtr4d 2664 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = (((!‘𝑁) / ((!‘((𝑁𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))
169120, 144, 1683brtr4d 4676 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))
1701693exp 1262 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))))
17148, 170syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴)) → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))))
1721713impia 1259 . . . . . . . . . . 11 ((𝐴 ∈ ℕ0𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))
1731723coml 1270 . . . . . . . . . 10 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))
174 simp2 1060 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝑁 ∈ ℕ0)
175 nn0z 11385 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℕ0𝐴 ∈ ℤ)
1761753ad2ant3 1082 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → 𝐴 ∈ ℤ)
177174, 176, 29syl2anc 692 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝐴) ∈ ℕ0)
178177nn0red 11337 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝐴) ∈ ℝ)
179 bccl 13092 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → (𝑁C𝑘) ∈ ℕ0)
180174, 36, 179syl2anc 692 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝑘) ∈ ℕ0)
181180nn0red 11337 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C𝑘) ∈ ℝ)
18236peano2zd 11470 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑘 + 1) ∈ ℤ)
183 bccl 13092 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑁C(𝑘 + 1)) ∈ ℕ0)
184174, 182, 183syl2anc 692 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C(𝑘 + 1)) ∈ ℕ0)
185184nn0red 11337 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝑁C(𝑘 + 1)) ∈ ℝ)
186 letr 10116 . . . . . . . . . . . 12 (((𝑁C𝐴) ∈ ℝ ∧ (𝑁C𝑘) ∈ ℝ ∧ (𝑁C(𝑘 + 1)) ∈ ℝ) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
187178, 181, 185, 186syl3anc 1324 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ𝐴) ∧ 𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
188187expcomd 454 . . . . . . . . . 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 1266 . . . . . 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 11731 . . . 4 (𝐵 ∈ (ℤ𝐴) → ((𝑁 ∈ ℕ0𝐴 ∈ ℕ0) → (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))
1951943imp 1254 . . 3 ((𝐵 ∈ (ℤ𝐴) ∧ (𝑁 ∈ ℕ0𝐴 ∈ ℕ0) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
1961, 2, 7, 8, 195syl121anc 1329 . 2 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝑁C𝐴) ≤ (𝑁C𝐵))
197 simpl1 1062 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝑁 ∈ ℕ0)
1984adantr 481 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐴 ∈ ℤ)
199 orc 400 . . . . 5 (𝐴 < 0 → (𝐴 < 0 ∨ 𝑁 < 𝐴))
200199adantl 482 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝐴 < 0 ∨ 𝑁 < 𝐴))
201 bcval4 13077 . . . 4 ((𝑁 ∈ ℕ0𝐴 ∈ ℤ ∧ (𝐴 < 0 ∨ 𝑁 < 𝐴)) → (𝑁C𝐴) = 0)
202197, 198, 200, 201syl3anc 1324 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) = 0)
203 simpl2 1063 . . . . . 6 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ (ℤ𝐴))
204 eluzelz 11682 . . . . . 6 (𝐵 ∈ (ℤ𝐴) → 𝐵 ∈ ℤ)
205203, 204syl 17 . . . . 5 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ ℤ)
206 bccl 13092 . . . . 5 ((𝑁 ∈ ℕ0𝐵 ∈ ℤ) → (𝑁C𝐵) ∈ ℕ0)
207197, 205, 206syl2anc 692 . . . 4 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐵) ∈ ℕ0)
208207nn0ge0d 11339 . . 3 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 0 ≤ (𝑁C𝐵))
209202, 208eqbrtrd 4666 . 2 (((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) ≤ (𝑁C𝐵))
210 0re 10025 . . 3 0 ∈ ℝ
2114zred 11467 . . 3 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℝ)
212 lelttric 10129 . . 3 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 ≤ 𝐴𝐴 < 0))
213210, 211, 212sylancr 694 . 2 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (0 ≤ 𝐴𝐴 < 0))
214196, 209, 213mpjaodan 826 1 ((𝑁 ∈ ℕ0𝐵 ∈ (ℤ𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1481  wcel 1988   class class class wbr 4644  cfv 5876  (class class class)co 6635  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926   < clt 10059  cle 10060  cmin 10251   / cdiv 10669  cn 11005  2c2 11055  0cn0 11277  cz 11362  cuz 11672  +crp 11817  ...cfz 12311  !cfa 13043  Ccbc 13072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-n0 11278  df-z 11363  df-uz 11673  df-rp 11818  df-fz 12312  df-seq 12785  df-fac 13044  df-bc 13073
This theorem is referenced by:  bcmax  24984
  Copyright terms: Public domain W3C validator