Theorem bcle2d

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

	Ref	Expression
Hypotheses	bcle2d.1	|- ( ph -> A e. NN0 )
	bcle2d.2	|- ( ph -> B e. NN0 )
	bcle2d.3	|- ( ph -> C e. NN0 )
	bcle2d.4	|- ( ph -> D e. ZZ )
	bcle2d.5	|- ( ph -> A <_ B )
	bcle2d.6	|- ( ph -> D <_ C )
Assertion	bcle2d	|- ( ph -> ( ( A + C ) _C ( A + D ) ) <_ ( ( B + C ) _C ( B + D ) ) )

Proof

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