itg2cnlem2 - Metamath Proof Explorer

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

Theorem itg2cnlem2 21240

Description: Lemma for itgcn 21320. (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 11039	. . 3
3		itg2cn.5	. . . 4
4	3	nnrpd 11026	. . 3
5	2, 4	rpdivcld 11044	. 2
6		simprl 755	. . . . . . . 8 $/\$ $/\$
7		itg2cn.2	. . . . . . . . . 10 MblFn
8	7	adantr 465	. . . . . . . . 9 $/\$ $/\$ MblFn
9		itg2cn.1	. . . . . . . . . . 11
10		0re 9386	. . . . . . . . . . . 12
11		pnfxr 11092	. . . . . . . . . . . 12
12		icossre 11376	. . . . . . . . . . . 12 $/\$
13	10, 11, 12	mp2an 672	. . . . . . . . . . 11
14		fss 5567	. . . . . . . . . . 11 $/\$
15	9, 13, 14	sylancl 662	. . . . . . . . . 10
16	15	adantr 465	. . . . . . . . 9 $/\$ $/\$
17		mbfima 21110	. . . . . . . . 9 MblFn $/\$
18	8, 16, 17	syl2anc 661	. . . . . . . 8 $/\$ $/\$
19		inmbl 21023	. . . . . . . 8 $/\$
20	6, 18, 19	syl2anc 661	. . . . . . 7 $/\$ $/\$
21		difmbl 21024	. . . . . . . 8 $/\$ $\$
22	6, 18, 21	syl2anc 661	. . . . . . 7 $/\$ $/\$ $\$
23		inass 3560	. . . . . . . . . . 11 $\$ $\$
24		disjdif 3751	. . . . . . . . . . . 12 $\$
25	24	ineq2i 3549	. . . . . . . . . . 11 $\$
26		in0 3663	. . . . . . . . . . 11
27	23, 25, 26	3eqtri 2467	. . . . . . . . . 10 $\$
28	27	fveq2i 5694	. . . . . . . . 9 $\$
29		ovol0 20976	. . . . . . . . 9
30	28, 29	eqtri 2463	. . . . . . . 8 $\$
31	30	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
32		inundif 3757	. . . . . . . . 9 $\$
33	32	eqcomi 2447	. . . . . . . 8 $\$
34	33	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
35		mblss 21014	. . . . . . . . . 10
36	6, 35	syl 16	. . . . . . . . 9 $/\$ $/\$
37	36	sselda 3356	. . . . . . . 8 $/\$ $/\$ $/\$
38	9	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
39	38	ffvelrnda 5843	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
40		elrege0 11392	. . . . . . . . . . . 12 $/\$
41	39, 40	sylib 196	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
42	41	simpld 459	. . . . . . . . . 10 $/\$ $/\$ $/\$
43	42	rexrd 9433	. . . . . . . . 9 $/\$ $/\$ $/\$
44	41	simprd 463	. . . . . . . . 9 $/\$ $/\$ $/\$
45		elxrge0 11394	. . . . . . . . 9 $/\$
46	43, 44, 45	sylanbrc 664	. . . . . . . 8 $/\$ $/\$ $/\$
47	37, 46	syldan 470	. . . . . . 7 $/\$ $/\$ $/\$
48		eqid 2443	. . . . . . 7
49		eqid 2443	. . . . . . 7 $\$ $\$
50		eqid 2443	. . . . . . 7
51		0e0iccpnf 11396	. . . . . . . . . 10
52		ifcl 3831	. . . . . . . . . 10 $/\$
53	46, 51, 52	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$
54	53, 48	fmptd 5867	. . . . . . . 8 $/\$ $/\$
55		itg2cn.3	. . . . . . . . 9
56	55	adantr 465	. . . . . . . 8 $/\$ $/\$
57		rexr 9429	. . . . . . . . . . . . 13
58	57	anim1i 568	. . . . . . . . . . . 12 $/\$ $/\$
59		elrege0 11392	. . . . . . . . . . . 12 $/\$
60		elxrge0 11394	. . . . . . . . . . . 12 $/\$
61	58, 59, 60	3imtr4i 266	. . . . . . . . . . 11
62	61	ssriv 3360	. . . . . . . . . 10
63		fss 5567	. . . . . . . . . 10 $/\$
64	38, 62, 63	sylancl 662	. . . . . . . . 9 $/\$ $/\$
65	42	leidd 9906	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
66		breq1 4295	. . . . . . . . . . . . 13
67		breq1 4295	. . . . . . . . . . . . 13
68	66, 67	ifboth 3825	. . . . . . . . . . . 12 $/\$
69	65, 44, 68	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
70	69	ralrimiva 2799	. . . . . . . . . 10 $/\$ $/\$
71		reex 9373	. . . . . . . . . . . 12
72	71	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
73		eqidd 2444	. . . . . . . . . . 11 $/\$ $/\$
74	38	feqmptd 5744	. . . . . . . . . . 11 $/\$ $/\$
75	72, 53, 42, 73, 74	ofrfval2 6337	. . . . . . . . . 10 $/\$ $/\$
76	70, 75	mpbird 232	. . . . . . . . 9 $/\$ $/\$
77		itg2le 21217	. . . . . . . . 9 $/\$ $/\$
78	54, 64, 76, 77	syl3anc 1218	. . . . . . . 8 $/\$ $/\$
79		itg2lecl 21216	. . . . . . . 8 $/\$ $/\$
80	54, 56, 78, 79	syl3anc 1218	. . . . . . 7 $/\$ $/\$
81		ifcl 3831	. . . . . . . . . 10 $/\$ $\$
82	46, 51, 81	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
83	82, 49	fmptd 5867	. . . . . . . 8 $/\$ $/\$ $\$
84		breq1 4295	. . . . . . . . . . . . 13 $\$ $\$
85		breq1 4295	. . . . . . . . . . . . 13 $\$ $\$
86	84, 85	ifboth 3825	. . . . . . . . . . . 12 $/\$ $\$
87	65, 44, 86	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
88	87	ralrimiva 2799	. . . . . . . . . 10 $/\$ $/\$ $\$
89		eqidd 2444	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
90	72, 82, 42, 89, 74	ofrfval2 6337	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
91	88, 90	mpbird 232	. . . . . . . . 9 $/\$ $/\$ $\$
92		itg2le 21217	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $\$
93	83, 64, 91, 92	syl3anc 1218	. . . . . . . 8 $/\$ $/\$ $\$
94		itg2lecl 21216	. . . . . . . 8 $\$ $/\$ $/\$ $\$ $\$
95	83, 56, 93, 94	syl3anc 1218	. . . . . . 7 $/\$ $/\$ $\$
96	20, 22, 31, 34, 47, 48, 49, 50, 80, 95	itg2split 21227	. . . . . 6 $/\$ $/\$ $\$
97	1	adantr 465	. . . . . . . . 9 $/\$ $/\$
98	97	rphalfcld 11039	. . . . . . . 8 $/\$ $/\$
99	98	rpred 11027	. . . . . . 7 $/\$ $/\$
100		ifcl 3831	. . . . . . . . . . 11 $/\$
101	46, 51, 100	sylancl 662	. . . . . . . . . 10 $/\$ $/\$ $/\$
102		eqid 2443	. . . . . . . . . 10
103	101, 102	fmptd 5867	. . . . . . . . 9 $/\$ $/\$
104		breq1 4295	. . . . . . . . . . . . . 14
105		breq1 4295	. . . . . . . . . . . . . 14
106	104, 105	ifboth 3825	. . . . . . . . . . . . 13 $/\$
107	65, 44, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
108	107	ralrimiva 2799	. . . . . . . . . . 11 $/\$ $/\$
109		eqidd 2444	. . . . . . . . . . . 12 $/\$ $/\$
110	72, 101, 46, 109, 74	ofrfval2 6337	. . . . . . . . . . 11 $/\$ $/\$
111	108, 110	mpbird 232	. . . . . . . . . 10 $/\$ $/\$
112		itg2le 21217	. . . . . . . . . 10 $/\$ $/\$
113	103, 64, 111, 112	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$
114		itg2lecl 21216	. . . . . . . . 9 $/\$ $/\$
115	103, 56, 113, 114	syl3anc 1218	. . . . . . . 8 $/\$ $/\$
116	10	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
117		inss2 3571	. . . . . . . . . . . . . 14
118	117	sseli 3352	. . . . . . . . . . . . 13
119	118	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120		ifle 11167	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	42, 116, 44, 119, 120	syl31anc 1221	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122	121	ralrimiva 2799	. . . . . . . . . 10 $/\$ $/\$
123	72, 53, 101, 73, 109	ofrfval2 6337	. . . . . . . . . 10 $/\$ $/\$
124	122, 123	mpbird 232	. . . . . . . . 9 $/\$ $/\$
125		itg2le 21217	. . . . . . . . 9 $/\$ $/\$
126	54, 103, 124, 125	syl3anc 1218	. . . . . . . 8 $/\$ $/\$
127	74	fveq2d 5695	. . . . . . . . . . 11 $/\$ $/\$
128		cmmbl 21016	. . . . . . . . . . . . 13 $\$
129	18, 128	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $\$
130		disjdif 3751	. . . . . . . . . . . . . . 15 $\$
131	130	fveq2i 5694	. . . . . . . . . . . . . 14 $\$
132	131, 29	eqtri 2463	. . . . . . . . . . . . 13 $\$
133	132	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $\$
134		undif2 3755	. . . . . . . . . . . . 13 $\$
135		mblss 21014	. . . . . . . . . . . . . . 15
136	18, 135	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
137		ssequn1 3526	. . . . . . . . . . . . . 14
138	136, 137	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
139	134, 138	syl5req 2488	. . . . . . . . . . . 12 $/\$ $/\$ $\$
140		eqid 2443	. . . . . . . . . . . 12 $\$ $\$
141		iftrue 3797	. . . . . . . . . . . . . 14
142	141	mpteq2ia 4374	. . . . . . . . . . . . 13
143	142	eqcomi 2447	. . . . . . . . . . . 12
144		ifcl 3831	. . . . . . . . . . . . . . 15 $/\$ $\$
145	46, 51, 144	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
146	145, 140	fmptd 5867	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
147		breq1 4295	. . . . . . . . . . . . . . . . . 18 $\$ $\$
148		breq1 4295	. . . . . . . . . . . . . . . . . 18 $\$ $\$
149	147, 148	ifboth 3825	. . . . . . . . . . . . . . . . 17 $/\$ $\$
150	65, 44, 149	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
151	150	ralrimiva 2799	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
152		eqidd 2444	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
153	72, 145, 46, 152, 74	ofrfval2 6337	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
154	151, 153	mpbird 232	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
155		itg2le 21217	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $\$
156	146, 64, 154, 155	syl3anc 1218	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
157		itg2lecl 21216	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $\$
158	146, 56, 156, 157	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $\$
159	18, 129, 133, 139, 46, 102, 140, 143, 115, 158	itg2split 21227	. . . . . . . . . . 11 $/\$ $/\$ $\$
160	127, 159	eqtrd 2475	. . . . . . . . . 10 $/\$ $/\$ $\$
161		itg2cn.6	. . . . . . . . . . . . . 14
162	161	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
163		eldif 3338	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
164	163	baib 896	. . . . . . . . . . . . . . . . . . 19 $\$
165	164	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$
166		ffn 5559	. . . . . . . . . . . . . . . . . . . . . . 23
167	9, 166	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
168	167	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
169		elpreima 5823	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	168, 169	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
171	42	biantrurd 508	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
172	3	nnred 10337	. . . . . . . . . . . . . . . . . . . . . . . 24
173	172	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
174	173	rexrd 9433	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
175		elioopnf 11383	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
176	174, 175	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
177		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
178	177	biantrurd 508	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
179	171, 176, 178	3bitr2d 281	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
180	173, 42	ltnled 9521	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
181	170, 179, 180	3bitr2rd 282	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
182	181	con1bid 330	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
183	165, 182	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
184	183	ifbid 3811	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
185	184	mpteq2dva 4378	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
186	185	fveq2d 5695	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
187	186	breq1d 4302	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
188	162, 187	mtbird 301	. . . . . . . . . . . 12 $/\$ $/\$ $\$
189	56, 99	resubcld 9776	. . . . . . . . . . . . 13 $/\$ $/\$
190	189, 158	ltnled 9521	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
191	188, 190	mpbird 232	. . . . . . . . . . 11 $/\$ $/\$ $\$
192	56, 99, 158	ltsubadd2d 9937	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
193	191, 192	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $\$
194	160, 193	eqbrtrrd 4314	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
195	115, 99, 158	ltadd1d 9932	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
196	194, 195	mpbird 232	. . . . . . . 8 $/\$ $/\$
197	80, 115, 99, 126, 196	lelttrd 9529	. . . . . . 7 $/\$ $/\$
198	172	adantr 465	. . . . . . . . 9 $/\$ $/\$
199		mblvol 21013	. . . . . . . . . . 11
200	6, 199	syl 16	. . . . . . . . . 10 $/\$ $/\$
201	5	rpred 11027	. . . . . . . . . . . 12
202	201	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
203		simprr 756	. . . . . . . . . . . . 13 $/\$ $/\$
204	200, 203	eqbrtrrd 4314	. . . . . . . . . . . 12 $/\$ $/\$
205		ovolcl 20961	. . . . . . . . . . . . . 14
206	36, 205	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
207	202	rexrd 9433	. . . . . . . . . . . . 13 $/\$ $/\$
208		xrltle 11126	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
210	204, 209	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
211		ovollecl 20966	. . . . . . . . . . 11 $/\$ $/\$
212	36, 202, 210, 211	syl3anc 1218	. . . . . . . . . 10 $/\$ $/\$
213	200, 212	eqeltrd 2517	. . . . . . . . 9 $/\$ $/\$
214	198, 213	remulcld 9414	. . . . . . . 8 $/\$ $/\$
215	198	rexrd 9433	. . . . . . . . . . . . . 14 $/\$ $/\$
216	3	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
217	216	nnnn0d 10636	. . . . . . . . . . . . . . 15 $/\$ $/\$
218	217	nn0ge0d 10639	. . . . . . . . . . . . . 14 $/\$ $/\$
219		elxrge0 11394	. . . . . . . . . . . . . 14 $/\$
220	215, 218, 219	sylanbrc 664	. . . . . . . . . . . . 13 $/\$ $/\$
221		ifcl 3831	. . . . . . . . . . . . 13 $/\$
222	220, 51, 221	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$
223	222	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
224		eqid 2443	. . . . . . . . . . 11
225	223, 224	fmptd 5867	. . . . . . . . . 10 $/\$ $/\$
226		eldifn 3479	. . . . . . . . . . . . . . . 16 $\$
227	226	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
228		difssd 3484	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
229	228	sselda 3356	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
230	37, 181	syldan 470	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
231	229, 230	syldan 470	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
232	231	con1bid 330	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
233	227, 232	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
234		iftrue 3797	. . . . . . . . . . . . . . 15 $\$ $\$
235	234	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
236		iftrue 3797	. . . . . . . . . . . . . . 15
237	229, 236	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
238	233, 235, 237	3brtr4d 4322	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
239		iffalse 3799	. . . . . . . . . . . . . . 15 $\$ $\$
240	239	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
241		0le0 10411	. . . . . . . . . . . . . . . 16
242		breq2 4296	. . . . . . . . . . . . . . . . 17
243		breq2 4296	. . . . . . . . . . . . . . . . 17
244	242, 243	ifboth 3825	. . . . . . . . . . . . . . . 16 $/\$
245	218, 241, 244	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$
246	245	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
247	240, 246	eqbrtrd 4312	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
248	238, 247	pm2.61dan 789	. . . . . . . . . . . 12 $/\$ $/\$ $\$
249	248	ralrimivw 2800	. . . . . . . . . . 11 $/\$ $/\$ $\$
250		eqidd 2444	. . . . . . . . . . . 12 $/\$ $/\$
251	72, 82, 223, 89, 250	ofrfval2 6337	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
252	249, 251	mpbird 232	. . . . . . . . . 10 $/\$ $/\$ $\$
253		itg2le 21217	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $\$
254	83, 225, 252, 253	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$ $\$
255		elrege0 11392	. . . . . . . . . . 11 $/\$
256	198, 218, 255	sylanbrc 664	. . . . . . . . . 10 $/\$ $/\$
257		itg2const 21218	. . . . . . . . . 10 $/\$ $/\$
258	6, 213, 256, 257	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$
259	254, 258	breqtrd 4316	. . . . . . . 8 $/\$ $/\$ $\$
260	216	nngt0d 10365	. . . . . . . . . 10 $/\$ $/\$
261		ltmuldiv2 10203	. . . . . . . . . 10 $/\$ $/\$ $/\$
262	213, 99, 198, 260, 261	syl112anc 1222	. . . . . . . . 9 $/\$ $/\$
263	203, 262	mpbird 232	. . . . . . . 8 $/\$ $/\$
264	95, 214, 99, 259, 263	lelttrd 9529	. . . . . . 7 $/\$ $/\$ $\$
265	80, 95, 99, 99, 197, 264	lt2addd 9961	. . . . . 6 $/\$ $/\$ $\$
266	96, 265	eqbrtrd 4312	. . . . 5 $/\$ $/\$
267	97	rpcnd 11029	. . . . . 6 $/\$ $/\$
268	267	2halvesd 10570	. . . . 5 $/\$ $/\$
269	266, 268	breqtrd 4316	. . . 4 $/\$ $/\$
270	269	expr 615	. . 3 $/\$
271	270	ralrimiva 2799	. 2
272		breq2 4296	. . . . 5
273	272	imbi1d 317	. . . 4
274	273	ralbidv 2735	. . 3
275	274	rspcev 3073	. 2 $/\$
276	5, 271, 275	syl2anc 661	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1369

wcel 1756

wral 2715

wrex 2716

cvv 2972 $\$ cdif 3325

cun 3326

cin 3327

wss 3328

c0 3637

cif 3791 class class class wbr 4292

cmpt 4350

ccnv 4839

cdm 4840

cima 4843

wfn 5413

wf 5414

cfv 5418 (class class class)co 6091

cofr 6319

cr 9281

cc0 9282

caddc 9285

cmul 9287

cpnf 9415

cxr 9417

clt 9418

cle 9419

cmin 9595

cdiv 9993

cn 10322

c2 10371

crp 10991

cioo 11300

cico 11302

cicc 11303

covol 20946

cvol 20947 MblFncmbf 21094

citg2 21096

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-inf2 7847 ax-cnex 9338 ax-resscn 9339 ax-1cn 9340 ax-icn 9341 ax-addcl 9342 ax-addrcl 9343 ax-mulcl 9344 ax-mulrcl 9345 ax-mulcom 9346 ax-addass 9347 ax-mulass 9348 ax-distr 9349 ax-i2m1 9350 ax-1ne0 9351 ax-1rid 9352 ax-rnegex 9353 ax-rrecex 9354 ax-cnre 9355 ax-pre-lttri 9356 ax-pre-lttrn 9357 ax-pre-ltadd 9358 ax-pre-mulgt0 9359 ax-pre-sup 9360 ax-addf 9361

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608