itg2cnlem2 - Metamath Proof Explorer

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

Theorem itg2cnlem2 22712

Description: Lemma for itgcn 22792. (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 11355	. . 3
3		itg2cn.5	. . . 4
4	3	nnrpd 11341	. . 3
5	2, 4	rpdivcld 11360	. 2
6		simprl 763	. . . . . . . 8 $/\$ $/\$
7		itg2cn.2	. . . . . . . . . 10 MblFn
8	7	adantr 467	. . . . . . . . 9 $/\$ $/\$ MblFn
9		itg2cn.1	. . . . . . . . . . 11
10		rge0ssre 11742	. . . . . . . . . . 11
11		fss 5752	. . . . . . . . . . 11 $/\$
12	9, 10, 11	sylancl 667	. . . . . . . . . 10
13	12	adantr 467	. . . . . . . . 9 $/\$ $/\$
14		mbfima 22580	. . . . . . . . 9 MblFn $/\$
15	8, 13, 14	syl2anc 666	. . . . . . . 8 $/\$ $/\$
16		inmbl 22487	. . . . . . . 8 $/\$
17	6, 15, 16	syl2anc 666	. . . . . . 7 $/\$ $/\$
18		difmbl 22488	. . . . . . . 8 $/\$ $\$
19	6, 15, 18	syl2anc 666	. . . . . . 7 $/\$ $/\$ $\$
20		inass 3673	. . . . . . . . . . 11 $\$ $\$
21		disjdif 3868	. . . . . . . . . . . 12 $\$
22	21	ineq2i 3662	. . . . . . . . . . 11 $\$
23		in0 3789	. . . . . . . . . . 11
24	20, 22, 23	3eqtri 2456	. . . . . . . . . 10 $\$
25	24	fveq2i 5882	. . . . . . . . 9 $\$
26		ovol0 22438	. . . . . . . . 9
27	25, 26	eqtri 2452	. . . . . . . 8 $\$
28	27	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
29		inundif 3874	. . . . . . . . 9 $\$
30	29	eqcomi 2436	. . . . . . . 8 $\$
31	30	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
32		mblss 22477	. . . . . . . . . 10
33	6, 32	syl 17	. . . . . . . . 9 $/\$ $/\$
34	33	sselda 3465	. . . . . . . 8 $/\$ $/\$ $/\$
35	9	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
36	35	ffvelrnda 6035	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
37		elrege0 11740	. . . . . . . . . . . 12 $/\$
38	36, 37	sylib 200	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
39	38	simpld 461	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	39	rexrd 9692	. . . . . . . . 9 $/\$ $/\$ $/\$
41	38	simprd 465	. . . . . . . . 9 $/\$ $/\$ $/\$
42		elxrge0 11743	. . . . . . . . 9 $/\$
43	40, 41, 42	sylanbrc 669	. . . . . . . 8 $/\$ $/\$ $/\$
44	34, 43	syldan 473	. . . . . . 7 $/\$ $/\$ $/\$
45		eqid 2423	. . . . . . 7
46		eqid 2423	. . . . . . 7 $\$ $\$
47		eqid 2423	. . . . . . 7
48		0e0iccpnf 11745	. . . . . . . . . 10
49		ifcl 3952	. . . . . . . . . 10 $/\$
50	43, 48, 49	sylancl 667	. . . . . . . . 9 $/\$ $/\$ $/\$
51	50, 45	fmptd 6059	. . . . . . . 8 $/\$ $/\$
52		itg2cn.3	. . . . . . . . 9
53	52	adantr 467	. . . . . . . 8 $/\$ $/\$
54		icossicc 11723	. . . . . . . . . 10
55		fss 5752	. . . . . . . . . 10 $/\$
56	35, 54, 55	sylancl 667	. . . . . . . . 9 $/\$ $/\$
57	39	leidd 10182	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		breq1 4424	. . . . . . . . . . . . 13
59		breq1 4424	. . . . . . . . . . . . 13
60	58, 59	ifboth 3946	. . . . . . . . . . . 12 $/\$
61	57, 41, 60	syl2anc 666	. . . . . . . . . . 11 $/\$ $/\$ $/\$
62	61	ralrimiva 2840	. . . . . . . . . 10 $/\$ $/\$
63		reex 9632	. . . . . . . . . . . 12
64	63	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
65		eqidd 2424	. . . . . . . . . . 11 $/\$ $/\$
66	35	feqmptd 5932	. . . . . . . . . . 11 $/\$ $/\$
67	64, 50, 39, 65, 66	ofrfval2 6561	. . . . . . . . . 10 $/\$ $/\$
68	62, 67	mpbird 236	. . . . . . . . 9 $/\$ $/\$
69		itg2le 22689	. . . . . . . . 9 $/\$ $/\$
70	51, 56, 68, 69	syl3anc 1265	. . . . . . . 8 $/\$ $/\$
71		itg2lecl 22688	. . . . . . . 8 $/\$ $/\$
72	51, 53, 70, 71	syl3anc 1265	. . . . . . 7 $/\$ $/\$
73		ifcl 3952	. . . . . . . . . 10 $/\$ $\$
74	43, 48, 73	sylancl 667	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
75	74, 46	fmptd 6059	. . . . . . . 8 $/\$ $/\$ $\$
76		breq1 4424	. . . . . . . . . . . . 13 $\$ $\$
77		breq1 4424	. . . . . . . . . . . . 13 $\$ $\$
78	76, 77	ifboth 3946	. . . . . . . . . . . 12 $/\$ $\$
79	57, 41, 78	syl2anc 666	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
80	79	ralrimiva 2840	. . . . . . . . . 10 $/\$ $/\$ $\$
81		eqidd 2424	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
82	64, 74, 39, 81, 66	ofrfval2 6561	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
83	80, 82	mpbird 236	. . . . . . . . 9 $/\$ $/\$ $\$
84		itg2le 22689	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $\$
85	75, 56, 83, 84	syl3anc 1265	. . . . . . . 8 $/\$ $/\$ $\$
86		itg2lecl 22688	. . . . . . . 8 $\$ $/\$ $/\$ $\$ $\$
87	75, 53, 85, 86	syl3anc 1265	. . . . . . 7 $/\$ $/\$ $\$
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 22699	. . . . . 6 $/\$ $/\$ $\$
89	1	adantr 467	. . . . . . . . 9 $/\$ $/\$
90	89	rphalfcld 11355	. . . . . . . 8 $/\$ $/\$
91	90	rpred 11343	. . . . . . 7 $/\$ $/\$
92		ifcl 3952	. . . . . . . . . . 11 $/\$
93	43, 48, 92	sylancl 667	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		eqid 2423	. . . . . . . . . 10
95	93, 94	fmptd 6059	. . . . . . . . 9 $/\$ $/\$
96		breq1 4424	. . . . . . . . . . . . . 14
97		breq1 4424	. . . . . . . . . . . . . 14
98	96, 97	ifboth 3946	. . . . . . . . . . . . 13 $/\$
99	57, 41, 98	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
100	99	ralrimiva 2840	. . . . . . . . . . 11 $/\$ $/\$
101		eqidd 2424	. . . . . . . . . . . 12 $/\$ $/\$
102	64, 93, 43, 101, 66	ofrfval2 6561	. . . . . . . . . . 11 $/\$ $/\$
103	100, 102	mpbird 236	. . . . . . . . . 10 $/\$ $/\$
104		itg2le 22689	. . . . . . . . . 10 $/\$ $/\$
105	95, 56, 103, 104	syl3anc 1265	. . . . . . . . 9 $/\$ $/\$
106		itg2lecl 22688	. . . . . . . . 9 $/\$ $/\$
107	95, 53, 105, 106	syl3anc 1265	. . . . . . . 8 $/\$ $/\$
108		0red 9646	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109		inss2 3684	. . . . . . . . . . . . . 14
110	109	sseli 3461	. . . . . . . . . . . . 13
111	110	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
112		ifle 11492	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113	39, 108, 41, 111, 112	syl31anc 1268	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	113	ralrimiva 2840	. . . . . . . . . 10 $/\$ $/\$
115	64, 50, 93, 65, 101	ofrfval2 6561	. . . . . . . . . 10 $/\$ $/\$
116	114, 115	mpbird 236	. . . . . . . . 9 $/\$ $/\$
117		itg2le 22689	. . . . . . . . 9 $/\$ $/\$
118	51, 95, 116, 117	syl3anc 1265	. . . . . . . 8 $/\$ $/\$
119	66	fveq2d 5883	. . . . . . . . . . 11 $/\$ $/\$
120		cmmbl 22480	. . . . . . . . . . . . 13 $\$
121	15, 120	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $\$
122		disjdif 3868	. . . . . . . . . . . . . . 15 $\$
123	122	fveq2i 5882	. . . . . . . . . . . . . 14 $\$
124	123, 26	eqtri 2452	. . . . . . . . . . . . 13 $\$
125	124	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $\$
126		undif2 3872	. . . . . . . . . . . . 13 $\$
127		mblss 22477	. . . . . . . . . . . . . . 15
128	15, 127	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
129		ssequn1 3637	. . . . . . . . . . . . . 14
130	128, 129	sylib 200	. . . . . . . . . . . . 13 $/\$ $/\$
131	126, 130	syl5req 2477	. . . . . . . . . . . 12 $/\$ $/\$ $\$
132		eqid 2423	. . . . . . . . . . . 12 $\$ $\$
133		iftrue 3916	. . . . . . . . . . . . . 14
134	133	mpteq2ia 4504	. . . . . . . . . . . . 13
135	134	eqcomi 2436	. . . . . . . . . . . 12
136		ifcl 3952	. . . . . . . . . . . . . . 15 $/\$ $\$
137	43, 48, 136	sylancl 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
138	137, 132	fmptd 6059	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
139		breq1 4424	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140		breq1 4424	. . . . . . . . . . . . . . . . . 18 $\$ $\$
141	139, 140	ifboth 3946	. . . . . . . . . . . . . . . . 17 $/\$ $\$
142	57, 41, 141	syl2anc 666	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
143	142	ralrimiva 2840	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
144		eqidd 2424	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
145	64, 137, 43, 144, 66	ofrfval2 6561	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
146	143, 145	mpbird 236	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
147		itg2le 22689	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $\$
148	138, 56, 146, 147	syl3anc 1265	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
149		itg2lecl 22688	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $\$
150	138, 53, 148, 149	syl3anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $\$
151	15, 121, 125, 131, 43, 94, 132, 135, 107, 150	itg2split 22699	. . . . . . . . . . 11 $/\$ $/\$ $\$
152	119, 151	eqtrd 2464	. . . . . . . . . 10 $/\$ $/\$ $\$
153		itg2cn.6	. . . . . . . . . . . . . 14
154	153	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
155		eldif 3447	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
156	155	baib 912	. . . . . . . . . . . . . . . . . . 19 $\$
157	156	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$
158		ffn 5744	. . . . . . . . . . . . . . . . . . . . . . 23
159	9, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
160	159	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
161		elpreima 6015	. . . . . . . . . . . . . . . . . . . . 21 $/\$
162	160, 161	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
163	39	biantrurd 511	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
164	3	nnred 10626	. . . . . . . . . . . . . . . . . . . . . . . 24
165	164	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
166	165	rexrd 9692	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
167		elioopnf 11730	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
168	166, 167	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
169		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
170	169	biantrurd 511	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
171	163, 168, 170	3bitr2d 285	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
172	165, 39	ltnled 9784	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	162, 171, 172	3bitr2rd 286	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174	173	con1bid 332	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175	157, 174	bitrd 257	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
176	175	ifbid 3932	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
177	176	mpteq2dva 4508	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
178	177	fveq2d 5883	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
179	178	breq1d 4431	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
180	154, 179	mtbird 303	. . . . . . . . . . . 12 $/\$ $/\$ $\$
181	53, 91	resubcld 10049	. . . . . . . . . . . . 13 $/\$ $/\$
182	181, 150	ltnled 9784	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
183	180, 182	mpbird 236	. . . . . . . . . . 11 $/\$ $/\$ $\$
184	53, 91, 150	ltsubadd2d 10213	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
185	183, 184	mpbid 214	. . . . . . . . . 10 $/\$ $/\$ $\$
186	152, 185	eqbrtrrd 4444	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
187	107, 91, 150	ltadd1d 10208	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
188	186, 187	mpbird 236	. . . . . . . 8 $/\$ $/\$
189	72, 107, 91, 118, 188	lelttrd 9795	. . . . . . 7 $/\$ $/\$
190	164	adantr 467	. . . . . . . . 9 $/\$ $/\$
191		mblvol 22476	. . . . . . . . . . 11
192	6, 191	syl 17	. . . . . . . . . 10 $/\$ $/\$
193	5	rpred 11343	. . . . . . . . . . . 12
194	193	adantr 467	. . . . . . . . . . 11 $/\$ $/\$
195		simprr 765	. . . . . . . . . . . . 13 $/\$ $/\$
196	192, 195	eqbrtrrd 4444	. . . . . . . . . . . 12 $/\$ $/\$
197		ovolcl 22423	. . . . . . . . . . . . . 14
198	33, 197	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
199	194	rexrd 9692	. . . . . . . . . . . . 13 $/\$ $/\$
200		xrltle 11450	. . . . . . . . . . . . 13 $/\$
201	198, 199, 200	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$
202	196, 201	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
203		ovollecl 22428	. . . . . . . . . . 11 $/\$ $/\$
204	33, 194, 202, 203	syl3anc 1265	. . . . . . . . . 10 $/\$ $/\$
205	192, 204	eqeltrd 2511	. . . . . . . . 9 $/\$ $/\$
206	190, 205	remulcld 9673	. . . . . . . 8 $/\$ $/\$
207	190	rexrd 9692	. . . . . . . . . . . . . 14 $/\$ $/\$
208	3	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$
209	208	nnnn0d 10927	. . . . . . . . . . . . . . 15 $/\$ $/\$
210	209	nn0ge0d 10930	. . . . . . . . . . . . . 14 $/\$ $/\$
211		elxrge0 11743	. . . . . . . . . . . . . 14 $/\$
212	207, 210, 211	sylanbrc 669	. . . . . . . . . . . . 13 $/\$ $/\$
213		ifcl 3952	. . . . . . . . . . . . 13 $/\$
214	212, 48, 213	sylancl 667	. . . . . . . . . . . 12 $/\$ $/\$
215	214	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$
216		eqid 2423	. . . . . . . . . . 11
217	215, 216	fmptd 6059	. . . . . . . . . 10 $/\$ $/\$
218		eldifn 3589	. . . . . . . . . . . . . . . 16 $\$
219	218	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
220		difssd 3594	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
221	220	sselda 3465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
222	34, 173	syldan 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	221, 222	syldan 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
224	223	con1bid 332	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
225	219, 224	mpbid 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
226		iftrue 3916	. . . . . . . . . . . . . . 15 $\$ $\$
227	226	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
228	221	iftrued 3918	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
229	225, 227, 228	3brtr4d 4452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
230		iffalse 3919	. . . . . . . . . . . . . . 15 $\$ $\$
231	230	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
232		0le0 10701	. . . . . . . . . . . . . . . 16
233		breq2 4425	. . . . . . . . . . . . . . . . 17
234		breq2 4425	. . . . . . . . . . . . . . . . 17
235	233, 234	ifboth 3946	. . . . . . . . . . . . . . . 16 $/\$
236	210, 232, 235	sylancl 667	. . . . . . . . . . . . . . 15 $/\$ $/\$
237	236	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
238	231, 237	eqbrtrd 4442	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
239	229, 238	pm2.61dan 799	. . . . . . . . . . . 12 $/\$ $/\$ $\$
240	239	ralrimivw 2841	. . . . . . . . . . 11 $/\$ $/\$ $\$
241		eqidd 2424	. . . . . . . . . . . 12 $/\$ $/\$
242	64, 74, 215, 81, 241	ofrfval2 6561	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
243	240, 242	mpbird 236	. . . . . . . . . 10 $/\$ $/\$ $\$
244		itg2le 22689	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $\$
245	75, 217, 243, 244	syl3anc 1265	. . . . . . . . 9 $/\$ $/\$ $\$
246		elrege0 11740	. . . . . . . . . . 11 $/\$
247	190, 210, 246	sylanbrc 669	. . . . . . . . . 10 $/\$ $/\$
248		itg2const 22690	. . . . . . . . . 10 $/\$ $/\$
249	6, 205, 247, 248	syl3anc 1265	. . . . . . . . 9 $/\$ $/\$
250	245, 249	breqtrd 4446	. . . . . . . 8 $/\$ $/\$ $\$
251	208	nngt0d 10655	. . . . . . . . . 10 $/\$ $/\$
252		ltmuldiv2 10481	. . . . . . . . . 10 $/\$ $/\$ $/\$
253	205, 91, 190, 251, 252	syl112anc 1269	. . . . . . . . 9 $/\$ $/\$
254	195, 253	mpbird 236	. . . . . . . 8 $/\$ $/\$
255	87, 206, 91, 250, 254	lelttrd 9795	. . . . . . 7 $/\$ $/\$ $\$
256	72, 87, 91, 91, 189, 255	lt2addd 10238	. . . . . 6 $/\$ $/\$ $\$
257	88, 256	eqbrtrd 4442	. . . . 5 $/\$ $/\$
258	89	rpcnd 11345	. . . . . 6 $/\$ $/\$
259	258	2halvesd 10860	. . . . 5 $/\$ $/\$
260	257, 259	breqtrd 4446	. . . 4 $/\$ $/\$
261	260	expr 619	. . 3 $/\$
262	261	ralrimiva 2840	. 2
263		breq2 4425	. . . . 5
264	263	imbi1d 319	. . . 4
265	264	ralbidv 2865	. . 3
266	265	rspcev 3183	. 2 $/\$
267	5, 262, 266	syl2anc 666	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1438

wcel 1869

wral 2776

wrex 2777

cvv 3082 $\$ cdif 3434

cun 3435

cin 3436

wss 3437

c0 3762

cif 3910 class class class wbr 4421

cmpt 4480

ccnv 4850

cdm 4851

cima 4854

wfn 5594

wf 5595

cfv 5599 (class class class)co 6303

cofr 6542

cr 9540

cc0 9541

caddc 9544

cmul 9546

cpnf 9674

cxr 9676

clt 9677

cle 9678

cmin 9862

cdiv 10271

cn 10611

c2 10661

crp 11304

cioo 11637

cico 11639

cicc 11640

covol 22405

cvol 22407 MblFncmbf 22564

citg2 22566

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-inf2 8150 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619 ax-addf 9620

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-fal 1444 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-disj 4393 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-se 4811 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-isom 5608 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-of 6543 df-ofr 6544 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-2o 7189 df-oadd 7192 df-er 7369 df-map 7480 df-pm 7481 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-fi 7929 df-sup 7960 df-inf 7961 df-oi 8029 df-card 8376 df-cda 8600 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-2 10670 df-3 10671 df-n0 10872 df-z 10940 df-uz 11162 df-q 11267 df-rp 11305 df-xneg 11411 df-xadd 11412 df-xmul 11413 df-ioo 11641 df-ico 11643 df-icc 11644 df-fz 11787 df-fzo 11918 df-fl 12029 df-seq 12215 df-exp 12274 df-hash 12517 df-cj 13156 df-re 13157 df-im 13158 df-sqrt 13292 df-abs 13293 df-clim 13545 <