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		0zd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to 0 \in ℤ$
126		nn0ge0	$⊢ k \in ℕ_{0} \to 0 \leq k$
127	126	3ad2ant1	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to 0 \leq k$
128	51 55 49 67 89	letrd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to k \leq N$
129	125 74 76 127 128	elfzd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to k \in (0 \dots N)$
130		bcval2	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) = \frac{N!}{(N - k)! k!}$
131	129 130	syl	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to (\binom{N}{k}) = \frac{N!}{(N - k)! k!}$
132	100	nncnd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to N! \in ℂ$
133	106	nncnd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to (N - k - 1)! k! \in ℂ$
134	106	nnne0d	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to (N - k - 1)! k! \neq 0$
135	94	nnne0d	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to N - k \neq 0$
136	132 133 121 134 135	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)}$
137	124 131 136	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}$
138		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
139	138	3ad2ant2	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to N \in ℂ$
140		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
141	140	3ad2ant1	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to k \in ℂ$
142		1cnd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to 1 \in ℂ$
143	139 141 142	subsub4d	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to N - k - 1 = N - (k + 1)$
144	143	eqcomd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to N - (k + 1) = N - k - 1$
145	144	fveq2d	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to (N - (k + 1))! = (N - k - 1)!$
146		facp1	$⊢ k \in ℕ_{0} \to (k + 1)! = k! (k + 1)$
147	146	3ad2ant1	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to (k + 1)! = k! (k + 1)$
148	145 147	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)$
149	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)$
150	148 149	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)$
151	150	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)}$
152	53	nnzd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to k + 1 \in ℤ$
153	54	nn0ge0d	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to 0 \leq k + 1$
154	125 74 152 153 89	elfzd	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to k + 1 \in (0 \dots N)$
155		bcval2	$⊢ k + 1 \in (0 \dots N) \to (\binom{N}{k + 1}) = \frac{N!}{(N - (k + 1))! (k + 1)!}$
156	154 155	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)!}$
157	53	nnne0d	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to k + 1 \neq 0$
158	132 133 56 134 157	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)}$
159	151 156 158	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}$
160	115 137 159	3brtr4d	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0} \land k + 1 \leq \frac{N}{2}) \to (\binom{N}{k}) \leq (\binom{N}{k + 1})$
161	160	3exp	$⊢ k \in ℕ_{0} \to (N \in ℕ_{0} \to (k + 1 \leq \frac{N}{2} \to (\binom{N}{k}) \leq (\binom{N}{k + 1})))$
162	48 161	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})))$
163	162	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}))$
164	163	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}))$
165		simp2	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to N \in ℕ_{0}$
166		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
167	166	3ad2ant3	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to A \in ℤ$
168	165 167 29	syl2anc	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to (\binom{N}{A}) \in ℕ_{0}$
169	168	nn0red	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to (\binom{N}{A}) \in ℝ$
170		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
171	165 36 170	syl2anc	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to (\binom{N}{k}) \in ℕ_{0}$
172	171	nn0red	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to (\binom{N}{k}) \in ℝ$
173	36	peano2zd	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to k + 1 \in ℤ$
174		bccl	$⊢ (N \in ℕ_{0} \land k + 1 \in ℤ) \to (\binom{N}{k + 1}) \in ℕ_{0}$
175	165 173 174	syl2anc	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to (\binom{N}{k + 1}) \in ℕ_{0}$
176	175	nn0red	$⊢ (k \in ℤ_{\geq A} \land N \in ℕ_{0} \land A \in ℕ_{0}) \to (\binom{N}{k + 1}) \in ℝ$
177		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}))$
178	169 172 176 177	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}))$
179	178	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})))$
180	164 179	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})))$
181	180	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})))$
182	47 181	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})))$
183	182	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}))))$
184	183	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}))))$
185	13 18 23 28 34 184	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})))$
186	185	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})$
187	1 2 7 8 186	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})$
188		simpl1	$⊢ ((N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \land A < 0) \to N \in ℕ_{0}$
189	4	adantr	$⊢ ((N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \land A < 0) \to A \in ℤ$
190		animorrl	$⊢ ((N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \land A < 0) \to (A < 0 \lor N < A)$
191		bcval4	$⊢ (N \in ℕ_{0} \land A \in ℤ \land (A < 0 \lor N < A)) \to (\binom{N}{A}) = 0$
192	188 189 190 191	syl3anc	$⊢ ((N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \land A < 0) \to (\binom{N}{A}) = 0$
193		simpl2	$⊢ ((N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \land A < 0) \to B \in ℤ_{\geq A}$
194		eluzelz	$⊢ B \in ℤ_{\geq A} \to B \in ℤ$
195	193 194	syl	$⊢ ((N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \land A < 0) \to B \in ℤ$
196		bccl	$⊢ (N \in ℕ_{0} \land B \in ℤ) \to (\binom{N}{B}) \in ℕ_{0}$
197	188 195 196	syl2anc	$⊢ ((N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \land A < 0) \to (\binom{N}{B}) \in ℕ_{0}$
198	197	nn0ge0d	$⊢ ((N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \land A < 0) \to 0 \leq (\binom{N}{B})$
199	192 198	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})$
200		0re	$⊢ 0 \in ℝ$
201	4	zred	$⊢ (N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \to A \in ℝ$
202		lelttric	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 \leq A \lor A < 0)$
203	200 201 202	sylancr	$⊢ (N \in ℕ_{0} \land B \in ℤ_{\geq A} \land B \leq \frac{N}{2}) \to (0 \leq A \lor A < 0)$
204	187 199 203	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