Metamath Proof Explorer

Theorem bcmono

Description: The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014)

Ref Expression
Assertion bcmono ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 0 ≤ 𝐴 ) → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
2 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 0 ≤ 𝐴 ) → 𝑁 ∈ ℕ0 )
3 eluzel2 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐴 ∈ ℤ )
4 3 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → 𝐴 ∈ ℤ )
5 4 anim1i ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 0 ≤ 𝐴 ) → ( 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) )
6 elnn0z ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) )
7 5 6 sylibr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℕ0 )
8 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 0 ≤ 𝐴 ) → 𝐵 ≤ ( 𝑁 / 2 ) )
9 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≤ ( 𝑁 / 2 ) ↔ 𝐴 ≤ ( 𝑁 / 2 ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 C 𝑥 ) = ( 𝑁 C 𝐴 ) )
11 10 breq2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ↔ ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐴 ) ) )
12 9 11 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ) ↔ ( 𝐴 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐴 ) ) ) )
13 12 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑥 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ) ) ↔ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐴 ) ) ) ) )
14 breq1 ⊢ ( 𝑥 = 𝑘 → ( 𝑥 ≤ ( 𝑁 / 2 ) ↔ 𝑘 ≤ ( 𝑁 / 2 ) ) )
15 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑁 C 𝑥 ) = ( 𝑁 C 𝑘 ) )
16 15 breq2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ↔ ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) )
17 14 16 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑥 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ) ↔ ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) ) )
18 17 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑥 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ) ) ↔ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) ) ) )
19 breq1 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑥 ≤ ( 𝑁 / 2 ) ↔ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) )
20 oveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑁 C 𝑥 ) = ( 𝑁 C ( 𝑘 + 1 ) ) )
21 20 breq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ↔ ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
22 19 21 imbi12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑥 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ) ↔ ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
23 22 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑥 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ) ) ↔ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) ) )
24 breq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ≤ ( 𝑁 / 2 ) ↔ 𝐵 ≤ ( 𝑁 / 2 ) ) )
25 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑁 C 𝑥 ) = ( 𝑁 C 𝐵 ) )
26 25 breq2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ↔ ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) ) )
27 24 26 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ) ↔ ( 𝐵 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) ) ) )
28 27 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑥 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑥 ) ) ) ↔ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝐵 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) ) ) ) )
29 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝑁 C 𝐴 ) ∈ ℕ0 )
30 29 nn0red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝑁 C 𝐴 ) ∈ ℝ )
31 30 leidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐴 ) )
32 31 a1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐴 ) ) )
33 32 expcom ⊢ ( 𝐴 ∈ ℤ → ( 𝑁 ∈ ℕ0 → ( 𝐴 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐴 ) ) ) )
34 33 adantrd ⊢ ( 𝐴 ∈ ℤ → ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐴 ) ) ) )
35 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑘 ∈ ℤ )
36 35 3ad2ant1 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → 𝑘 ∈ ℤ )
37 36 zred ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
38 37 lep1d ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → 𝑘 ≤ ( 𝑘 + 1 ) )
39 peano2re ⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
40 37 39 syl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℝ )
41 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
42 41 3ad2ant2 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
43 42 rehalfcld ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 / 2 ) ∈ ℝ )
44 letr ⊢ ( ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ∧ ( 𝑁 / 2 ) ∈ ℝ ) → ( ( 𝑘 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ≤ ( 𝑁 / 2 ) ) )
45 37 40 43 44 syl3anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ≤ ( 𝑁 / 2 ) ) )
46 38 45 mpand ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → 𝑘 ≤ ( 𝑁 / 2 ) ) )
47 46 imim1d ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) ) )
48 eluznn0 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝑘 ∈ ℕ0 )
49 41 3ad2ant2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑁 ∈ ℝ )
50 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
51 50 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ∈ ℝ )
52 nn0p1nn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
53 52 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ∈ ℕ )
54 53 nnnn0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
55 54 nn0red ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
56 53 nncnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ∈ ℂ )
57 56 2timesd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 2 · ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) + ( 𝑘 + 1 ) ) )
58 simp3 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) )
59 2re ⊢ 2 ∈ ℝ
60 2pos ⊢ 0 < 2
61 59 60 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
62 61 a1i ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
63 lemuldiv2 ⊢ ( ( ( 𝑘 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · ( 𝑘 + 1 ) ) ≤ 𝑁 ↔ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) )
64 55 49 62 63 syl3anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 2 · ( 𝑘 + 1 ) ) ≤ 𝑁 ↔ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) )
65 58 64 mpbird ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 2 · ( 𝑘 + 1 ) ) ≤ 𝑁 )
66 57 65 eqbrtrrd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑘 + 1 ) + ( 𝑘 + 1 ) ) ≤ 𝑁 )
67 51 lep1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ≤ ( 𝑘 + 1 ) )
68 49 51 55 55 66 67 lesub3d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ≤ ( 𝑁 − 𝑘 ) )
69 nnre ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝑘 + 1 ) ∈ ℝ )
70 nngt0 ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → 0 < ( 𝑘 + 1 ) )
71 69 70 jca ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( ( 𝑘 + 1 ) ∈ ℝ ∧ 0 < ( 𝑘 + 1 ) ) )
72 53 71 syl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑘 + 1 ) ∈ ℝ ∧ 0 < ( 𝑘 + 1 ) ) )
73 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
74 73 3ad2ant2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑁 ∈ ℤ )
75 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
76 75 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ∈ ℤ )
77 74 76 zsubcld ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
78 49 rehalfcld ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 / 2 ) ∈ ℝ )
79 49 59 jctir ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ) )
80 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
81 80 3ad2ant2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 0 ≤ 𝑁 )
82 1le2 ⊢ 1 ≤ 2
83 81 82 jctir ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 0 ≤ 𝑁 ∧ 1 ≤ 2 ) )
84 lemulge12 ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ) ∧ ( 0 ≤ 𝑁 ∧ 1 ≤ 2 ) ) → 𝑁 ≤ ( 2 · 𝑁 ) )
85 79 83 84 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑁 ≤ ( 2 · 𝑁 ) )
86 ledivmul ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑁 / 2 ) ≤ 𝑁 ↔ 𝑁 ≤ ( 2 · 𝑁 ) ) )
87 49 49 62 86 syl3anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑁 / 2 ) ≤ 𝑁 ↔ 𝑁 ≤ ( 2 · 𝑁 ) ) )
88 85 87 mpbird ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 / 2 ) ≤ 𝑁 )
89 55 78 49 58 88 letrd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ≤ 𝑁 )
90 1red ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 1 ∈ ℝ )
91 51 90 49 leaddsub2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑘 + 1 ) ≤ 𝑁 ↔ 1 ≤ ( 𝑁 − 𝑘 ) ) )
92 89 91 mpbid ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 1 ≤ ( 𝑁 − 𝑘 ) )
93 elnnz1 ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ ↔ ( ( 𝑁 − 𝑘 ) ∈ ℤ ∧ 1 ≤ ( 𝑁 − 𝑘 ) ) )
94 77 92 93 sylanbrc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ )
95 nnre ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ → ( 𝑁 − 𝑘 ) ∈ ℝ )
96 nngt0 ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ → 0 < ( 𝑁 − 𝑘 ) )
97 95 96 jca ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ → ( ( 𝑁 − 𝑘 ) ∈ ℝ ∧ 0 < ( 𝑁 − 𝑘 ) ) )
98 94 97 syl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑁 − 𝑘 ) ∈ ℝ ∧ 0 < ( 𝑁 − 𝑘 ) ) )
99 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
100 99 3ad2ant2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ 𝑁 ) ∈ ℕ )
101 nnm1nn0 ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 )
102 faccl ⊢ ( ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) ∈ ℕ )
103 94 101 102 3syl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) ∈ ℕ )
104 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
105 104 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
106 103 105 nnmulcld ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ∈ ℕ )
107 nnrp ⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℝ+ )
108 nnrp ⊢ ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ∈ ℕ → ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ∈ ℝ+ )
109 rpdivcl ⊢ ( ( ( ! ‘ 𝑁 ) ∈ ℝ+ ∧ ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) ∈ ℝ+ )
110 107 108 109 syl2an ⊢ ( ( ( ! ‘ 𝑁 ) ∈ ℕ ∧ ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ∈ ℕ ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) ∈ ℝ+ )
111 100 106 110 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) ∈ ℝ+ )
112 111 rpregt0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) ∈ ℝ ∧ 0 < ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) ) )
113 lediv2 ⊢ ( ( ( ( 𝑘 + 1 ) ∈ ℝ ∧ 0 < ( 𝑘 + 1 ) ) ∧ ( ( 𝑁 − 𝑘 ) ∈ ℝ ∧ 0 < ( 𝑁 − 𝑘 ) ) ∧ ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) ∈ ℝ ∧ 0 < ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 − 𝑘 ) ↔ ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑁 − 𝑘 ) ) ≤ ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑘 + 1 ) ) ) )
114 72 98 112 113 syl3anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 − 𝑘 ) ↔ ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑁 − 𝑘 ) ) ≤ ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑘 + 1 ) ) ) )
115 68 114 mpbid ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑁 − 𝑘 ) ) ≤ ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑘 + 1 ) ) )
116 facnn2 ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ → ( ! ‘ ( 𝑁 − 𝑘 ) ) = ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( 𝑁 − 𝑘 ) ) )
117 94 116 syl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ ( 𝑁 − 𝑘 ) ) = ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( 𝑁 − 𝑘 ) ) )
118 117 oveq1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) = ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) )
119 103 nncnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) ∈ ℂ )
120 105 nncnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
121 77 zcnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 − 𝑘 ) ∈ ℂ )
122 119 120 121 mul32d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑁 − 𝑘 ) ) = ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) )
123 118 122 eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) = ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑁 − 𝑘 ) ) )
124 123 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑁 − 𝑘 ) ) ) )
125 0zd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 0 ∈ ℤ )
126 nn0ge0 ⊢ ( 𝑘 ∈ ℕ0 → 0 ≤ 𝑘 )
127 126 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 0 ≤ 𝑘 )
128 51 55 49 67 89 letrd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ≤ 𝑁 )
129 125 74 76 127 128 elfzd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
130 bcval2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑘 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) )
131 129 130 syl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝑘 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) )
132 100 nncnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
133 106 nncnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ∈ ℂ )
134 106 nnne0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ≠ 0 )
135 94 nnne0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 − 𝑘 ) ≠ 0 )
136 132 133 121 134 135 divdiv1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑁 − 𝑘 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑁 − 𝑘 ) ) ) )
137 124 131 136 3eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝑘 ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑁 − 𝑘 ) ) )
138 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
139 138 3ad2ant2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑁 ∈ ℂ )
140 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
141 140 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ∈ ℂ )
142 1cnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 1 ∈ ℂ )
143 139 141 142 subsub4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑁 − 𝑘 ) − 1 ) = ( 𝑁 − ( 𝑘 + 1 ) ) )
144 143 eqcomd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 − ( 𝑘 + 1 ) ) = ( ( 𝑁 − 𝑘 ) − 1 ) )
145 144 fveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) = ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) )
146 facp1 ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
147 146 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
148 145 147 oveq12d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) = ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
149 119 120 56 mulassd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) = ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
150 148 149 eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) = ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) )
151 150 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) ) )
152 53 nnzd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
153 54 nn0ge0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 0 ≤ ( 𝑘 + 1 ) )
154 125 74 152 153 89 elfzd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
155 bcval2 ⊢ ( ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) )
156 154 155 syl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) )
157 53 nnne0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ≠ 0 )
158 132 133 56 134 157 divdiv1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) ) )
159 151 156 158 3eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C ( 𝑘 + 1 ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑘 + 1 ) ) )
160 115 137 159 3brtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) )
161 160 3exp ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
162 48 161 syl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑁 ∈ ℕ0 → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
163 162 3impia ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
164 163 3coml ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
165 simp2 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
166 nn0z ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
167 166 3ad2ant3 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
168 165 167 29 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C 𝐴 ) ∈ ℕ0 )
169 168 nn0red ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C 𝐴 ) ∈ ℝ )
170 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
171 165 36 170 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
172 171 nn0red ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C 𝑘 ) ∈ ℝ )
173 36 peano2zd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℤ )
174 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 + 1 ) ) ∈ ℕ0 )
175 165 173 174 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C ( 𝑘 + 1 ) ) ∈ ℕ0 )
176 175 nn0red ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C ( 𝑘 + 1 ) ) ∈ ℝ )
177 letr ⊢ ( ( ( 𝑁 C 𝐴 ) ∈ ℝ ∧ ( 𝑁 C 𝑘 ) ∈ ℝ ∧ ( 𝑁 C ( 𝑘 + 1 ) ) ∈ ℝ ) → ( ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ∧ ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
178 169 172 176 177 syl3anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ∧ ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
179 178 expcomd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) → ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
180 164 179 syld ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
181 180 a2d ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
182 47 181 syld ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
183 182 3expib ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) ) )
184 183 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) ) )
185 13 18 23 28 34 184 uzind4 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝐵 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) ) ) )
186 185 3imp ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )
187 1 2 7 8 186 syl121anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 0 ≤ 𝐴 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )
188 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 𝑁 ∈ ℕ0 )
189 4 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 𝐴 ∈ ℤ )
190 animorrl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → ( 𝐴 < 0 ∨ 𝑁 < 𝐴 ) )
191 bcval4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 < 0 ∨ 𝑁 < 𝐴 ) ) → ( 𝑁 C 𝐴 ) = 0 )
192 188 189 190 191 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → ( 𝑁 C 𝐴 ) = 0 )
193 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
194 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℤ )
195 193 194 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 𝐵 ∈ ℤ )
196 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ) → ( 𝑁 C 𝐵 ) ∈ ℕ0 )
197 188 195 196 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → ( 𝑁 C 𝐵 ) ∈ ℕ0 )
198 197 nn0ge0d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 0 ≤ ( 𝑁 C 𝐵 ) )
199 192 198 eqbrtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )
200 0re ⊢ 0 ∈ ℝ
201 4 zred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → 𝐴 ∈ ℝ )
202 lelttric ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ∨ 𝐴 < 0 ) )
203 200 201 202 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → ( 0 ≤ 𝐴 ∨ 𝐴 < 0 ) )
204 187 199 203 mpjaodan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )