itg2cnlem2 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > itg2cnlem2		Structured version Unicode version

Theorem itg2cnlem2 21140

Description: Lemma for itgcn 21220. (Contributed by Mario Carneiro, 31-Aug-2014.)

**Hypotheses**
Ref	Expression
itg2cn.1
itg2cn.2	MblFn
itg2cn.3
itg2cn.4
itg2cn.5
itg2cn.6

**Assertion**
Ref	Expression
itg2cnlem2

Distinct variable groups:

Allowed substitution hint:

(

)

**Proof of Theorem itg2cnlem2**
Step	Hyp	Ref	Expression
1		itg2cn.4	. . . 4
2	1	rphalfcld 11035	. . 3
3		itg2cn.5	. . . 4
4	3	nnrpd 11022	. . 3
5	2, 4	rpdivcld 11040	. 2
6		simprl 750	. . . . . . . 8 $/\$ $/\$
7		itg2cn.2	. . . . . . . . . 10 MblFn
8	7	adantr 462	. . . . . . . . 9 $/\$ $/\$ MblFn
9		itg2cn.1	. . . . . . . . . . 11
10		0re 9382	. . . . . . . . . . . 12
11		pnfxr 11088	. . . . . . . . . . . 12
12		icossre 11372	. . . . . . . . . . . 12 $/\$
13	10, 11, 12	mp2an 667	. . . . . . . . . . 11
14		fss 5564	. . . . . . . . . . 11 $/\$
15	9, 13, 14	sylancl 657	. . . . . . . . . 10
16	15	adantr 462	. . . . . . . . 9 $/\$ $/\$
17		mbfima 21010	. . . . . . . . 9 MblFn $/\$
18	8, 16, 17	syl2anc 656	. . . . . . . 8 $/\$ $/\$
19		inmbl 20923	. . . . . . . 8 $/\$
20	6, 18, 19	syl2anc 656	. . . . . . 7 $/\$ $/\$
21		difmbl 20924	. . . . . . . 8 $/\$ $\$
22	6, 18, 21	syl2anc 656	. . . . . . 7 $/\$ $/\$ $\$
23		inass 3557	. . . . . . . . . . 11 $\$ $\$
24		disjdif 3748	. . . . . . . . . . . 12 $\$
25	24	ineq2i 3546	. . . . . . . . . . 11 $\$
26		in0 3660	. . . . . . . . . . 11
27	23, 25, 26	3eqtri 2465	. . . . . . . . . 10 $\$
28	27	fveq2i 5691	. . . . . . . . 9 $\$
29		ovol0 20876	. . . . . . . . 9
30	28, 29	eqtri 2461	. . . . . . . 8 $\$
31	30	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
32		inundif 3754	. . . . . . . . 9 $\$
33	32	eqcomi 2445	. . . . . . . 8 $\$
34	33	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
35		mblss 20914	. . . . . . . . . 10
36	6, 35	syl 16	. . . . . . . . 9 $/\$ $/\$
37	36	sselda 3353	. . . . . . . 8 $/\$ $/\$ $/\$
38	9	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$
39	38	ffvelrnda 5840	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
40		elrege0 11388	. . . . . . . . . . . 12 $/\$
41	39, 40	sylib 196	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
42	41	simpld 456	. . . . . . . . . 10 $/\$ $/\$ $/\$
43	42	rexrd 9429	. . . . . . . . 9 $/\$ $/\$ $/\$
44	41	simprd 460	. . . . . . . . 9 $/\$ $/\$ $/\$
45		elxrge0 11390	. . . . . . . . 9 $/\$
46	43, 44, 45	sylanbrc 659	. . . . . . . 8 $/\$ $/\$ $/\$
47	37, 46	syldan 467	. . . . . . 7 $/\$ $/\$ $/\$
48		eqid 2441	. . . . . . 7
49		eqid 2441	. . . . . . 7 $\$ $\$
50		eqid 2441	. . . . . . 7
51		0e0iccpnf 11392	. . . . . . . . . 10
52		ifcl 3828	. . . . . . . . . 10 $/\$
53	46, 51, 52	sylancl 657	. . . . . . . . 9 $/\$ $/\$ $/\$
54	53, 48	fmptd 5864	. . . . . . . 8 $/\$ $/\$
55		itg2cn.3	. . . . . . . . 9
56	55	adantr 462	. . . . . . . 8 $/\$ $/\$
57		rexr 9425	. . . . . . . . . . . . 13
58	57	anim1i 565	. . . . . . . . . . . 12 $/\$ $/\$
59		elrege0 11388	. . . . . . . . . . . 12 $/\$
60		elxrge0 11390	. . . . . . . . . . . 12 $/\$
61	58, 59, 60	3imtr4i 266	. . . . . . . . . . 11
62	61	ssriv 3357	. . . . . . . . . 10
63		fss 5564	. . . . . . . . . 10 $/\$
64	38, 62, 63	sylancl 657	. . . . . . . . 9 $/\$ $/\$
65	42	leidd 9902	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
66		breq1 4292	. . . . . . . . . . . . 13
67		breq1 4292	. . . . . . . . . . . . 13
68	66, 67	ifboth 3822	. . . . . . . . . . . 12 $/\$
69	65, 44, 68	syl2anc 656	. . . . . . . . . . 11 $/\$ $/\$ $/\$
70	69	ralrimiva 2797	. . . . . . . . . 10 $/\$ $/\$
71		reex 9369	. . . . . . . . . . . 12
72	71	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
73		eqidd 2442	. . . . . . . . . . 11 $/\$ $/\$
74	38	feqmptd 5741	. . . . . . . . . . 11 $/\$ $/\$
75	72, 53, 42, 73, 74	ofrfval2 6336	. . . . . . . . . 10 $/\$ $/\$
76	70, 75	mpbird 232	. . . . . . . . 9 $/\$ $/\$
77		itg2le 21117	. . . . . . . . 9 $/\$ $/\$
78	54, 64, 76, 77	syl3anc 1213	. . . . . . . 8 $/\$ $/\$
79		itg2lecl 21116	. . . . . . . 8 $/\$ $/\$
80	54, 56, 78, 79	syl3anc 1213	. . . . . . 7 $/\$ $/\$
81		ifcl 3828	. . . . . . . . . 10 $/\$ $\$
82	46, 51, 81	sylancl 657	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
83	82, 49	fmptd 5864	. . . . . . . 8 $/\$ $/\$ $\$
84		breq1 4292	. . . . . . . . . . . . 13 $\$ $\$
85		breq1 4292	. . . . . . . . . . . . 13 $\$ $\$
86	84, 85	ifboth 3822	. . . . . . . . . . . 12 $/\$ $\$
87	65, 44, 86	syl2anc 656	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
88	87	ralrimiva 2797	. . . . . . . . . 10 $/\$ $/\$ $\$
89		eqidd 2442	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
90	72, 82, 42, 89, 74	ofrfval2 6336	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
91	88, 90	mpbird 232	. . . . . . . . 9 $/\$ $/\$ $\$
92		itg2le 21117	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $\$
93	83, 64, 91, 92	syl3anc 1213	. . . . . . . 8 $/\$ $/\$ $\$
94		itg2lecl 21116	. . . . . . . 8 $\$ $/\$ $/\$ $\$ $\$
95	83, 56, 93, 94	syl3anc 1213	. . . . . . 7 $/\$ $/\$ $\$
96	20, 22, 31, 34, 47, 48, 49, 50, 80, 95	itg2split 21127	. . . . . 6 $/\$ $/\$ $\$
97	1	adantr 462	. . . . . . . . 9 $/\$ $/\$
98	97	rphalfcld 11035	. . . . . . . 8 $/\$ $/\$
99	98	rpred 11023	. . . . . . 7 $/\$ $/\$
100		ifcl 3828	. . . . . . . . . . 11 $/\$
101	46, 51, 100	sylancl 657	. . . . . . . . . 10 $/\$ $/\$ $/\$
102		eqid 2441	. . . . . . . . . 10
103	101, 102	fmptd 5864	. . . . . . . . 9 $/\$ $/\$
104		breq1 4292	. . . . . . . . . . . . . 14
105		breq1 4292	. . . . . . . . . . . . . 14
106	104, 105	ifboth 3822	. . . . . . . . . . . . 13 $/\$
107	65, 44, 106	syl2anc 656	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
108	107	ralrimiva 2797	. . . . . . . . . . 11 $/\$ $/\$
109		eqidd 2442	. . . . . . . . . . . 12 $/\$ $/\$
110	72, 101, 46, 109, 74	ofrfval2 6336	. . . . . . . . . . 11 $/\$ $/\$
111	108, 110	mpbird 232	. . . . . . . . . 10 $/\$ $/\$
112		itg2le 21117	. . . . . . . . . 10 $/\$ $/\$
113	103, 64, 111, 112	syl3anc 1213	. . . . . . . . 9 $/\$ $/\$
114		itg2lecl 21116	. . . . . . . . 9 $/\$ $/\$
115	103, 56, 113, 114	syl3anc 1213	. . . . . . . 8 $/\$ $/\$
116	10	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
117		inss2 3568	. . . . . . . . . . . . . 14
118	117	sseli 3349	. . . . . . . . . . . . 13
119	118	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120		ifle 11163	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	42, 116, 44, 119, 120	syl31anc 1216	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122	121	ralrimiva 2797	. . . . . . . . . 10 $/\$ $/\$
123	72, 53, 101, 73, 109	ofrfval2 6336	. . . . . . . . . 10 $/\$ $/\$
124	122, 123	mpbird 232	. . . . . . . . 9 $/\$ $/\$
125		itg2le 21117	. . . . . . . . 9 $/\$ $/\$
126	54, 103, 124, 125	syl3anc 1213	. . . . . . . 8 $/\$ $/\$
127	74	fveq2d 5692	. . . . . . . . . . 11 $/\$ $/\$
128		cmmbl 20916	. . . . . . . . . . . . 13 $\$
129	18, 128	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $\$
130		disjdif 3748	. . . . . . . . . . . . . . 15 $\$
131	130	fveq2i 5691	. . . . . . . . . . . . . 14 $\$
132	131, 29	eqtri 2461	. . . . . . . . . . . . 13 $\$
133	132	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $\$
134		undif2 3752	. . . . . . . . . . . . 13 $\$
135		mblss 20914	. . . . . . . . . . . . . . 15
136	18, 135	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
137		ssequn1 3523	. . . . . . . . . . . . . 14
138	136, 137	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
139	134, 138	syl5req 2486	. . . . . . . . . . . 12 $/\$ $/\$ $\$
140		eqid 2441	. . . . . . . . . . . 12 $\$ $\$
141		iftrue 3794	. . . . . . . . . . . . . 14
142	141	mpteq2ia 4371	. . . . . . . . . . . . 13
143	142	eqcomi 2445	. . . . . . . . . . . 12
144		ifcl 3828	. . . . . . . . . . . . . . 15 $/\$ $\$
145	46, 51, 144	sylancl 657	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
146	145, 140	fmptd 5864	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
147		breq1 4292	. . . . . . . . . . . . . . . . . 18 $\$ $\$
148		breq1 4292	. . . . . . . . . . . . . . . . . 18 $\$ $\$
149	147, 148	ifboth 3822	. . . . . . . . . . . . . . . . 17 $/\$ $\$
150	65, 44, 149	syl2anc 656	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
151	150	ralrimiva 2797	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
152		eqidd 2442	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
153	72, 145, 46, 152, 74	ofrfval2 6336	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
154	151, 153	mpbird 232	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
155		itg2le 21117	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $\$
156	146, 64, 154, 155	syl3anc 1213	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
157		itg2lecl 21116	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $\$
158	146, 56, 156, 157	syl3anc 1213	. . . . . . . . . . . 12 $/\$ $/\$ $\$
159	18, 129, 133, 139, 46, 102, 140, 143, 115, 158	itg2split 21127	. . . . . . . . . . 11 $/\$ $/\$ $\$
160	127, 159	eqtrd 2473	. . . . . . . . . 10 $/\$ $/\$ $\$
161		itg2cn.6	. . . . . . . . . . . . . 14
162	161	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$
163		eldif 3335	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
164	163	baib 891	. . . . . . . . . . . . . . . . . . 19 $\$
165	164	adantl 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$
166		ffn 5556	. . . . . . . . . . . . . . . . . . . . . . 23
167	9, 166	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
168	167	ad2antrr 720	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
169		elpreima 5820	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	168, 169	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
171	42	biantrurd 505	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
172	3	nnred 10333	. . . . . . . . . . . . . . . . . . . . . . . 24
173	172	ad2antrr 720	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
174	173	rexrd 9429	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
175		elioopnf 11379	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
176	174, 175	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
177		simpr 458	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
178	177	biantrurd 505	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
179	171, 176, 178	3bitr2d 281	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
180	173, 42	ltnled 9517	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
181	170, 179, 180	3bitr2rd 282	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
182	181	con1bid 330	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
183	165, 182	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
184	183	ifbid 3808	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
185	184	mpteq2dva 4375	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
186	185	fveq2d 5692	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
187	186	breq1d 4299	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
188	162, 187	mtbird 301	. . . . . . . . . . . 12 $/\$ $/\$ $\$
189	56, 99	resubcld 9772	. . . . . . . . . . . . 13 $/\$ $/\$
190	189, 158	ltnled 9517	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
191	188, 190	mpbird 232	. . . . . . . . . . 11 $/\$ $/\$ $\$
192	56, 99, 158	ltsubadd2d 9933	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
193	191, 192	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $\$
194	160, 193	eqbrtrrd 4311	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
195	115, 99, 158	ltadd1d 9928	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
196	194, 195	mpbird 232	. . . . . . . 8 $/\$ $/\$
197	80, 115, 99, 126, 196	lelttrd 9525	. . . . . . 7 $/\$ $/\$
198	172	adantr 462	. . . . . . . . 9 $/\$ $/\$
199		mblvol 20913	. . . . . . . . . . 11
200	6, 199	syl 16	. . . . . . . . . 10 $/\$ $/\$
201	5	rpred 11023	. . . . . . . . . . . 12
202	201	adantr 462	. . . . . . . . . . 11 $/\$ $/\$
203		simprr 751	. . . . . . . . . . . . 13 $/\$ $/\$
204	200, 203	eqbrtrrd 4311	. . . . . . . . . . . 12 $/\$ $/\$
205		ovolcl 20861	. . . . . . . . . . . . . 14
206	36, 205	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
207	202	rexrd 9429	. . . . . . . . . . . . 13 $/\$ $/\$
208		xrltle 11122	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 656	. . . . . . . . . . . 12 $/\$ $/\$
210	204, 209	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
211		ovollecl 20866	. . . . . . . . . . 11 $/\$ $/\$
212	36, 202, 210, 211	syl3anc 1213	. . . . . . . . . 10 $/\$ $/\$
213	200, 212	eqeltrd 2515	. . . . . . . . 9 $/\$ $/\$
214	198, 213	remulcld 9410	. . . . . . . 8 $/\$ $/\$
215	198	rexrd 9429	. . . . . . . . . . . . . 14 $/\$ $/\$
216	3	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$
217	216	nnnn0d 10632	. . . . . . . . . . . . . . 15 $/\$ $/\$
218	217	nn0ge0d 10635	. . . . . . . . . . . . . 14 $/\$ $/\$
219		elxrge0 11390	. . . . . . . . . . . . . 14 $/\$
220	215, 218, 219	sylanbrc 659	. . . . . . . . . . . . 13 $/\$ $/\$
221		ifcl 3828	. . . . . . . . . . . . 13 $/\$
222	220, 51, 221	sylancl 657	. . . . . . . . . . . 12 $/\$ $/\$
223	222	adantr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
224		eqid 2441	. . . . . . . . . . 11
225	223, 224	fmptd 5864	. . . . . . . . . 10 $/\$ $/\$
226		eldifn 3476	. . . . . . . . . . . . . . . 16 $\$
227	226	adantl 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
228		difssd 3481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
229	228	sselda 3353	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
230	37, 181	syldan 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
231	229, 230	syldan 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
232	231	con1bid 330	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
233	227, 232	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
234		iftrue 3794	. . . . . . . . . . . . . . 15 $\$ $\$
235	234	adantl 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
236		iftrue 3794	. . . . . . . . . . . . . . 15
237	229, 236	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
238	233, 235, 237	3brtr4d 4319	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
239		iffalse 3796	. . . . . . . . . . . . . . 15 $\$ $\$
240	239	adantl 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
241		0le0 10407	. . . . . . . . . . . . . . . 16
242		breq2 4293	. . . . . . . . . . . . . . . . 17
243		breq2 4293	. . . . . . . . . . . . . . . . 17
244	242, 243	ifboth 3822	. . . . . . . . . . . . . . . 16 $/\$
245	218, 241, 244	sylancl 657	. . . . . . . . . . . . . . 15 $/\$ $/\$
246	245	adantr 462	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
247	240, 246	eqbrtrd 4309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
248	238, 247	pm2.61dan 784	. . . . . . . . . . . 12 $/\$ $/\$ $\$
249	248	ralrimivw 2798	. . . . . . . . . . 11 $/\$ $/\$ $\$
250		eqidd 2442	. . . . . . . . . . . 12 $/\$ $/\$
251	72, 82, 223, 89, 250	ofrfval2 6336	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
252	249, 251	mpbird 232	. . . . . . . . . 10 $/\$ $/\$ $\$
253		itg2le 21117	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $\$
254	83, 225, 252, 253	syl3anc 1213	. . . . . . . . 9 $/\$ $/\$ $\$
255		elrege0 11388	. . . . . . . . . . 11 $/\$
256	198, 218, 255	sylanbrc 659	. . . . . . . . . 10 $/\$ $/\$
257		itg2const 21118	. . . . . . . . . 10 $/\$ $/\$
258	6, 213, 256, 257	syl3anc 1213	. . . . . . . . 9 $/\$ $/\$
259	254, 258	breqtrd 4313	. . . . . . . 8 $/\$ $/\$ $\$
260	216	nngt0d 10361	. . . . . . . . . 10 $/\$ $/\$
261		ltmuldiv2 10199	. . . . . . . . . 10 $/\$ $/\$ $/\$
262	213, 99, 198, 260, 261	syl112anc 1217	. . . . . . . . 9 $/\$ $/\$
263	203, 262	mpbird 232	. . . . . . . 8 $/\$ $/\$
264	95, 214, 99, 259, 263	lelttrd 9525	. . . . . . 7 $/\$ $/\$ $\$
265	80, 95, 99, 99, 197, 264	lt2addd 9957	. . . . . 6 $/\$ $/\$ $\$
266	96, 265	eqbrtrd 4309	. . . . 5 $/\$ $/\$
267	97	rpcnd 11025	. . . . . 6 $/\$ $/\$
268	267	2halvesd 10566	. . . . 5 $/\$ $/\$
269	266, 268	breqtrd 4313	. . . 4 $/\$ $/\$
270	269	expr 612	. . 3 $/\$
271	270	ralrimiva 2797	. 2
272		breq2 4293	. . . . 5
273	272	imbi1d 317	. . . 4
274	273	ralbidv 2733	. . 3
275	274	rspcev 3070	. 2 $/\$
276	5, 271, 275	syl2anc 656	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1364

wcel 1761

wral 2713

wrex 2714

cvv 2970 $\$ cdif 3322

cun 3323

cin 3324

wss 3325

c0 3634

cif 3788 class class class wbr 4289

cmpt 4347

ccnv 4835

cdm 4836

cima 4839

wfn 5410

wf 5411

cfv 5415 (class class class)co 6090

cofr 6318

cr 9277

cc0 9278

caddc 9281

cmul 9283

cpnf 9411

cxr 9413

clt 9414

cle 9415

cmin 9591

cdiv 9989

cn 10318

c2 10367

crp 10987

cioo 11296

cico 11298

cicc 11299

covol 20846

cvol 20847 MblFncmbf 20994

citg2 20996

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356 ax-addf 9357

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-fal 1370 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606