itg2cnlem2 - Metamath Proof Explorer

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

Theorem itg2cnlem2 21932

Description: Lemma for itgcn 22012. (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 11268	. . 3
3		itg2cn.5	. . . 4
4	3	nnrpd 11255	. . 3
5	2, 4	rpdivcld 11273	. 2
6		simprl 755	. . . . . . . 8 $/\$ $/\$
7		itg2cn.2	. . . . . . . . . 10 MblFn
8	7	adantr 465	. . . . . . . . 9 $/\$ $/\$ MblFn
9		itg2cn.1	. . . . . . . . . . 11
10		0re 9596	. . . . . . . . . . . 12
11		pnfxr 11321	. . . . . . . . . . . 12
12		icossre 11605	. . . . . . . . . . . 12 $/\$
13	10, 11, 12	mp2an 672	. . . . . . . . . . 11
14		fss 5739	. . . . . . . . . . 11 $/\$
15	9, 13, 14	sylancl 662	. . . . . . . . . 10
16	15	adantr 465	. . . . . . . . 9 $/\$ $/\$
17		mbfima 21802	. . . . . . . . 9 MblFn $/\$
18	8, 16, 17	syl2anc 661	. . . . . . . 8 $/\$ $/\$
19		inmbl 21715	. . . . . . . 8 $/\$
20	6, 18, 19	syl2anc 661	. . . . . . 7 $/\$ $/\$
21		difmbl 21716	. . . . . . . 8 $/\$ $\$
22	6, 18, 21	syl2anc 661	. . . . . . 7 $/\$ $/\$ $\$
23		inass 3708	. . . . . . . . . . 11 $\$ $\$
24		disjdif 3899	. . . . . . . . . . . 12 $\$
25	24	ineq2i 3697	. . . . . . . . . . 11 $\$
26		in0 3811	. . . . . . . . . . 11
27	23, 25, 26	3eqtri 2500	. . . . . . . . . 10 $\$
28	27	fveq2i 5869	. . . . . . . . 9 $\$
29		ovol0 21667	. . . . . . . . 9
30	28, 29	eqtri 2496	. . . . . . . 8 $\$
31	30	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
32		inundif 3905	. . . . . . . . 9 $\$
33	32	eqcomi 2480	. . . . . . . 8 $\$
34	33	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
35		mblss 21705	. . . . . . . . . 10
36	6, 35	syl 16	. . . . . . . . 9 $/\$ $/\$
37	36	sselda 3504	. . . . . . . 8 $/\$ $/\$ $/\$
38	9	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
39	38	ffvelrnda 6021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
40		elrege0 11627	. . . . . . . . . . . 12 $/\$
41	39, 40	sylib 196	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
42	41	simpld 459	. . . . . . . . . 10 $/\$ $/\$ $/\$
43	42	rexrd 9643	. . . . . . . . 9 $/\$ $/\$ $/\$
44	41	simprd 463	. . . . . . . . 9 $/\$ $/\$ $/\$
45		elxrge0 11629	. . . . . . . . 9 $/\$
46	43, 44, 45	sylanbrc 664	. . . . . . . 8 $/\$ $/\$ $/\$
47	37, 46	syldan 470	. . . . . . 7 $/\$ $/\$ $/\$
48		eqid 2467	. . . . . . 7
49		eqid 2467	. . . . . . 7 $\$ $\$
50		eqid 2467	. . . . . . 7
51		0e0iccpnf 11631	. . . . . . . . . 10
52		ifcl 3981	. . . . . . . . . 10 $/\$
53	46, 51, 52	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$
54	53, 48	fmptd 6045	. . . . . . . 8 $/\$ $/\$
55		itg2cn.3	. . . . . . . . 9
56	55	adantr 465	. . . . . . . 8 $/\$ $/\$
57		rexr 9639	. . . . . . . . . . . . 13
58	57	anim1i 568	. . . . . . . . . . . 12 $/\$ $/\$
59		elrege0 11627	. . . . . . . . . . . 12 $/\$
60		elxrge0 11629	. . . . . . . . . . . 12 $/\$
61	58, 59, 60	3imtr4i 266	. . . . . . . . . . 11
62	61	ssriv 3508	. . . . . . . . . 10
63		fss 5739	. . . . . . . . . 10 $/\$
64	38, 62, 63	sylancl 662	. . . . . . . . 9 $/\$ $/\$
65	42	leidd 10119	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
66		breq1 4450	. . . . . . . . . . . . 13
67		breq1 4450	. . . . . . . . . . . . 13
68	66, 67	ifboth 3975	. . . . . . . . . . . 12 $/\$
69	65, 44, 68	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
70	69	ralrimiva 2878	. . . . . . . . . 10 $/\$ $/\$
71		reex 9583	. . . . . . . . . . . 12
72	71	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
73		eqidd 2468	. . . . . . . . . . 11 $/\$ $/\$
74	38	feqmptd 5920	. . . . . . . . . . 11 $/\$ $/\$
75	72, 53, 42, 73, 74	ofrfval2 6541	. . . . . . . . . 10 $/\$ $/\$
76	70, 75	mpbird 232	. . . . . . . . 9 $/\$ $/\$
77		itg2le 21909	. . . . . . . . 9 $/\$ $/\$
78	54, 64, 76, 77	syl3anc 1228	. . . . . . . 8 $/\$ $/\$
79		itg2lecl 21908	. . . . . . . 8 $/\$ $/\$
80	54, 56, 78, 79	syl3anc 1228	. . . . . . 7 $/\$ $/\$
81		ifcl 3981	. . . . . . . . . 10 $/\$ $\$
82	46, 51, 81	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
83	82, 49	fmptd 6045	. . . . . . . 8 $/\$ $/\$ $\$
84		breq1 4450	. . . . . . . . . . . . 13 $\$ $\$
85		breq1 4450	. . . . . . . . . . . . 13 $\$ $\$
86	84, 85	ifboth 3975	. . . . . . . . . . . 12 $/\$ $\$
87	65, 44, 86	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
88	87	ralrimiva 2878	. . . . . . . . . 10 $/\$ $/\$ $\$
89		eqidd 2468	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
90	72, 82, 42, 89, 74	ofrfval2 6541	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
91	88, 90	mpbird 232	. . . . . . . . 9 $/\$ $/\$ $\$
92		itg2le 21909	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $\$
93	83, 64, 91, 92	syl3anc 1228	. . . . . . . 8 $/\$ $/\$ $\$
94		itg2lecl 21908	. . . . . . . 8 $\$ $/\$ $/\$ $\$ $\$
95	83, 56, 93, 94	syl3anc 1228	. . . . . . 7 $/\$ $/\$ $\$
96	20, 22, 31, 34, 47, 48, 49, 50, 80, 95	itg2split 21919	. . . . . 6 $/\$ $/\$ $\$
97	1	adantr 465	. . . . . . . . 9 $/\$ $/\$
98	97	rphalfcld 11268	. . . . . . . 8 $/\$ $/\$
99	98	rpred 11256	. . . . . . 7 $/\$ $/\$
100		ifcl 3981	. . . . . . . . . . 11 $/\$
101	46, 51, 100	sylancl 662	. . . . . . . . . 10 $/\$ $/\$ $/\$
102		eqid 2467	. . . . . . . . . 10
103	101, 102	fmptd 6045	. . . . . . . . 9 $/\$ $/\$
104		breq1 4450	. . . . . . . . . . . . . 14
105		breq1 4450	. . . . . . . . . . . . . 14
106	104, 105	ifboth 3975	. . . . . . . . . . . . 13 $/\$
107	65, 44, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
108	107	ralrimiva 2878	. . . . . . . . . . 11 $/\$ $/\$
109		eqidd 2468	. . . . . . . . . . . 12 $/\$ $/\$
110	72, 101, 46, 109, 74	ofrfval2 6541	. . . . . . . . . . 11 $/\$ $/\$
111	108, 110	mpbird 232	. . . . . . . . . 10 $/\$ $/\$
112		itg2le 21909	. . . . . . . . . 10 $/\$ $/\$
113	103, 64, 111, 112	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$
114		itg2lecl 21908	. . . . . . . . 9 $/\$ $/\$
115	103, 56, 113, 114	syl3anc 1228	. . . . . . . 8 $/\$ $/\$
116	10	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
117		inss2 3719	. . . . . . . . . . . . . 14
118	117	sseli 3500	. . . . . . . . . . . . 13
119	118	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120		ifle 11396	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	42, 116, 44, 119, 120	syl31anc 1231	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122	121	ralrimiva 2878	. . . . . . . . . 10 $/\$ $/\$
123	72, 53, 101, 73, 109	ofrfval2 6541	. . . . . . . . . 10 $/\$ $/\$
124	122, 123	mpbird 232	. . . . . . . . 9 $/\$ $/\$
125		itg2le 21909	. . . . . . . . 9 $/\$ $/\$
126	54, 103, 124, 125	syl3anc 1228	. . . . . . . 8 $/\$ $/\$
127	74	fveq2d 5870	. . . . . . . . . . 11 $/\$ $/\$
128		cmmbl 21708	. . . . . . . . . . . . 13 $\$
129	18, 128	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $\$
130		disjdif 3899	. . . . . . . . . . . . . . 15 $\$
131	130	fveq2i 5869	. . . . . . . . . . . . . 14 $\$
132	131, 29	eqtri 2496	. . . . . . . . . . . . 13 $\$
133	132	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $\$
134		undif2 3903	. . . . . . . . . . . . 13 $\$
135		mblss 21705	. . . . . . . . . . . . . . 15
136	18, 135	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
137		ssequn1 3674	. . . . . . . . . . . . . 14
138	136, 137	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
139	134, 138	syl5req 2521	. . . . . . . . . . . 12 $/\$ $/\$ $\$
140		eqid 2467	. . . . . . . . . . . 12 $\$ $\$
141		iftrue 3945	. . . . . . . . . . . . . 14
142	141	mpteq2ia 4529	. . . . . . . . . . . . 13
143	142	eqcomi 2480	. . . . . . . . . . . 12
144		ifcl 3981	. . . . . . . . . . . . . . 15 $/\$ $\$
145	46, 51, 144	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
146	145, 140	fmptd 6045	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
147		breq1 4450	. . . . . . . . . . . . . . . . . 18 $\$ $\$
148		breq1 4450	. . . . . . . . . . . . . . . . . 18 $\$ $\$
149	147, 148	ifboth 3975	. . . . . . . . . . . . . . . . 17 $/\$ $\$
150	65, 44, 149	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
151	150	ralrimiva 2878	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
152		eqidd 2468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
153	72, 145, 46, 152, 74	ofrfval2 6541	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
154	151, 153	mpbird 232	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
155		itg2le 21909	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $\$
156	146, 64, 154, 155	syl3anc 1228	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
157		itg2lecl 21908	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $\$
158	146, 56, 156, 157	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $\$
159	18, 129, 133, 139, 46, 102, 140, 143, 115, 158	itg2split 21919	. . . . . . . . . . 11 $/\$ $/\$ $\$
160	127, 159	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$ $\$
161		itg2cn.6	. . . . . . . . . . . . . 14
162	161	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
163		eldif 3486	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
164	163	baib 901	. . . . . . . . . . . . . . . . . . 19 $\$
165	164	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$
166		ffn 5731	. . . . . . . . . . . . . . . . . . . . . . 23
167	9, 166	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
168	167	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
169		elpreima 6001	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	168, 169	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
171	42	biantrurd 508	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
172	3	nnred 10551	. . . . . . . . . . . . . . . . . . . . . . . 24
173	172	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
174	173	rexrd 9643	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
175		elioopnf 11618	. . . . . . . . . . . . . . . . . . . . . 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 9731	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
181	170, 179, 180	3bitr2rd 282	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
182	181	con1bid 330	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
183	165, 182	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
184	183	ifbid 3961	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
185	184	mpteq2dva 4533	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
186	185	fveq2d 5870	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
187	186	breq1d 4457	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
188	162, 187	mtbird 301	. . . . . . . . . . . 12 $/\$ $/\$ $\$
189	56, 99	resubcld 9987	. . . . . . . . . . . . 13 $/\$ $/\$
190	189, 158	ltnled 9731	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
191	188, 190	mpbird 232	. . . . . . . . . . 11 $/\$ $/\$ $\$
192	56, 99, 158	ltsubadd2d 10150	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
193	191, 192	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $\$
194	160, 193	eqbrtrrd 4469	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
195	115, 99, 158	ltadd1d 10145	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
196	194, 195	mpbird 232	. . . . . . . 8 $/\$ $/\$
197	80, 115, 99, 126, 196	lelttrd 9739	. . . . . . 7 $/\$ $/\$
198	172	adantr 465	. . . . . . . . 9 $/\$ $/\$
199		mblvol 21704	. . . . . . . . . . 11
200	6, 199	syl 16	. . . . . . . . . 10 $/\$ $/\$
201	5	rpred 11256	. . . . . . . . . . . 12
202	201	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
203		simprr 756	. . . . . . . . . . . . 13 $/\$ $/\$
204	200, 203	eqbrtrrd 4469	. . . . . . . . . . . 12 $/\$ $/\$
205		ovolcl 21652	. . . . . . . . . . . . . 14
206	36, 205	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
207	202	rexrd 9643	. . . . . . . . . . . . 13 $/\$ $/\$
208		xrltle 11355	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
210	204, 209	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
211		ovollecl 21657	. . . . . . . . . . 11 $/\$ $/\$
212	36, 202, 210, 211	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$
213	200, 212	eqeltrd 2555	. . . . . . . . 9 $/\$ $/\$
214	198, 213	remulcld 9624	. . . . . . . 8 $/\$ $/\$
215	198	rexrd 9643	. . . . . . . . . . . . . 14 $/\$ $/\$
216	3	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
217	216	nnnn0d 10852	. . . . . . . . . . . . . . 15 $/\$ $/\$
218	217	nn0ge0d 10855	. . . . . . . . . . . . . 14 $/\$ $/\$
219		elxrge0 11629	. . . . . . . . . . . . . 14 $/\$
220	215, 218, 219	sylanbrc 664	. . . . . . . . . . . . 13 $/\$ $/\$
221		ifcl 3981	. . . . . . . . . . . . 13 $/\$
222	220, 51, 221	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$
223	222	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
224		eqid 2467	. . . . . . . . . . 11
225	223, 224	fmptd 6045	. . . . . . . . . 10 $/\$ $/\$
226		eldifn 3627	. . . . . . . . . . . . . . . 16 $\$
227	226	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
228		difssd 3632	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
229	228	sselda 3504	. . . . . . . . . . . . . . . . 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 3945	. . . . . . . . . . . . . . 15 $\$ $\$
235	234	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
236		iftrue 3945	. . . . . . . . . . . . . . 15
237	229, 236	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
238	233, 235, 237	3brtr4d 4477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
239		iffalse 3948	. . . . . . . . . . . . . . 15 $\$ $\$
240	239	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
241		0le0 10625	. . . . . . . . . . . . . . . 16
242		breq2 4451	. . . . . . . . . . . . . . . . 17
243		breq2 4451	. . . . . . . . . . . . . . . . 17
244	242, 243	ifboth 3975	. . . . . . . . . . . . . . . 16 $/\$
245	218, 241, 244	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$
246	245	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
247	240, 246	eqbrtrd 4467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
248	238, 247	pm2.61dan 789	. . . . . . . . . . . 12 $/\$ $/\$ $\$
249	248	ralrimivw 2879	. . . . . . . . . . 11 $/\$ $/\$ $\$
250		eqidd 2468	. . . . . . . . . . . 12 $/\$ $/\$
251	72, 82, 223, 89, 250	ofrfval2 6541	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
252	249, 251	mpbird 232	. . . . . . . . . 10 $/\$ $/\$ $\$
253		itg2le 21909	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $\$
254	83, 225, 252, 253	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$ $\$
255		elrege0 11627	. . . . . . . . . . 11 $/\$
256	198, 218, 255	sylanbrc 664	. . . . . . . . . 10 $/\$ $/\$
257		itg2const 21910	. . . . . . . . . 10 $/\$ $/\$
258	6, 213, 256, 257	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$
259	254, 258	breqtrd 4471	. . . . . . . 8 $/\$ $/\$ $\$
260	216	nngt0d 10579	. . . . . . . . . 10 $/\$ $/\$
261		ltmuldiv2 10416	. . . . . . . . . 10 $/\$ $/\$ $/\$
262	213, 99, 198, 260, 261	syl112anc 1232	. . . . . . . . 9 $/\$ $/\$
263	203, 262	mpbird 232	. . . . . . . 8 $/\$ $/\$
264	95, 214, 99, 259, 263	lelttrd 9739	. . . . . . 7 $/\$ $/\$ $\$
265	80, 95, 99, 99, 197, 264	lt2addd 10174	. . . . . 6 $/\$ $/\$ $\$
266	96, 265	eqbrtrd 4467	. . . . 5 $/\$ $/\$
267	97	rpcnd 11258	. . . . . 6 $/\$ $/\$
268	267	2halvesd 10784	. . . . 5 $/\$ $/\$
269	266, 268	breqtrd 4471	. . . 4 $/\$ $/\$
270	269	expr 615	. . 3 $/\$
271	270	ralrimiva 2878	. 2
272		breq2 4451	. . . . 5
273	272	imbi1d 317	. . . 4
274	273	ralbidv 2903	. . 3
275	274	rspcev 3214	. 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 1379

wcel 1767

wral 2814

wrex 2815

cvv 3113 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

cif 3939 class class class wbr 4447

cmpt 4505

ccnv 4998

cdm 4999

cima 5002

wfn 5583

wf 5584

cfv 5588 (class class class)co 6284

cofr 6523

cr 9491

cc0 9492

caddc 9495

cmul 9497

cpnf 9625

cxr 9627

clt 9628

cle 9629

cmin 9805

cdiv 10206

cn 10536

c2 10585

crp 11220

cioo 11529

cico 11531

cicc 11532

covol 21637

cvol 21638 MblFncmbf 21786

citg2 21788

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570 ax-addf 9571

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664