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	$⊢ (N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \to (\binom{N}{A}) \leq (\binom{N}{B})$

Proof

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

Metamath Proof Explorer

Theorem bcmono

Proof