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 𝐵 ) )