bcle2d

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

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

Proof

Step	Hyp	Ref	Expression
1		bcle2d.1	$⊢ φ \to A \in ℕ_{0}$
2		bcle2d.2	$⊢ φ \to B \in ℕ_{0}$
3		bcle2d.3	$⊢ φ \to C \in ℕ_{0}$
4		bcle2d.4	$⊢ φ \to D \in ℤ$
5		bcle2d.5	$⊢ φ \to A \leq B$
6		bcle2d.6	$⊢ φ \to D \leq C$
7		bcval2	$⊢ A + D \in (0 \dots A + C) \to (\binom{A + C}{A + D}) = \frac{(A + C)!}{(A + C - (A + D))! (A + D)!}$
8	7	adantl	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (\binom{A + C}{A + D}) = \frac{(A + C)!}{(A + C - (A + D))! (A + D)!}$
9	1 3	nn0addcld	$⊢ φ \to A + C \in ℕ_{0}$
10	9	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + C \in ℕ_{0}$
11	10	faccld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C)! \in ℕ$
12	11	nncnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C)! \in ℂ$
13	1	nn0zd	$⊢ φ \to A \in ℤ$
14	13 4	zaddcld	$⊢ φ \to A + D \in ℤ$
15		elfzle1	$⊢ A + D \in (0 \dots A + C) \to 0 \leq A + D$
16	14 15	anim12i	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + D \in ℤ \land 0 \leq A + D)$
17		elnn0z	$⊢ A + D \in ℕ_{0} \leftrightarrow (A + D \in ℤ \land 0 \leq A + D)$
18	16 17	sylibr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + D \in ℕ_{0}$
19	18	faccld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + D)! \in ℕ$
20	19	nnnn0d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + D)! \in ℕ_{0}$
21	20	nn0cnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + D)! \in ℂ$
22	1	nn0red	$⊢ φ \to A \in ℝ$
23	22	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A \in ℝ$
24	23	recnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A \in ℂ$
25	3	nn0cnd	$⊢ φ \to C \in ℂ$
26	25	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C \in ℂ$
27	4	zred	$⊢ φ \to D \in ℝ$
28	27	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to D \in ℝ$
29	28	recnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to D \in ℂ$
30	24 26 24 29	addsub4d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + C - (A + D) = (A - A) + C - D$
31	24	subidd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A - A = 0$
32	31	oveq1d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - A) + C - D = 0 + C - D$
33	26 29	subcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D \in ℂ$
34	33	addlidd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to 0 + C - D = C - D$
35	32 34	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - A) + C - D = C - D$
36	30 35	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + C - (A + D) = C - D$
37	3	nn0zd	$⊢ φ \to C \in ℤ$
38	37	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C \in ℤ$
39	4	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to D \in ℤ$
40	38 39	zsubcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D \in ℤ$
41	6	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to D \leq C$
42	38	zred	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C \in ℝ$
43	42 28	subge0d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (0 \leq C - D \leftrightarrow D \leq C)$
44	41 43	mpbird	$⊢ (φ \land A + D \in (0 \dots A + C)) \to 0 \leq C - D$
45	40 44	jca	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (C - D \in ℤ \land 0 \leq C - D)$
46		elnn0z	$⊢ C - D \in ℕ_{0} \leftrightarrow (C - D \in ℤ \land 0 \leq C - D)$
47	45 46	sylibr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D \in ℕ_{0}$
48	36 47	eqeltrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + C - (A + D) \in ℕ_{0}$
49	48	faccld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C - (A + D))! \in ℕ$
50	49	nnnn0d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C - (A + D))! \in ℕ_{0}$
51	50	nn0cnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C - (A + D))! \in ℂ$
52	19	nnne0d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + D)! \neq 0$
53	49	nnne0d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C - (A + D))! \neq 0$
54	12 21 51 52 53	divdiv1d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{\frac{(A + C)!}{(A + D)!}}{(A + C - (A + D))!} = \frac{(A + C)!}{(A + D)! (A + C - (A + D))!}$
55	54	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + D)! (A + C - (A + D))!} = \frac{\frac{(A + C)!}{(A + D)!}}{(A + C - (A + D))!}$
56		0zd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to 0 \in ℤ$
57	10	nn0zd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + C \in ℤ$
58	28	renegcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to - D \in ℝ$
59	3	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C \in ℕ_{0}$
60	59	nn0red	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C \in ℝ$
61		df-neg	$⊢ - D = 0 - D$
62	61	a1i	$⊢ (φ \land A + D \in (0 \dots A + C)) \to - D = 0 - D$
63	15	adantl	$⊢ (φ \land A + D \in (0 \dots A + C)) \to 0 \leq A + D$
64		0red	$⊢ (φ \land A + D \in (0 \dots A + C)) \to 0 \in ℝ$
65	64 28 23	lesubaddd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (0 - D \leq A \leftrightarrow 0 \leq A + D)$
66	63 65	mpbird	$⊢ (φ \land A + D \in (0 \dots A + C)) \to 0 - D \leq A$
67	62 66	eqbrtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to - D \leq A$
68	58 23 60 67	leadd2dd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C + (- D) \leq C + A$
69	26 29	negsubd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C + (- D) = C - D$
70	26 24	addcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C + A = A + C$
71	68 69 70	3brtr3d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D \leq A + C$
72	56 57 40 44 71	elfzd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D \in (0 \dots A + C)$
73		fallfacval4	$⊢ C - D \in (0 \dots A + C) \to {(A + C)}^{\underline{(C - D)}} = \frac{(A + C)!}{(A + C - (C - D))!}$
74	72 73	syl	$⊢ (φ \land A + D \in (0 \dots A + C)) \to {(A + C)}^{\underline{(C - D)}} = \frac{(A + C)!}{(A + C - (C - D))!}$
75	9	nn0cnd	$⊢ φ \to A + C \in ℂ$
76	27	recnd	$⊢ φ \to D \in ℂ$
77	75 25 76	subsubd	$⊢ φ \to A + C - (C - D) = (A + C) - C + D$
78	22	recnd	$⊢ φ \to A \in ℂ$
79	78 25	pncand	$⊢ φ \to A + C - C = A$
80	79	oveq1d	$⊢ φ \to (A + C) - C + D = A + D$
81	77 80	eqtrd	$⊢ φ \to A + C - (C - D) = A + D$
82	81	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + C - (C - D) = A + D$
83	82	fveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C - (C - D))! = (A + D)!$
84	83	oveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + C - (C - D))!} = \frac{(A + C)!}{(A + D)!}$
85	74 84	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to {(A + C)}^{\underline{(C - D)}} = \frac{(A + C)!}{(A + D)!}$
86	85	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + D)!} = {(A + C)}^{\underline{(C - D)}}$
87		nfv	$⊢ Ⅎ k (φ \land A + D \in (0 \dots A + C))$
88		fzfid	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (0 \dots C - D - 1) \in Fin$
89	23	adantr	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to A \in ℝ$
90	3	nn0red	$⊢ φ \to C \in ℝ$
91	90	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C \in ℝ$
92	91	adantr	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to C \in ℝ$
93	89 92	readdcld	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to A + C \in ℝ$
94		elfzelz	$⊢ k \in (0 \dots C - D - 1) \to k \in ℤ$
95	94	zred	$⊢ k \in (0 \dots C - D - 1) \to k \in ℝ$
96	95	adantl	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to k \in ℝ$
97	93 96	resubcld	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to A + C - k \in ℝ$
98		0red	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to 0 \in ℝ$
99	98 96	readdcld	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to 0 + k \in ℝ$
100	28	adantr	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to D \in ℝ$
101	92 100	resubcld	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to C - D \in ℝ$
102		1red	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to 1 \in ℝ$
103	101 102	resubcld	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to C - D - 1 \in ℝ$
104	96	recnd	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to k \in ℂ$
105	104	addlidd	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to 0 + k = k$
106		elfzle2	$⊢ k \in (0 \dots C - D - 1) \to k \leq C - D - 1$
107	106	adantl	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to k \leq C - D - 1$
108	105 107	eqbrtrd	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to 0 + k \leq C - D - 1$
109	101	lem1d	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to C - D - 1 \leq C - D$
110	71	adantr	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to C - D \leq A + C$
111	103 101 93 109 110	letrd	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to C - D - 1 \leq A + C$
112	99 103 93 108 111	letrd	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to 0 + k \leq A + C$
113	64	adantr	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to 0 \in ℝ$
114		leaddsub	$⊢ (0 \in ℝ \land k \in ℝ \land A + C \in ℝ) \to (0 + k \leq A + C \leftrightarrow 0 \leq A + C - k)$
115	113 96 93 114	syl3anc	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to (0 + k \leq A + C \leftrightarrow 0 \leq A + C - k)$
116	112 115	mpbid	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to 0 \leq A + C - k$
117	2	nn0red	$⊢ φ \to B \in ℝ$
118	117	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B \in ℝ$
119	118	adantr	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to B \in ℝ$
120	119 92	readdcld	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to B + C \in ℝ$
121	120 96	resubcld	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to B + C - k \in ℝ$
122	5	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A \leq B$
123	122	adantr	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to A \leq B$
124	89 119 92 123	leadd1dd	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to A + C \leq B + C$
125	93 120 96 124	lesub1dd	$⊢ ((φ \land A + D \in (0 \dots A + C)) \land k \in (0 \dots C - D - 1)) \to A + C - k \leq B + C - k$
126	87 88 97 116 121 125	fprodle	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \prod_{k = 0}^{C - D - 1} (A + C - k) \leq \prod_{k = 0}^{C - D - 1} (B + C - k)$
127	75	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + C \in ℂ$
128		fallfacval	$⊢ (A + C \in ℂ \land C - D \in ℕ_{0}) \to {(A + C)}^{\underline{(C - D)}} = \prod_{k = 0}^{C - D - 1} (A + C - k)$
129	127 47 128	syl2anc	$⊢ (φ \land A + D \in (0 \dots A + C)) \to {(A + C)}^{\underline{(C - D)}} = \prod_{k = 0}^{C - D - 1} (A + C - k)$
130	129	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \prod_{k = 0}^{C - D - 1} (A + C - k) = {(A + C)}^{\underline{(C - D)}}$
131	118	recnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B \in ℂ$
132	131 26	addcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C \in ℂ$
133		fallfacval	$⊢ (B + C \in ℂ \land C - D \in ℕ_{0}) \to {(B + C)}^{\underline{(C - D)}} = \prod_{k = 0}^{C - D - 1} (B + C - k)$
134	132 47 133	syl2anc	$⊢ (φ \land A + D \in (0 \dots A + C)) \to {(B + C)}^{\underline{(C - D)}} = \prod_{k = 0}^{C - D - 1} (B + C - k)$
135	134	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \prod_{k = 0}^{C - D - 1} (B + C - k) = {(B + C)}^{\underline{(C - D)}}$
136	126 130 135	3brtr3d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to {(A + C)}^{\underline{(C - D)}} \leq {(B + C)}^{\underline{(C - D)}}$
137	2	nn0zd	$⊢ φ \to B \in ℤ$
138	137 37	zaddcld	$⊢ φ \to B + C \in ℤ$
139	138	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C \in ℤ$
140	23 28	readdcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + D \in ℝ$
141	137 4	zaddcld	$⊢ φ \to B + D \in ℤ$
142	141	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D \in ℤ$
143	142	zred	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D \in ℝ$
144	23 118 28 122	leadd1dd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + D \leq B + D$
145	64 140 143 63 144	letrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to 0 \leq B + D$
146	64 28 118	lesubaddd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (0 - D \leq B \leftrightarrow 0 \leq B + D)$
147	145 146	mpbird	$⊢ (φ \land A + D \in (0 \dots A + C)) \to 0 - D \leq B$
148	62 147	eqbrtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to - D \leq B$
149	58 118 60 148	leadd2dd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C + (- D) \leq C + B$
150	26 131	addcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C + B = B + C$
151	149 69 150	3brtr3d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D \leq B + C$
152	56 139 40 44 151	elfzd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D \in (0 \dots B + C)$
153		fallfacval4	$⊢ C - D \in (0 \dots B + C) \to {(B + C)}^{\underline{(C - D)}} = \frac{(B + C)!}{(B + C - (C - D))!}$
154	152 153	syl	$⊢ (φ \land A + D \in (0 \dots A + C)) \to {(B + C)}^{\underline{(C - D)}} = \frac{(B + C)!}{(B + C - (C - D))!}$
155	132 26 29	subsubd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C - (C - D) = (B + C) - C + D$
156	131 26	pncand	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C - C = B$
157	156	oveq1d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C) - C + D = B + D$
158	155 157	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C - (C - D) = B + D$
159	158	fveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C - (C - D))! = (B + D)!$
160	159	oveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(B + C)!}{(B + C - (C - D))!} = \frac{(B + C)!}{(B + D)!}$
161	154 160	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to {(B + C)}^{\underline{(C - D)}} = \frac{(B + C)!}{(B + D)!}$
162	136 161	breqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to {(A + C)}^{\underline{(C - D)}} \leq \frac{(B + C)!}{(B + D)!}$
163	86 162	eqbrtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + D)!} \leq \frac{(B + C)!}{(B + D)!}$
164	11	nnred	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C)! \in ℝ$
165	19	nnred	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + D)! \in ℝ$
166	164 165 52	redivcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + D)!} \in ℝ$
167	2	adantr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B \in ℕ_{0}$
168	167 59	nn0addcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C \in ℕ_{0}$
169	168	faccld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C)! \in ℕ$
170	169	nnred	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C)! \in ℝ$
171	142 145	jca	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + D \in ℤ \land 0 \leq B + D)$
172		elnn0z	$⊢ B + D \in ℕ_{0} \leftrightarrow (B + D \in ℤ \land 0 \leq B + D)$
173	171 172	sylibr	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D \in ℕ_{0}$
174	173	faccld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + D)! \in ℕ$
175	174	nnred	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + D)! \in ℝ$
176	174	nnne0d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + D)! \neq 0$
177	170 175 176	redivcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(B + C)!}{(B + D)!} \in ℝ$
178	35	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D = (A - A) + C - D$
179	30	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - A) + C - D = A + C - (A + D)$
180	178 179	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D = A + C - (A + D)$
181	180	fveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (C - D)! = (A + C - (A + D))!$
182	181 49	eqeltrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (C - D)! \in ℕ$
183	182	nnrpd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (C - D)! \in ℝ^{+}$
184	166 177 183	lediv1d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (\frac{(A + C)!}{(A + D)!} \leq \frac{(B + C)!}{(B + D)!} \leftrightarrow \frac{\frac{(A + C)!}{(A + D)!}}{(C - D)!} \leq \frac{\frac{(B + C)!}{(B + D)!}}{(C - D)!})$
185	163 184	mpbid	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{\frac{(A + C)!}{(A + D)!}}{(C - D)!} \leq \frac{\frac{(B + C)!}{(B + D)!}}{(C - D)!}$
186	181	oveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{\frac{(A + C)!}{(A + D)!}}{(C - D)!} = \frac{\frac{(A + C)!}{(A + D)!}}{(A + C - (A + D))!}$
187	131 26	pncan2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C - B = C$
188	187	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C = B + C - B$
189	188	oveq1d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D = (B + C) - B - D$
190	132 131 29	subsub4d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C) - B - D = B + C - (B + D)$
191	189 190	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to C - D = B + C - (B + D)$
192	191	fveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (C - D)! = (B + C - (B + D))!$
193	192	oveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{\frac{(B + C)!}{(B + D)!}}{(C - D)!} = \frac{\frac{(B + C)!}{(B + D)!}}{(B + C - (B + D))!}$
194	185 186 193	3brtr3d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{\frac{(A + C)!}{(A + D)!}}{(A + C - (A + D))!} \leq \frac{\frac{(B + C)!}{(B + D)!}}{(B + C - (B + D))!}$
195	169	nncnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C)! \in ℂ$
196	174	nncnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + D)! \in ℂ$
197	131 26 29	pnpcand	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C - (B + D) = C - D$
198	197 47	eqeltrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C - (B + D) \in ℕ_{0}$
199	198	faccld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C - (B + D))! \in ℕ$
200	199	nncnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C - (B + D))! \in ℂ$
201	199	nnne0d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + C - (B + D))! \neq 0$
202	195 196 200 176 201	divdiv1d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{\frac{(B + C)!}{(B + D)!}}{(B + C - (B + D))!} = \frac{(B + C)!}{(B + D)! (B + C - (B + D))!}$
203	194 202	breqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{\frac{(A + C)!}{(A + D)!}}{(A + C - (A + D))!} \leq \frac{(B + C)!}{(B + D)! (B + C - (B + D))!}$
204	55 203	eqbrtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + D)! (A + C - (A + D))!} \leq \frac{(B + C)!}{(B + D)! (B + C - (B + D))!}$
205	19	nncnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + D)! \in ℂ$
206	49	nncnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + C - (A + D))! \in ℂ$
207	205 206	mulcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A + D)! (A + C - (A + D))! = (A + C - (A + D))! (A + D)!$
208	207	oveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + D)! (A + C - (A + D))!} = \frac{(A + C)!}{(A + C - (A + D))! (A + D)!}$
209	196 200	mulcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + D)! (B + C - (B + D))! = (B + C - (B + D))! (B + D)!$
210	209	oveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(B + C)!}{(B + D)! (B + C - (B + D))!} = \frac{(B + C)!}{(B + C - (B + D))! (B + D)!}$
211	204 208 210	3brtr3d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + C - (A + D))! (A + D)!} \leq \frac{(B + C)!}{(B + C - (B + D))! (B + D)!}$
212		elfzle2	$⊢ A + D \in (0 \dots A + C) \to A + D \leq A + C$
213	212	adantl	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + D \leq A + C$
214	131 29	addcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D = D + B$
215	214	oveq1d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D + (A - B) = D + B + (A - B)$
216	29 131	addcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to D + B \in ℂ$
217	23 118	resubcld	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A - B \in ℝ$
218	217	recnd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A - B \in ℂ$
219	216 218	addcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to D + B + (A - B) = (A - B) + D + B$
220	215 219	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D + (A - B) = (A - B) + D + B$
221	218 29 131	addassd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - B) + D + B = (A - B) + D + B$
222	221	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - B) + D + B = (A - B) + D + B$
223	220 222	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D + (A - B) = (A - B) + D + B$
224	24 131 29	nppcand	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - B) + D + B = A + D$
225	223 224	eqtr2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + D = B + D + (A - B)$
226	132 218	addcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C + (A - B) = (A - B) + B + C$
227	131 26	addcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C = C + B$
228	227	oveq2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - B) + B + C = (A - B) + C + B$
229	226 228	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C + (A - B) = (A - B) + C + B$
230	218 26 131	addassd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - B) + C + B = (A - B) + C + B$
231	230	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - B) + C + B = (A - B) + C + B$
232	229 231	eqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C + (A - B) = (A - B) + C + B$
233	24 131 26	nppcand	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (A - B) + C + B = A + C$
234	232 233	eqtr2d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to A + C = B + C + (A - B)$
235	213 225 234	3brtr3d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D + (A - B) \leq B + C + (A - B)$
236	139	zred	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + C \in ℝ$
237	143 236 217	leadd1d	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (B + D \leq B + C \leftrightarrow B + D + (A - B) \leq B + C + (A - B))$
238	235 237	mpbird	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D \leq B + C$
239	56 139 142 145 238	elfzd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to B + D \in (0 \dots B + C)$
240		bcval2	$⊢ B + D \in (0 \dots B + C) \to (\binom{B + C}{B + D}) = \frac{(B + C)!}{(B + C - (B + D))! (B + D)!}$
241	239 240	syl	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (\binom{B + C}{B + D}) = \frac{(B + C)!}{(B + C - (B + D))! (B + D)!}$
242	241	eqcomd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(B + C)!}{(B + C - (B + D))! (B + D)!} = (\binom{B + C}{B + D})$
243	211 242	breqtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to \frac{(A + C)!}{(A + C - (A + D))! (A + D)!} \leq (\binom{B + C}{B + D})$
244	8 243	eqbrtrd	$⊢ (φ \land A + D \in (0 \dots A + C)) \to (\binom{A + C}{A + D}) \leq (\binom{B + C}{B + D})$
245	9	adantr	$⊢ (φ \land \neg A + D \in (0 \dots A + C)) \to A + C \in ℕ_{0}$
246	14	adantr	$⊢ (φ \land \neg A + D \in (0 \dots A + C)) \to A + D \in ℤ$
247		simpr	$⊢ (φ \land \neg A + D \in (0 \dots A + C)) \to \neg A + D \in (0 \dots A + C)$
248		bcval3	$⊢ (A + C \in ℕ_{0} \land A + D \in ℤ \land \neg A + D \in (0 \dots A + C)) \to (\binom{A + C}{A + D}) = 0$
249	245 246 247 248	syl3anc	$⊢ (φ \land \neg A + D \in (0 \dots A + C)) \to (\binom{A + C}{A + D}) = 0$
250		bccl2	$⊢ B + D \in (0 \dots B + C) \to (\binom{B + C}{B + D}) \in ℕ$
251	250	adantl	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land B + D \in (0 \dots B + C)) \to (\binom{B + C}{B + D}) \in ℕ$
252	251	nnnn0d	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land B + D \in (0 \dots B + C)) \to (\binom{B + C}{B + D}) \in ℕ_{0}$
253	252	nn0ge0d	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land B + D \in (0 \dots B + C)) \to 0 \leq (\binom{B + C}{B + D})$
254		0le0	$⊢ 0 \leq 0$
255	254	a1i	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to 0 \leq 0$
256	2	ad2antrr	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to B \in ℕ_{0}$
257	3	ad2antrr	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to C \in ℕ_{0}$
258	256 257	nn0addcld	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to B + C \in ℕ_{0}$
259	141	adantr	$⊢ (φ \land \neg A + D \in (0 \dots A + C)) \to B + D \in ℤ$
260	259	adantr	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to B + D \in ℤ$
261		simpr	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to \neg B + D \in (0 \dots B + C)$
262		bcval3	$⊢ (B + C \in ℕ_{0} \land B + D \in ℤ \land \neg B + D \in (0 \dots B + C)) \to (\binom{B + C}{B + D}) = 0$
263	258 260 261 262	syl3anc	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to (\binom{B + C}{B + D}) = 0$
264	263	eqcomd	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to 0 = (\binom{B + C}{B + D})$
265	255 264	breqtrd	$⊢ ((φ \land \neg A + D \in (0 \dots A + C)) \land \neg B + D \in (0 \dots B + C)) \to 0 \leq (\binom{B + C}{B + D})$
266	253 265	pm2.61dan	$⊢ (φ \land \neg A + D \in (0 \dots A + C)) \to 0 \leq (\binom{B + C}{B + D})$
267	249 266	eqbrtrd	$⊢ (φ \land \neg A + D \in (0 \dots A + C)) \to (\binom{A + C}{A + D}) \leq (\binom{B + C}{B + D})$
268	244 267	pm2.61dan	$⊢ φ \to (\binom{A + C}{A + D}) \leq (\binom{B + C}{B + D})$

Metamath Proof Explorer

Theorem bcle2d

Proof