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 nn0ge0 ⊢ ( 𝑘 ∈ ℕ0 → 0 ≤ 𝑘 )
126 125 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 0 ≤ 𝑘 )
127 51 55 49 67 89 letrd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ≤ 𝑁 )
128 0zd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 0 ∈ ℤ )
129 elfz ⊢ ( ( 𝑘 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
130 76 128 74 129 syl3anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
131 126 127 130 mpbir2and ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
132 bcval2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑘 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) )
133 131 132 syl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝑘 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) )
134 100 nncnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
135 106 nncnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ∈ ℂ )
136 106 nnne0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ≠ 0 )
137 94 nnne0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 − 𝑘 ) ≠ 0 )
138 134 135 121 136 137 divdiv1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑁 − 𝑘 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑁 − 𝑘 ) ) ) )
139 124 133 138 3eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝑘 ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑁 − 𝑘 ) ) )
140 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
141 140 3ad2ant2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑁 ∈ ℂ )
142 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
143 142 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 𝑘 ∈ ℂ )
144 1cnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 1 ∈ ℂ )
145 141 143 144 subsub4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑁 − 𝑘 ) − 1 ) = ( 𝑁 − ( 𝑘 + 1 ) ) )
146 145 eqcomd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 − ( 𝑘 + 1 ) ) = ( ( 𝑁 − 𝑘 ) − 1 ) )
147 146 fveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) = ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) )
148 facp1 ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
149 148 3ad2ant1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
150 147 149 oveq12d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) = ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
151 119 120 56 mulassd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) = ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
152 150 151 eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) = ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) )
153 152 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) ) )
154 54 nn0ge0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → 0 ≤ ( 𝑘 + 1 ) )
155 53 nnzd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
156 elfz ⊢ ( ( ( 𝑘 + 1 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) )
157 155 128 74 156 syl3anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) )
158 154 89 157 mpbir2and ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
159 bcval2 ⊢ ( ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) )
160 158 159 syl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑘 + 1 ) ) ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) )
161 53 nnne0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑘 + 1 ) ≠ 0 )
162 134 135 56 136 161 divdiv1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) ) )
163 153 160 162 3eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C ( 𝑘 + 1 ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝑘 ) − 1 ) ) · ( ! ‘ 𝑘 ) ) ) / ( 𝑘 + 1 ) ) )
164 115 139 163 3brtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) )
165 164 3exp ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
166 48 165 syl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑁 ∈ ℕ0 → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
167 166 3impia ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
168 167 3coml ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
169 simp2 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
170 nn0z ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
171 170 3ad2ant3 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
172 169 171 29 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C 𝐴 ) ∈ ℕ0 )
173 172 nn0red ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C 𝐴 ) ∈ ℝ )
174 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
175 169 36 174 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
176 175 nn0red ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C 𝑘 ) ∈ ℝ )
177 36 peano2zd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℤ )
178 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 + 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 + 1 ) ) ∈ ℕ0 )
179 169 177 178 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C ( 𝑘 + 1 ) ) ∈ ℕ0 )
180 179 nn0red ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑁 C ( 𝑘 + 1 ) ) ∈ ℝ )
181 letr ⊢ ( ( ( 𝑁 C 𝐴 ) ∈ ℝ ∧ ( 𝑁 C 𝑘 ) ∈ ℝ ∧ ( 𝑁 C ( 𝑘 + 1 ) ) ∈ ℝ ) → ( ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ∧ ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
182 173 176 180 181 syl3anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ∧ ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) )
183 182 expcomd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑁 C 𝑘 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) → ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
184 168 183 syld ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
185 184 a2d ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
186 47 185 syld ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) )
187 186 3expib ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) ) )
188 187 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑘 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝑘 ) ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C ( 𝑘 + 1 ) ) ) ) ) )
189 13 18 23 28 34 188 uzind4 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( 𝐵 ≤ ( 𝑁 / 2 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) ) ) )
190 189 3imp ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )
191 1 2 7 8 190 syl121anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 0 ≤ 𝐴 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )
192 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 𝑁 ∈ ℕ0 )
193 4 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 𝐴 ∈ ℤ )
194 animorrl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → ( 𝐴 < 0 ∨ 𝑁 < 𝐴 ) )
195 bcval4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 < 0 ∨ 𝑁 < 𝐴 ) ) → ( 𝑁 C 𝐴 ) = 0 )
196 192 193 194 195 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → ( 𝑁 C 𝐴 ) = 0 )
197 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
198 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℤ )
199 197 198 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 𝐵 ∈ ℤ )
200 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ) → ( 𝑁 C 𝐵 ) ∈ ℕ0 )
201 192 199 200 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → ( 𝑁 C 𝐵 ) ∈ ℕ0 )
202 201 nn0ge0d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → 0 ≤ ( 𝑁 C 𝐵 ) )
203 196 202 eqbrtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) ∧ 𝐴 < 0 ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )
204 0re ⊢ 0 ∈ ℝ
205 4 zred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → 𝐴 ∈ ℝ )
206 lelttric ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ∨ 𝐴 < 0 ) )
207 204 205 206 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → ( 0 ≤ 𝐴 ∨ 𝐴 < 0 ) )
208 191 203 207 mpjaodan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ≤ ( 𝑁 / 2 ) ) → ( 𝑁 C 𝐴 ) ≤ ( 𝑁 C 𝐵 ) )