itg2cnlem2 - Metamath Proof Explorer

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

Theorem itg2cnlem2 22463

Description: Lemma for itgcn 22543. (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 11318	. . 3
3		itg2cn.5	. . . 4
4	3	nnrpd 11304	. . 3
5	2, 4	rpdivcld 11323	. 2
6		simprl 758	. . . . . . . 8 $/\$ $/\$
7		itg2cn.2	. . . . . . . . . 10 MblFn
8	7	adantr 465	. . . . . . . . 9 $/\$ $/\$ MblFn
9		itg2cn.1	. . . . . . . . . . 11
10		rge0ssre 11684	. . . . . . . . . . 11
11		fss 5724	. . . . . . . . . . 11 $/\$
12	9, 10, 11	sylancl 662	. . . . . . . . . 10
13	12	adantr 465	. . . . . . . . 9 $/\$ $/\$
14		mbfima 22333	. . . . . . . . 9 MblFn $/\$
15	8, 13, 14	syl2anc 661	. . . . . . . 8 $/\$ $/\$
16		inmbl 22246	. . . . . . . 8 $/\$
17	6, 15, 16	syl2anc 661	. . . . . . 7 $/\$ $/\$
18		difmbl 22247	. . . . . . . 8 $/\$ $\$
19	6, 15, 18	syl2anc 661	. . . . . . 7 $/\$ $/\$ $\$
20		inass 3651	. . . . . . . . . . 11 $\$ $\$
21		disjdif 3846	. . . . . . . . . . . 12 $\$
22	21	ineq2i 3640	. . . . . . . . . . 11 $\$
23		in0 3767	. . . . . . . . . . 11
24	20, 22, 23	3eqtri 2437	. . . . . . . . . 10 $\$
25	24	fveq2i 5854	. . . . . . . . 9 $\$
26		ovol0 22198	. . . . . . . . 9
27	25, 26	eqtri 2433	. . . . . . . 8 $\$
28	27	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
29		inundif 3852	. . . . . . . . 9 $\$
30	29	eqcomi 2417	. . . . . . . 8 $\$
31	30	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
32		mblss 22236	. . . . . . . . . 10
33	6, 32	syl 17	. . . . . . . . 9 $/\$ $/\$
34	33	sselda 3444	. . . . . . . 8 $/\$ $/\$ $/\$
35	9	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
36	35	ffvelrnda 6011	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
37		elrege0 11683	. . . . . . . . . . . 12 $/\$
38	36, 37	sylib 198	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
39	38	simpld 459	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	39	rexrd 9675	. . . . . . . . 9 $/\$ $/\$ $/\$
41	38	simprd 463	. . . . . . . . 9 $/\$ $/\$ $/\$
42		elxrge0 11685	. . . . . . . . 9 $/\$
43	40, 41, 42	sylanbrc 664	. . . . . . . 8 $/\$ $/\$ $/\$
44	34, 43	syldan 470	. . . . . . 7 $/\$ $/\$ $/\$
45		eqid 2404	. . . . . . 7
46		eqid 2404	. . . . . . 7 $\$ $\$
47		eqid 2404	. . . . . . 7
48		0e0iccpnf 11687	. . . . . . . . . 10
49		ifcl 3929	. . . . . . . . . 10 $/\$
50	43, 48, 49	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$
51	50, 45	fmptd 6035	. . . . . . . 8 $/\$ $/\$
52		itg2cn.3	. . . . . . . . 9
53	52	adantr 465	. . . . . . . 8 $/\$ $/\$
54		icossicc 11667	. . . . . . . . . 10
55		fss 5724	. . . . . . . . . 10 $/\$
56	35, 54, 55	sylancl 662	. . . . . . . . 9 $/\$ $/\$
57	39	leidd 10161	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		breq1 4400	. . . . . . . . . . . . 13
59		breq1 4400	. . . . . . . . . . . . 13
60	58, 59	ifboth 3923	. . . . . . . . . . . 12 $/\$
61	57, 41, 60	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
62	61	ralrimiva 2820	. . . . . . . . . 10 $/\$ $/\$
63		reex 9615	. . . . . . . . . . . 12
64	63	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
65		eqidd 2405	. . . . . . . . . . 11 $/\$ $/\$
66	35	feqmptd 5904	. . . . . . . . . . 11 $/\$ $/\$
67	64, 50, 39, 65, 66	ofrfval2 6541	. . . . . . . . . 10 $/\$ $/\$
68	62, 67	mpbird 234	. . . . . . . . 9 $/\$ $/\$
69		itg2le 22440	. . . . . . . . 9 $/\$ $/\$
70	51, 56, 68, 69	syl3anc 1232	. . . . . . . 8 $/\$ $/\$
71		itg2lecl 22439	. . . . . . . 8 $/\$ $/\$
72	51, 53, 70, 71	syl3anc 1232	. . . . . . 7 $/\$ $/\$
73		ifcl 3929	. . . . . . . . . 10 $/\$ $\$
74	43, 48, 73	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
75	74, 46	fmptd 6035	. . . . . . . 8 $/\$ $/\$ $\$
76		breq1 4400	. . . . . . . . . . . . 13 $\$ $\$
77		breq1 4400	. . . . . . . . . . . . 13 $\$ $\$
78	76, 77	ifboth 3923	. . . . . . . . . . . 12 $/\$ $\$
79	57, 41, 78	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
80	79	ralrimiva 2820	. . . . . . . . . 10 $/\$ $/\$ $\$
81		eqidd 2405	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
82	64, 74, 39, 81, 66	ofrfval2 6541	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
83	80, 82	mpbird 234	. . . . . . . . 9 $/\$ $/\$ $\$
84		itg2le 22440	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $\$
85	75, 56, 83, 84	syl3anc 1232	. . . . . . . 8 $/\$ $/\$ $\$
86		itg2lecl 22439	. . . . . . . 8 $\$ $/\$ $/\$ $\$ $\$
87	75, 53, 85, 86	syl3anc 1232	. . . . . . 7 $/\$ $/\$ $\$
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 22450	. . . . . 6 $/\$ $/\$ $\$
89	1	adantr 465	. . . . . . . . 9 $/\$ $/\$
90	89	rphalfcld 11318	. . . . . . . 8 $/\$ $/\$
91	90	rpred 11306	. . . . . . 7 $/\$ $/\$
92		ifcl 3929	. . . . . . . . . . 11 $/\$
93	43, 48, 92	sylancl 662	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		eqid 2404	. . . . . . . . . 10
95	93, 94	fmptd 6035	. . . . . . . . 9 $/\$ $/\$
96		breq1 4400	. . . . . . . . . . . . . 14
97		breq1 4400	. . . . . . . . . . . . . 14
98	96, 97	ifboth 3923	. . . . . . . . . . . . 13 $/\$
99	57, 41, 98	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
100	99	ralrimiva 2820	. . . . . . . . . . 11 $/\$ $/\$
101		eqidd 2405	. . . . . . . . . . . 12 $/\$ $/\$
102	64, 93, 43, 101, 66	ofrfval2 6541	. . . . . . . . . . 11 $/\$ $/\$
103	100, 102	mpbird 234	. . . . . . . . . 10 $/\$ $/\$
104		itg2le 22440	. . . . . . . . . 10 $/\$ $/\$
105	95, 56, 103, 104	syl3anc 1232	. . . . . . . . 9 $/\$ $/\$
106		itg2lecl 22439	. . . . . . . . 9 $/\$ $/\$
107	95, 53, 105, 106	syl3anc 1232	. . . . . . . 8 $/\$ $/\$
108		0red 9629	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109		inss2 3662	. . . . . . . . . . . . . 14
110	109	sseli 3440	. . . . . . . . . . . . 13
111	110	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
112		ifle 11451	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113	39, 108, 41, 111, 112	syl31anc 1235	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	113	ralrimiva 2820	. . . . . . . . . 10 $/\$ $/\$
115	64, 50, 93, 65, 101	ofrfval2 6541	. . . . . . . . . 10 $/\$ $/\$
116	114, 115	mpbird 234	. . . . . . . . 9 $/\$ $/\$
117		itg2le 22440	. . . . . . . . 9 $/\$ $/\$
118	51, 95, 116, 117	syl3anc 1232	. . . . . . . 8 $/\$ $/\$
119	66	fveq2d 5855	. . . . . . . . . . 11 $/\$ $/\$
120		cmmbl 22239	. . . . . . . . . . . . 13 $\$
121	15, 120	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $\$
122		disjdif 3846	. . . . . . . . . . . . . . 15 $\$
123	122	fveq2i 5854	. . . . . . . . . . . . . 14 $\$
124	123, 26	eqtri 2433	. . . . . . . . . . . . 13 $\$
125	124	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $\$
126		undif2 3850	. . . . . . . . . . . . 13 $\$
127		mblss 22236	. . . . . . . . . . . . . . 15
128	15, 127	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
129		ssequn1 3615	. . . . . . . . . . . . . 14
130	128, 129	sylib 198	. . . . . . . . . . . . 13 $/\$ $/\$
131	126, 130	syl5req 2458	. . . . . . . . . . . 12 $/\$ $/\$ $\$
132		eqid 2404	. . . . . . . . . . . 12 $\$ $\$
133		iftrue 3893	. . . . . . . . . . . . . 14
134	133	mpteq2ia 4479	. . . . . . . . . . . . 13
135	134	eqcomi 2417	. . . . . . . . . . . 12
136		ifcl 3929	. . . . . . . . . . . . . . 15 $/\$ $\$
137	43, 48, 136	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
138	137, 132	fmptd 6035	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
139		breq1 4400	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140		breq1 4400	. . . . . . . . . . . . . . . . . 18 $\$ $\$
141	139, 140	ifboth 3923	. . . . . . . . . . . . . . . . 17 $/\$ $\$
142	57, 41, 141	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
143	142	ralrimiva 2820	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
144		eqidd 2405	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
145	64, 137, 43, 144, 66	ofrfval2 6541	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
146	143, 145	mpbird 234	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
147		itg2le 22440	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $\$
148	138, 56, 146, 147	syl3anc 1232	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
149		itg2lecl 22439	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $\$
150	138, 53, 148, 149	syl3anc 1232	. . . . . . . . . . . 12 $/\$ $/\$ $\$
151	15, 121, 125, 131, 43, 94, 132, 135, 107, 150	itg2split 22450	. . . . . . . . . . 11 $/\$ $/\$ $\$
152	119, 151	eqtrd 2445	. . . . . . . . . 10 $/\$ $/\$ $\$
153		itg2cn.6	. . . . . . . . . . . . . 14
154	153	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
155		eldif 3426	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
156	155	baib 906	. . . . . . . . . . . . . . . . . . 19 $\$
157	156	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$
158		ffn 5716	. . . . . . . . . . . . . . . . . . . . . . 23
159	9, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
160	159	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
161		elpreima 5987	. . . . . . . . . . . . . . . . . . . . 21 $/\$
162	160, 161	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
163	39	biantrurd 508	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
164	3	nnred 10593	. . . . . . . . . . . . . . . . . . . . . . . 24
165	164	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
166	165	rexrd 9675	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
167		elioopnf 11674	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
168	166, 167	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
169		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
170	169	biantrurd 508	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
171	163, 168, 170	3bitr2d 283	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
172	165, 39	ltnled 9766	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	162, 171, 172	3bitr2rd 284	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174	173	con1bid 330	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175	157, 174	bitrd 255	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
176	175	ifbid 3909	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
177	176	mpteq2dva 4483	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
178	177	fveq2d 5855	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
179	178	breq1d 4407	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
180	154, 179	mtbird 301	. . . . . . . . . . . 12 $/\$ $/\$ $\$
181	53, 91	resubcld 10030	. . . . . . . . . . . . 13 $/\$ $/\$
182	181, 150	ltnled 9766	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
183	180, 182	mpbird 234	. . . . . . . . . . 11 $/\$ $/\$ $\$
184	53, 91, 150	ltsubadd2d 10192	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
185	183, 184	mpbid 212	. . . . . . . . . 10 $/\$ $/\$ $\$
186	152, 185	eqbrtrrd 4419	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
187	107, 91, 150	ltadd1d 10187	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
188	186, 187	mpbird 234	. . . . . . . 8 $/\$ $/\$
189	72, 107, 91, 118, 188	lelttrd 9776	. . . . . . 7 $/\$ $/\$
190	164	adantr 465	. . . . . . . . 9 $/\$ $/\$
191		mblvol 22235	. . . . . . . . . . 11
192	6, 191	syl 17	. . . . . . . . . 10 $/\$ $/\$
193	5	rpred 11306	. . . . . . . . . . . 12
194	193	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
195		simprr 760	. . . . . . . . . . . . 13 $/\$ $/\$
196	192, 195	eqbrtrrd 4419	. . . . . . . . . . . 12 $/\$ $/\$
197		ovolcl 22183	. . . . . . . . . . . . . 14
198	33, 197	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
199	194	rexrd 9675	. . . . . . . . . . . . 13 $/\$ $/\$
200		xrltle 11410	. . . . . . . . . . . . 13 $/\$
201	198, 199, 200	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
202	196, 201	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
203		ovollecl 22188	. . . . . . . . . . 11 $/\$ $/\$
204	33, 194, 202, 203	syl3anc 1232	. . . . . . . . . 10 $/\$ $/\$
205	192, 204	eqeltrd 2492	. . . . . . . . 9 $/\$ $/\$
206	190, 205	remulcld 9656	. . . . . . . 8 $/\$ $/\$
207	190	rexrd 9675	. . . . . . . . . . . . . 14 $/\$ $/\$
208	3	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
209	208	nnnn0d 10895	. . . . . . . . . . . . . . 15 $/\$ $/\$
210	209	nn0ge0d 10898	. . . . . . . . . . . . . 14 $/\$ $/\$
211		elxrge0 11685	. . . . . . . . . . . . . 14 $/\$
212	207, 210, 211	sylanbrc 664	. . . . . . . . . . . . 13 $/\$ $/\$
213		ifcl 3929	. . . . . . . . . . . . 13 $/\$
214	212, 48, 213	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$
215	214	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
216		eqid 2404	. . . . . . . . . . 11
217	215, 216	fmptd 6035	. . . . . . . . . 10 $/\$ $/\$
218		eldifn 3568	. . . . . . . . . . . . . . . 16 $\$
219	218	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
220		difssd 3573	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
221	220	sselda 3444	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
222	34, 173	syldan 470	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	221, 222	syldan 470	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
224	223	con1bid 330	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
225	219, 224	mpbid 212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
226		iftrue 3893	. . . . . . . . . . . . . . 15 $\$ $\$
227	226	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
228	221	iftrued 3895	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
229	225, 227, 228	3brtr4d 4427	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
230		iffalse 3896	. . . . . . . . . . . . . . 15 $\$ $\$
231	230	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
232		0le0 10668	. . . . . . . . . . . . . . . 16
233		breq2 4401	. . . . . . . . . . . . . . . . 17
234		breq2 4401	. . . . . . . . . . . . . . . . 17
235	233, 234	ifboth 3923	. . . . . . . . . . . . . . . 16 $/\$
236	210, 232, 235	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$
237	236	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
238	231, 237	eqbrtrd 4417	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
239	229, 238	pm2.61dan 794	. . . . . . . . . . . 12 $/\$ $/\$ $\$
240	239	ralrimivw 2821	. . . . . . . . . . 11 $/\$ $/\$ $\$
241		eqidd 2405	. . . . . . . . . . . 12 $/\$ $/\$
242	64, 74, 215, 81, 241	ofrfval2 6541	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
243	240, 242	mpbird 234	. . . . . . . . . 10 $/\$ $/\$ $\$
244		itg2le 22440	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $\$
245	75, 217, 243, 244	syl3anc 1232	. . . . . . . . 9 $/\$ $/\$ $\$
246		elrege0 11683	. . . . . . . . . . 11 $/\$
247	190, 210, 246	sylanbrc 664	. . . . . . . . . 10 $/\$ $/\$
248		itg2const 22441	. . . . . . . . . 10 $/\$ $/\$
249	6, 205, 247, 248	syl3anc 1232	. . . . . . . . 9 $/\$ $/\$
250	245, 249	breqtrd 4421	. . . . . . . 8 $/\$ $/\$ $\$
251	208	nngt0d 10622	. . . . . . . . . 10 $/\$ $/\$
252		ltmuldiv2 10459	. . . . . . . . . 10 $/\$ $/\$ $/\$
253	205, 91, 190, 251, 252	syl112anc 1236	. . . . . . . . 9 $/\$ $/\$
254	195, 253	mpbird 234	. . . . . . . 8 $/\$ $/\$
255	87, 206, 91, 250, 254	lelttrd 9776	. . . . . . 7 $/\$ $/\$ $\$
256	72, 87, 91, 91, 189, 255	lt2addd 10216	. . . . . 6 $/\$ $/\$ $\$
257	88, 256	eqbrtrd 4417	. . . . 5 $/\$ $/\$
258	89	rpcnd 11308	. . . . . 6 $/\$ $/\$
259	258	2halvesd 10827	. . . . 5 $/\$ $/\$
260	257, 259	breqtrd 4421	. . . 4 $/\$ $/\$
261	260	expr 615	. . 3 $/\$
262	261	ralrimiva 2820	. 2
263		breq2 4401	. . . . 5
264	263	imbi1d 317	. . . 4
265	264	ralbidv 2845	. . 3
266	265	rspcev 3162	. 2 $/\$
267	5, 262, 266	syl2anc 661	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 186 $/\$ wa 369

wceq 1407

wcel 1844

wral 2756

wrex 2757

cvv 3061 $\$ cdif 3413

cun 3414

cin 3415

wss 3416

c0 3740

cif 3887 class class class wbr 4397

cmpt 4455

ccnv 4824

cdm 4825

cima 4828

wfn 5566

wf 5567

cfv 5571 (class class class)co 6280

cofr 6522

cr 9523

cc0 9524

caddc 9527

cmul 9529

cpnf 9657

cxr 9659

clt 9660

cle 9661

cmin 9843

cdiv 10249

cn 10578

c2 10628

crp 11267

cioo 11584

cico 11586

cicc 11587

covol 22168

cvol 22169 MblFncmbf 22317

citg2 22319

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1641 ax-4 1654 ax-5 1727 ax-6 1773 ax-7 1816 ax-8 1846 ax-9 1848 ax-10 1863 ax-11 1868 ax-12 1880 ax-13 2028 ax-ext 2382 ax-rep 4509 ax-sep 4519 ax-nul 4527 ax-pow 4574 ax-pr 4632 ax-un 6576 ax-inf2 8093 ax-cnex 9580 ax-resscn 9581 ax-1cn 9582 ax-icn 9583 ax-addcl 9584 ax-addrcl 9585 ax-mulcl 9586 ax-mulrcl 9587 ax-mulcom 9588 ax-addass 9589 ax-mulass 9590 ax-distr 9591 ax-i2m1 9592 ax-1ne0 9593 ax-1rid 9594 ax-rnegex 9595 ax-rrecex 9596 ax-cnre 9597 ax-pre-lttri 9598 ax-pre-lttrn 9599 ax-pre-ltadd 9600 ax-pre-mulgt0 9601 ax-pre-sup 9602 ax-addf 9603

This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-fal 1413 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-nel 2603 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-tp 3979 df-op 3981 df-uni 4194 df-int 4230 df-iun 4275 df-disj 4369 df-br 4398 df-opab 4456 df-mpt 4457 df-tr 4492 df-eprel 4736 df-id 4740 df-po 4746 df-so 4747 df-fr 4784 df-se 4785 df-we 4786 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-pred 5369 df-ord 5415 df-on 5416 df-lim 5417 df-suc 5418 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-isom 5580 df-riota 6242 df-ov 6283 df-oprab 6284 df-mpt2 6285 df-of 6523 df-ofr 6524 df-om 6686 df-1st 6786 df-2nd 6787 df-wrecs 7015 df-recs 7077 df-rdg 7115 df-1o 7169 df-2o 7170 df-oadd 7173 df-er 7350 df-map 7461 df-pm 7462 df-en 7557 df-dom 7558 df-sdom 7559 df-fin 7560 df-fi 7907 df-sup 7937 df-oi 7971 df-card 8354 df-cda 8582 df-pnf 9662 df-mnf 9663 df-xr 9664 df-ltxr 9665 df-le 9666 df-sub 9845 df-neg 9846 df-div 10250 df-nn 10579 df-2 10637 df-3 10638 df-n0 10839 df-z 10908 df-uz 11130 df-q 11230 df-rp 11268 df-xneg 11373 df-xadd 11374 df-xmul 11375 df-ioo 11588 df-ico 11590 df-icc 11591 df-fz 11729 df-fzo 11857 df-fl 11968 df-seq 12154 df-exp 12213 df-hash 12455 df-cj 13083 df-re 13084 df-im 13085 df-sqrt 13219 df-abs 13220 df-clim 13462 df-sum