Theorem bcmono 25855

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.

Step	Hyp	Ref	Expression
1		simpl2 1188	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ∈ (ℤ≥‘𝐴))
2		simpl1 1187	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝑁 ∈ ℕ0)
3		eluzel2 12251	. . . . . 6 ⊢ (𝐵 ∈ (ℤ≥‘𝐴) → 𝐴 ∈ ℤ)
4	3	3ad2ant2 1130	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℤ)
5	4	anim1i 616	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
6		elnn0z 11997	. . . 4 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
7	5, 6	sylibr 236	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℕ0)
8		simpl3 1189	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ≤ (𝑁 / 2))
9		breq1 5071	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐴 ≤ (𝑁 / 2)))
10		oveq2 7166	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑁C𝑥) = (𝑁C𝐴))
11	10	breq2d 5080	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐴)))
12	9, 11	imbi12d 347	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
13	12	imbi2d 343	. . . . 5 ⊢ (𝑥 = 𝐴 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))))
14		breq1 5071	. . . . . . 7 ⊢ (𝑥 = 𝑘 → (𝑥 ≤ (𝑁 / 2) ↔ 𝑘 ≤ (𝑁 / 2)))
15		oveq2 7166	. . . . . . . 8 ⊢ (𝑥 = 𝑘 → (𝑁C𝑥) = (𝑁C𝑘))
16	15	breq2d 5080	. . . . . . 7 ⊢ (𝑥 = 𝑘 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝑘)))
17	14, 16	imbi12d 347	. . . . . 6 ⊢ (𝑥 = 𝑘 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))
18	17	imbi2d 343	. . . . 5 ⊢ (𝑥 = 𝑘 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)))))
19		breq1 5071	. . . . . . 7 ⊢ (𝑥 = (𝑘 + 1) → (𝑥 ≤ (𝑁 / 2) ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
20		oveq2 7166	. . . . . . . 8 ⊢ (𝑥 = (𝑘 + 1) → (𝑁C𝑥) = (𝑁C(𝑘 + 1)))
21	20	breq2d 5080	. . . . . . 7 ⊢ (𝑥 = (𝑘 + 1) → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
22	19, 21	imbi12d 347	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
23	22	imbi2d 343	. . . . 5 ⊢ (𝑥 = (𝑘 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
24		breq1 5071	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐵 ≤ (𝑁 / 2)))
25		oveq2 7166	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝑁C𝑥) = (𝑁C𝐵))
26	25	breq2d 5080	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐵)))
27	24, 26	imbi12d 347	. . . . . 6 ⊢ (𝑥 = 𝐵 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))
28	27	imbi2d 343	. . . . 5 ⊢ (𝑥 = 𝐵 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵)))))
29		bccl 13685	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝑁C𝐴) ∈ ℕ0)
30	29	nn0red 11959	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝑁C𝐴) ∈ ℝ)
31	30	leidd 11208	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝑁C𝐴) ≤ (𝑁C𝐴))
32	31	a1d 25	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))
33	32	expcom 416	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝑁 ∈ ℕ0 → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
34	33	adantrd 494	. . . . 5 ⊢ (𝐴 ∈ ℤ → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))
35		eluzelz 12256	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ≥‘𝐴) → 𝑘 ∈ ℤ)
36	35	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → 𝑘 ∈ ℤ)
37	36	zred 12090	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → 𝑘 ∈ ℝ)
38	37	lep1d 11573	. . . . . . . . . 10 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → 𝑘 ≤ (𝑘 + 1))
39		peano2re 10815	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
40	37, 39	syl 17	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ)
41		nn0re 11909	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
42	41	3ad2ant2 1130	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → 𝑁 ∈ ℝ)
43	42	rehalfcld 11887	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑁 / 2) ∈ ℝ)
44		letr 10736	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑁 / 2) ∈ ℝ) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2)))
45	37, 40, 43, 44	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2)))
46	38, 45	mpand 693	. . . . . . . . 9 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → 𝑘 ≤ (𝑁 / 2)))
47	46	imim1d 82	. . . . . . . 8 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))
48		eluznn0 12320	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘𝐴)) → 𝑘 ∈ ℕ0)
49	41	3ad2ant2 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℝ)
50		nn0re 11909	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ)
51	50	3ad2ant1 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℝ)
52		nn0p1nn 11939	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
53	52	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ)
54	53	nnnn0d 11958	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ0)
55	54	nn0red 11959	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℝ)
56	53	nncnd 11656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℂ)
57	56	2timesd 11883	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) = ((𝑘 + 1) + (𝑘 + 1)))
58		simp3 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 / 2))
59		2re 11714	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ
60		2pos 11743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < 2
61	59, 60	pm3.2i 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 ∈ ℝ ∧ 0 < 2)
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 ∈ ℝ ∧ 0 < 2))
63		lemuldiv2 11523	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑘 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
64	55, 49, 62, 63	syl3anc 1367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2)))
65	58, 64	mpbird 259	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) ≤ 𝑁)
66	57, 65	eqbrtrrd 5092	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ≤ 𝑁)
67	51	lep1d 11573	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑘 + 1))
68	49, 51, 55, 55, 66, 67	lesub3d 11260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 − 𝑘))
69		nnre 11647	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ∈ ℝ)
70		nngt0 11671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 + 1) ∈ ℕ → 0 < (𝑘 + 1))
71	69, 70	jca 514	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 + 1) ∈ ℕ → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)))
72	53, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)))
73		nn0z 12008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
74	73	3ad2ant2 1130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℤ)
75		nn0z 12008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ)
76	75	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℤ)
77	74, 76	zsubcld 12095	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℤ)
78	49	rehalfcld 11887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ∈ ℝ)
79	49, 59	jctir 523	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 ∈ ℝ ∧ 2 ∈ ℝ))
80		nn0ge0 11925	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)
81	80	3ad2ant2 1130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑁)
82		1le2 11849	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ≤ 2
83	81, 82	jctir 523	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (0 ≤ 𝑁 ∧ 1 ≤ 2))
84		lemulge12 11505	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (0 ≤ 𝑁 ∧ 1 ≤ 2)) → 𝑁 ≤ (2 · 𝑁))
85	79, 83, 84	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ≤ (2 · 𝑁))
86		ledivmul 11518	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑁 / 2) ≤ 𝑁 ↔ 𝑁 ≤ (2 · 𝑁)))
87	49, 49, 62, 86	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 / 2) ≤ 𝑁 ↔ 𝑁 ≤ (2 · 𝑁)))
88	85, 87	mpbird 259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ≤ 𝑁)
89	55, 78, 49, 58, 88	letrd 10799	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ 𝑁)
90		1red 10644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈ ℝ)
91	51, 90, 49	leaddsub2d 11244	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑘)))
92	89, 91	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ≤ (𝑁 − 𝑘))
93		elnnz1 12011	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 𝑘) ∈ ℕ ↔ ((𝑁 − 𝑘) ∈ ℤ ∧ 1 ≤ (𝑁 − 𝑘)))
94	77, 92, 93	sylanbrc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℕ)
95		nnre 11647	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 𝑘) ∈ ℕ → (𝑁 − 𝑘) ∈ ℝ)
96		nngt0 11671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 𝑘) ∈ ℕ → 0 < (𝑁 − 𝑘))
97	95, 96	jca 514	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 𝑘) ∈ ℕ → ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘)))
98	94, 97	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘)))
99		faccl 13646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
100	99	3ad2ant2 1130	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℕ)
101		nnm1nn0 11941	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑘) ∈ ℕ → ((𝑁 − 𝑘) − 1) ∈ ℕ0)
102		faccl 13646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 − 𝑘) − 1) ∈ ℕ0 → (!‘((𝑁 − 𝑘) − 1)) ∈ ℕ)
103	94, 101, 102	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁 − 𝑘) − 1)) ∈ ℕ)
104		faccl 13646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
105	104	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℕ)
106	103, 105	nnmulcld 11693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈ ℕ)
107		nnrp 12403	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℝ+)
108		nnrp 12403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈ ℕ → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+)
109		rpdivcl 12417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((!‘𝑁) ∈ ℝ+ ∧ ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+) → ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
110	107, 108, 109	syl2an 597	. . . . . . . . . . . . . . . . . . 19 ⊢ (((!‘𝑁) ∈ ℕ ∧ ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈ ℕ) → ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
111	100, 106, 110	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ+)
112	111	rpregt0d 12440	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 < ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)))))
113		lediv2 11532	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘)) ∧ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 < ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))))) → ((𝑘 + 1) ≤ (𝑁 − 𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))))
114	72, 98, 112, 113	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ (𝑁 − 𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))))
115	68, 114	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))
116		facnn2 13645	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 𝑘) ∈ ℕ → (!‘(𝑁 − 𝑘)) = ((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘)))
117	94, 116	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − 𝑘)) = ((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘)))
118	117	oveq1d 7173	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − 𝑘)) · (!‘𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘)) · (!‘𝑘)))
119	103	nncnd 11656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁 − 𝑘) − 1)) ∈ ℂ)
120	105	nncnd 11656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℂ)
121	77	zcnd 12091	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℂ)
122	119, 120, 121	mul32d 10852	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘)) · (!‘𝑘)))
123	118, 122	eqtr4d 2861	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − 𝑘)) · (!‘𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘)))
124	123	oveq2d 7174	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘))) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘))))
125		nn0ge0 11925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ0 → 0 ≤ 𝑘)
126	125	3ad2ant1 1129	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑘)
127	51, 55, 49, 67, 89	letrd 10799	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ 𝑁)
128		0zd 11996	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ∈ ℤ)
129		elfz 12901	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
130	76, 128, 74, 129	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
131	126, 127, 130	mpbir2and 711	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ (0...𝑁))
132		bcval2 13668	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘))))
133	131, 132	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘))))
134	100	nncnd 11656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℂ)
135	106	nncnd 11656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈ ℂ)
136	106	nnne0d 11690	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ≠ 0)
137	94	nnne0d 11690	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ≠ 0)
138	134, 135, 121, 136, 137	divdiv1d 11449	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘))))
139	124, 133, 138	3eqtr4d 2868	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)))
140		nn0cn 11910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
141	140	3ad2ant2 1130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℂ)
142		nn0cn 11910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
143	142	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℂ)
144		1cnd 10638	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈ ℂ)
145	141, 143, 144	subsub4d 11030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 − 𝑘) − 1) = (𝑁 − (𝑘 + 1)))
146	145	eqcomd 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − (𝑘 + 1)) = ((𝑁 − 𝑘) − 1))
147	146	fveq2d 6676	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − (𝑘 + 1))) = (!‘((𝑁 − 𝑘) − 1)))
148		facp1 13641	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ0 → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
149	148	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1)))
150	147, 149	oveq12d 7176	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = ((!‘((𝑁 − 𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1))))
151	119, 120, 56	mulassd 10666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)) = ((!‘((𝑁 − 𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1))))
152	150, 151	eqtr4d 2861	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)))
153	152	oveq2d 7174	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))))
154	54	nn0ge0d 11961	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ (𝑘 + 1))
155	53	nnzd 12089	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℤ)
156		elfz 12901	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
157	155, 128, 74, 156	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
158	154, 89, 157	mpbir2and 711	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ (0...𝑁))
159		bcval2 13668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (0...𝑁) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))))
160	158, 159	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))))
161	53	nnne0d 11690	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≠ 0)
162	134, 135, 56, 136, 161	divdiv1d 11449	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))))
163	153, 160, 162	3eqtr4d 2868	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))
164	115, 139, 163	3brtr4d 5100	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))
165	164	3exp 1115	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))))
166	48, 165	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘𝐴)) → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))))
167	166	3impia 1113	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))
168	167	3coml 1123	. . . . . . . . . 10 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))
169		simp2 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → 𝑁 ∈ ℕ0)
170		nn0z 12008	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ)
171	170	3ad2ant3 1131	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → 𝐴 ∈ ℤ)
172	169, 171, 29	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑁C𝐴) ∈ ℕ0)
173	172	nn0red 11959	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑁C𝐴) ∈ ℝ)
174		bccl 13685	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ) → (𝑁C𝑘) ∈ ℕ0)
175	169, 36, 174	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑁C𝑘) ∈ ℕ0)
176	175	nn0red 11959	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑁C𝑘) ∈ ℝ)
177	36	peano2zd 12093	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑘 + 1) ∈ ℤ)
178		bccl 13685	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑁C(𝑘 + 1)) ∈ ℕ0)
179	169, 177, 178	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑁C(𝑘 + 1)) ∈ ℕ0)
180	179	nn0red 11959	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑁C(𝑘 + 1)) ∈ ℝ)
181		letr 10736	. . . . . . . . . . . 12 ⊢ (((𝑁C𝐴) ∈ ℝ ∧ (𝑁C𝑘) ∈ ℝ ∧ (𝑁C(𝑘 + 1)) ∈ ℝ) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
182	173, 176, 180, 181	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))
183	182	expcomd 419	. . . . . . . . . 10 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
184	168, 183	syld 47	. . . . . . . . 9 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
185	184	a2d 29	. . . . . . . 8 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
186	47, 185	syld 47	. . . . . . 7 ⊢ ((𝑘 ∈ (ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))
187	186	3expib 1118	. . . . . 6 ⊢ (𝑘 ∈ (ℤ≥‘𝐴) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
188	187	a2d 29	. . . . 5 ⊢ (𝑘 ∈ (ℤ≥‘𝐴) → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))))
189	13, 18, 23, 28, 34, 188	uzind4 12309	. . . 4 ⊢ (𝐵 ∈ (ℤ≥‘𝐴) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) → (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))
190	189	3imp 1107	. . 3 ⊢ ((𝐵 ∈ (ℤ≥‘𝐴) ∧ (𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
191	1, 2, 7, 8, 190	syl121anc 1371	. 2 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝑁C𝐴) ≤ (𝑁C𝐵))
192		simpl1 1187	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝑁 ∈ ℕ0)
193	4	adantr 483	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐴 ∈ ℤ)
194		animorrl 977	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝐴 < 0 ∨ 𝑁 < 𝐴))
195		bcval4 13670	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ (𝐴 < 0 ∨ 𝑁 < 𝐴)) → (𝑁C𝐴) = 0)
196	192, 193, 194, 195	syl3anc 1367	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) = 0)
197		simpl2 1188	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ (ℤ≥‘𝐴))
198		eluzelz 12256	. . . . . 6 ⊢ (𝐵 ∈ (ℤ≥‘𝐴) → 𝐵 ∈ ℤ)
199	197, 198	syl 17	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ ℤ)
200		bccl 13685	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ℤ) → (𝑁C𝐵) ∈ ℕ0)
201	192, 199, 200	syl2anc 586	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐵) ∈ ℕ0)
202	201	nn0ge0d 11961	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 0 ≤ (𝑁C𝐵))
203	196, 202	eqbrtrd 5090	. 2 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) ≤ (𝑁C𝐵))
204		0re 10645	. . 3 ⊢ 0 ∈ ℝ
205	4	zred 12090	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℝ)
206		lelttric 10749	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 ≤ 𝐴 ∨ 𝐴 < 0))
207	204, 205, 206	sylancr 589	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (0 ≤ 𝐴 ∨ 𝐴 < 0))
208	191, 203, 207	mpjaodan 955	1 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   class class class wbr 5068  ‘cfv 6357  (class class class)co 7158  ℂcc 10537  ℝcr 10538  0cc0 10539  1c1 10540   + caddc 10542   · cmul 10544   < clt 10677   ≤ cle 10678   − cmin 10872   / cdiv 11299  ℕcn 11640  2c2 11695  ℕ₀cn0 11900  ℤcz 11984  ℤ_≥cuz 12246  ℝ⁺crp 12392  ...cfz 12895  !cfa 13636  Ccbc 13665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641  df-2 11703  df-n0 11901  df-z 11985  df-uz 12247  df-rp 12393  df-fz 12896  df-seq 13373  df-fac 13637  df-bc 13666

This theorem is referenced by:  bcmax  25856