bcled

Description: Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025)

	Ref	Expression
Hypotheses	bcled.1	$⊢ φ \to A \in ℕ_{0}$
	bcled.2	$⊢ φ \to B \in ℕ_{0}$
	bcled.3	$⊢ φ \to C \in ℤ$
	bcled.4	$⊢ φ \to A \leq B$
Assertion	bcled	$⊢ φ \to (\binom{A}{C}) \leq (\binom{B}{C})$

Proof

Step	Hyp	Ref	Expression
1		bcled.1	$⊢ φ \to A \in ℕ_{0}$
2		bcled.2	$⊢ φ \to B \in ℕ_{0}$
3		bcled.3	$⊢ φ \to C \in ℤ$
4		bcled.4	$⊢ φ \to A \leq B$
5		bcval2	$⊢ C \in (0 \dots A) \to (\binom{A}{C}) = \frac{A!}{(A - C)! C!}$
6	5	adantl	$⊢ (φ \land C \in (0 \dots A)) \to (\binom{A}{C}) = \frac{A!}{(A - C)! C!}$
7	1	adantr	$⊢ (φ \land C \in (0 \dots A)) \to A \in ℕ_{0}$
8	7	faccld	$⊢ (φ \land C \in (0 \dots A)) \to A! \in ℕ$
9	8	nncnd	$⊢ (φ \land C \in (0 \dots A)) \to A! \in ℂ$
10	7	nn0zd	$⊢ (φ \land C \in (0 \dots A)) \to A \in ℤ$
11	3	adantr	$⊢ (φ \land C \in (0 \dots A)) \to C \in ℤ$
12	10 11	zsubcld	$⊢ (φ \land C \in (0 \dots A)) \to A - C \in ℤ$
13	11	zred	$⊢ (φ \land C \in (0 \dots A)) \to C \in ℝ$
14	7	nn0red	$⊢ (φ \land C \in (0 \dots A)) \to A \in ℝ$
15		0red	$⊢ (φ \land C \in (0 \dots A)) \to 0 \in ℝ$
16		elfzle2	$⊢ C \in (0 \dots A) \to C \leq A$
17	16	adantl	$⊢ (φ \land C \in (0 \dots A)) \to C \leq A$
18	14	recnd	$⊢ (φ \land C \in (0 \dots A)) \to A \in ℂ$
19	18	subid1d	$⊢ (φ \land C \in (0 \dots A)) \to A - 0 = A$
20	19	eqcomd	$⊢ (φ \land C \in (0 \dots A)) \to A = A - 0$
21	17 20	breqtrd	$⊢ (φ \land C \in (0 \dots A)) \to C \leq A - 0$
22	13 14 15 21	lesubd	$⊢ (φ \land C \in (0 \dots A)) \to 0 \leq A - C$
23	12 22	jca	$⊢ (φ \land C \in (0 \dots A)) \to (A - C \in ℤ \land 0 \leq A - C)$
24		elnn0z	$⊢ A - C \in ℕ_{0} \leftrightarrow (A - C \in ℤ \land 0 \leq A - C)$
25	23 24	sylibr	$⊢ (φ \land C \in (0 \dots A)) \to A - C \in ℕ_{0}$
26	25	faccld	$⊢ (φ \land C \in (0 \dots A)) \to (A - C)! \in ℕ$
27	26	nncnd	$⊢ (φ \land C \in (0 \dots A)) \to (A - C)! \in ℂ$
28		elfznn0	$⊢ C \in (0 \dots A) \to C \in ℕ_{0}$
29	28	adantl	$⊢ (φ \land C \in (0 \dots A)) \to C \in ℕ_{0}$
30	29	faccld	$⊢ (φ \land C \in (0 \dots A)) \to C! \in ℕ$
31	30	nncnd	$⊢ (φ \land C \in (0 \dots A)) \to C! \in ℂ$
32	26	nnne0d	$⊢ (φ \land C \in (0 \dots A)) \to (A - C)! \neq 0$
33	30	nnne0d	$⊢ (φ \land C \in (0 \dots A)) \to C! \neq 0$
34	9 27 31 32 33	divdiv1d	$⊢ (φ \land C \in (0 \dots A)) \to \frac{\frac{A!}{(A - C)!}}{C!} = \frac{A!}{(A - C)! C!}$
35	34	eqcomd	$⊢ (φ \land C \in (0 \dots A)) \to \frac{A!}{(A - C)! C!} = \frac{\frac{A!}{(A - C)!}}{C!}$
36	8	nnred	$⊢ (φ \land C \in (0 \dots A)) \to A! \in ℝ$
37	26	nnred	$⊢ (φ \land C \in (0 \dots A)) \to (A - C)! \in ℝ$
38	36 37 32	redivcld	$⊢ (φ \land C \in (0 \dots A)) \to \frac{A!}{(A - C)!} \in ℝ$
39	2	adantr	$⊢ (φ \land C \in (0 \dots A)) \to B \in ℕ_{0}$
40	39	faccld	$⊢ (φ \land C \in (0 \dots A)) \to B! \in ℕ$
41	40	nnred	$⊢ (φ \land C \in (0 \dots A)) \to B! \in ℝ$
42	39	nn0zd	$⊢ (φ \land C \in (0 \dots A)) \to B \in ℤ$
43	42 11	zsubcld	$⊢ (φ \land C \in (0 \dots A)) \to B - C \in ℤ$
44	39	nn0red	$⊢ (φ \land C \in (0 \dots A)) \to B \in ℝ$
45	4	adantr	$⊢ (φ \land C \in (0 \dots A)) \to A \leq B$
46	13 14 44 17 45	letrd	$⊢ (φ \land C \in (0 \dots A)) \to C \leq B$
47	44	recnd	$⊢ (φ \land C \in (0 \dots A)) \to B \in ℂ$
48	47	subid1d	$⊢ (φ \land C \in (0 \dots A)) \to B - 0 = B$
49	48	eqcomd	$⊢ (φ \land C \in (0 \dots A)) \to B = B - 0$
50	46 49	breqtrd	$⊢ (φ \land C \in (0 \dots A)) \to C \leq B - 0$
51	13 44 15 50	lesubd	$⊢ (φ \land C \in (0 \dots A)) \to 0 \leq B - C$
52	43 51	jca	$⊢ (φ \land C \in (0 \dots A)) \to (B - C \in ℤ \land 0 \leq B - C)$
53		elnn0z	$⊢ B - C \in ℕ_{0} \leftrightarrow (B - C \in ℤ \land 0 \leq B - C)$
54	52 53	sylibr	$⊢ (φ \land C \in (0 \dots A)) \to B - C \in ℕ_{0}$
55	54	faccld	$⊢ (φ \land C \in (0 \dots A)) \to (B - C)! \in ℕ$
56	55	nnred	$⊢ (φ \land C \in (0 \dots A)) \to (B - C)! \in ℝ$
57	55	nnne0d	$⊢ (φ \land C \in (0 \dots A)) \to (B - C)! \neq 0$
58	41 56 57	redivcld	$⊢ (φ \land C \in (0 \dots A)) \to \frac{B!}{(B - C)!} \in ℝ$
59	30	nnrpd	$⊢ (φ \land C \in (0 \dots A)) \to C! \in ℝ^{+}$
60		nfv	$⊢ Ⅎ k (φ \land C \in (0 \dots A))$
61		fzfid	$⊢ (φ \land C \in (0 \dots A)) \to (0 \dots C - 1) \in Fin$
62	14	adantr	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to A \in ℝ$
63		elfzelz	$⊢ k \in (0 \dots C - 1) \to k \in ℤ$
64	63	adantl	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to k \in ℤ$
65	64	zred	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to k \in ℝ$
66	62 65	resubcld	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to A - k \in ℝ$
67		0red	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to 0 \in ℝ$
68	29	nn0red	$⊢ (φ \land C \in (0 \dots A)) \to C \in ℝ$
69	68	adantr	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to C \in ℝ$
70		1red	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to 1 \in ℝ$
71	69 70	resubcld	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to C - 1 \in ℝ$
72	62 67	resubcld	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to A - 0 \in ℝ$
73		elfzle2	$⊢ k \in (0 \dots C - 1) \to k \leq C - 1$
74	73	adantl	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to k \leq C - 1$
75	17	adantr	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to C \leq A$
76		0le1	$⊢ 0 \leq 1$
77	76	a1i	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to 0 \leq 1$
78	69 67 62 70 75 77	le2subd	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to C - 1 \leq A - 0$
79	65 71 72 74 78	letrd	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to k \leq A - 0$
80	65 62 67 79	lesubd	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to 0 \leq A - k$
81	44	adantr	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to B \in ℝ$
82	81 65	resubcld	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to B - k \in ℝ$
83	4	ad2antrr	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to A \leq B$
84	62 81 65 83	lesub1dd	$⊢ ((φ \land C \in (0 \dots A)) \land k \in (0 \dots C - 1)) \to A - k \leq B - k$
85	60 61 66 80 82 84	fprodle	$⊢ (φ \land C \in (0 \dots A)) \to \prod_{k = 0}^{C - 1} (A - k) \leq \prod_{k = 0}^{C - 1} (B - k)$
86	7	nn0cnd	$⊢ (φ \land C \in (0 \dots A)) \to A \in ℂ$
87		fallfacval	$⊢ (A \in ℂ \land C \in ℕ_{0}) \to A^{\underline{C}} = \prod_{k = 0}^{C - 1} (A - k)$
88	86 29 87	syl2anc	$⊢ (φ \land C \in (0 \dots A)) \to A^{\underline{C}} = \prod_{k = 0}^{C - 1} (A - k)$
89	88	eqcomd	$⊢ (φ \land C \in (0 \dots A)) \to \prod_{k = 0}^{C - 1} (A - k) = A^{\underline{C}}$
90	39	nn0cnd	$⊢ (φ \land C \in (0 \dots A)) \to B \in ℂ$
91		fallfacval	$⊢ (B \in ℂ \land C \in ℕ_{0}) \to B^{\underline{C}} = \prod_{k = 0}^{C - 1} (B - k)$
92	90 29 91	syl2anc	$⊢ (φ \land C \in (0 \dots A)) \to B^{\underline{C}} = \prod_{k = 0}^{C - 1} (B - k)$
93	92	eqcomd	$⊢ (φ \land C \in (0 \dots A)) \to \prod_{k = 0}^{C - 1} (B - k) = B^{\underline{C}}$
94	85 89 93	3brtr3d	$⊢ (φ \land C \in (0 \dots A)) \to A^{\underline{C}} \leq B^{\underline{C}}$
95		fallfacval4	$⊢ C \in (0 \dots A) \to A^{\underline{C}} = \frac{A!}{(A - C)!}$
96	95	adantl	$⊢ (φ \land C \in (0 \dots A)) \to A^{\underline{C}} = \frac{A!}{(A - C)!}$
97		0zd	$⊢ (φ \land C \in (0 \dots A)) \to 0 \in ℤ$
98	29	nn0ge0d	$⊢ (φ \land C \in (0 \dots A)) \to 0 \leq C$
99	68 14 44 17 45	letrd	$⊢ (φ \land C \in (0 \dots A)) \to C \leq B$
100	97 42 11 98 99	elfzd	$⊢ (φ \land C \in (0 \dots A)) \to C \in (0 \dots B)$
101		fallfacval4	$⊢ C \in (0 \dots B) \to B^{\underline{C}} = \frac{B!}{(B - C)!}$
102	100 101	syl	$⊢ (φ \land C \in (0 \dots A)) \to B^{\underline{C}} = \frac{B!}{(B - C)!}$
103	94 96 102	3brtr3d	$⊢ (φ \land C \in (0 \dots A)) \to \frac{A!}{(A - C)!} \leq \frac{B!}{(B - C)!}$
104	38 58 59 103	lediv1dd	$⊢ (φ \land C \in (0 \dots A)) \to \frac{\frac{A!}{(A - C)!}}{C!} \leq \frac{\frac{B!}{(B - C)!}}{C!}$
105	40	nncnd	$⊢ (φ \land C \in (0 \dots A)) \to B! \in ℂ$
106	55	nncnd	$⊢ (φ \land C \in (0 \dots A)) \to (B - C)! \in ℂ$
107	105 106 31 57 33	divdiv1d	$⊢ (φ \land C \in (0 \dots A)) \to \frac{\frac{B!}{(B - C)!}}{C!} = \frac{B!}{(B - C)! C!}$
108	104 107	breqtrd	$⊢ (φ \land C \in (0 \dots A)) \to \frac{\frac{A!}{(A - C)!}}{C!} \leq \frac{B!}{(B - C)! C!}$
109	35 108	eqbrtrd	$⊢ (φ \land C \in (0 \dots A)) \to \frac{A!}{(A - C)! C!} \leq \frac{B!}{(B - C)! C!}$
110	2	nn0zd	$⊢ φ \to B \in ℤ$
111	110	adantr	$⊢ (φ \land C \in (0 \dots A)) \to B \in ℤ$
112		elfzle1	$⊢ C \in (0 \dots A) \to 0 \leq C$
113	112	adantl	$⊢ (φ \land C \in (0 \dots A)) \to 0 \leq C$
114	1	nn0red	$⊢ φ \to A \in ℝ$
115	114	adantr	$⊢ (φ \land C \in (0 \dots A)) \to A \in ℝ$
116	111	zred	$⊢ (φ \land C \in (0 \dots A)) \to B \in ℝ$
117	13 115 116 17 45	letrd	$⊢ (φ \land C \in (0 \dots A)) \to C \leq B$
118	97 111 11 113 117	elfzd	$⊢ (φ \land C \in (0 \dots A)) \to C \in (0 \dots B)$
119		bcval2	$⊢ C \in (0 \dots B) \to (\binom{B}{C}) = \frac{B!}{(B - C)! C!}$
120	118 119	syl	$⊢ (φ \land C \in (0 \dots A)) \to (\binom{B}{C}) = \frac{B!}{(B - C)! C!}$
121	120	eqcomd	$⊢ (φ \land C \in (0 \dots A)) \to \frac{B!}{(B - C)! C!} = (\binom{B}{C})$
122	109 121	breqtrd	$⊢ (φ \land C \in (0 \dots A)) \to \frac{A!}{(A - C)! C!} \leq (\binom{B}{C})$
123	6 122	eqbrtrd	$⊢ (φ \land C \in (0 \dots A)) \to (\binom{A}{C}) \leq (\binom{B}{C})$
124	1	adantr	$⊢ (φ \land \neg C \in (0 \dots A)) \to A \in ℕ_{0}$
125	3	adantr	$⊢ (φ \land \neg C \in (0 \dots A)) \to C \in ℤ$
126		simpr	$⊢ (φ \land \neg C \in (0 \dots A)) \to \neg C \in (0 \dots A)$
127		bcval3	$⊢ (A \in ℕ_{0} \land C \in ℤ \land \neg C \in (0 \dots A)) \to (\binom{A}{C}) = 0$
128	124 125 126 127	syl3anc	$⊢ (φ \land \neg C \in (0 \dots A)) \to (\binom{A}{C}) = 0$
129		bccl2	$⊢ C \in (0 \dots B) \to (\binom{B}{C}) \in ℕ$
130	129	adantl	$⊢ ((φ \land \neg C \in (0 \dots A)) \land C \in (0 \dots B)) \to (\binom{B}{C}) \in ℕ$
131	130	nnnn0d	$⊢ ((φ \land \neg C \in (0 \dots A)) \land C \in (0 \dots B)) \to (\binom{B}{C}) \in ℕ_{0}$
132	131	nn0ge0d	$⊢ ((φ \land \neg C \in (0 \dots A)) \land C \in (0 \dots B)) \to 0 \leq (\binom{B}{C})$
133		0le0	$⊢ 0 \leq 0$
134	133	a1i	$⊢ ((φ \land \neg C \in (0 \dots A)) \land \neg C \in (0 \dots B)) \to 0 \leq 0$
135	2	ad2antrr	$⊢ ((φ \land \neg C \in (0 \dots A)) \land \neg C \in (0 \dots B)) \to B \in ℕ_{0}$
136	125	adantr	$⊢ ((φ \land \neg C \in (0 \dots A)) \land \neg C \in (0 \dots B)) \to C \in ℤ$
137		simpr	$⊢ ((φ \land \neg C \in (0 \dots A)) \land \neg C \in (0 \dots B)) \to \neg C \in (0 \dots B)$
138		bcval3	$⊢ (B \in ℕ_{0} \land C \in ℤ \land \neg C \in (0 \dots B)) \to (\binom{B}{C}) = 0$
139	135 136 137 138	syl3anc	$⊢ ((φ \land \neg C \in (0 \dots A)) \land \neg C \in (0 \dots B)) \to (\binom{B}{C}) = 0$
140	139	eqcomd	$⊢ ((φ \land \neg C \in (0 \dots A)) \land \neg C \in (0 \dots B)) \to 0 = (\binom{B}{C})$
141	134 140	breqtrd	$⊢ ((φ \land \neg C \in (0 \dots A)) \land \neg C \in (0 \dots B)) \to 0 \leq (\binom{B}{C})$
142	132 141	pm2.61dan	$⊢ (φ \land \neg C \in (0 \dots A)) \to 0 \leq (\binom{B}{C})$
143	128 142	eqbrtrd	$⊢ (φ \land \neg C \in (0 \dots A)) \to (\binom{A}{C}) \leq (\binom{B}{C})$
144	123 143	pm2.61dan	$⊢ φ \to (\binom{A}{C}) \leq (\binom{B}{C})$

Metamath Proof Explorer

Theorem bcled

Proof