itg2cnlem2 - Metamath Proof Explorer

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

Theorem itg2cnlem2 22147

Description: Lemma for itgcn 22227. (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 11279	. . 3
3		itg2cn.5	. . . 4
4	3	nnrpd 11266	. . 3
5	2, 4	rpdivcld 11284	. 2
6		simprl 756	. . . . . . . 8 $/\$ $/\$
7		itg2cn.2	. . . . . . . . . 10 MblFn
8	7	adantr 465	. . . . . . . . 9 $/\$ $/\$ MblFn
9		itg2cn.1	. . . . . . . . . . 11
10		rge0ssre 11639	. . . . . . . . . . 11
11		fss 5729	. . . . . . . . . . 11 $/\$
12	9, 10, 11	sylancl 662	. . . . . . . . . 10
13	12	adantr 465	. . . . . . . . 9 $/\$ $/\$
14		mbfima 22017	. . . . . . . . 9 MblFn $/\$
15	8, 13, 14	syl2anc 661	. . . . . . . 8 $/\$ $/\$
16		inmbl 21930	. . . . . . . 8 $/\$
17	6, 15, 16	syl2anc 661	. . . . . . 7 $/\$ $/\$
18		difmbl 21931	. . . . . . . 8 $/\$ $\$
19	6, 15, 18	syl2anc 661	. . . . . . 7 $/\$ $/\$ $\$
20		inass 3693	. . . . . . . . . . 11 $\$ $\$
21		disjdif 3886	. . . . . . . . . . . 12 $\$
22	21	ineq2i 3682	. . . . . . . . . . 11 $\$
23		in0 3797	. . . . . . . . . . 11
24	20, 22, 23	3eqtri 2476	. . . . . . . . . 10 $\$
25	24	fveq2i 5859	. . . . . . . . 9 $\$
26		ovol0 21882	. . . . . . . . 9
27	25, 26	eqtri 2472	. . . . . . . 8 $\$
28	27	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
29		inundif 3892	. . . . . . . . 9 $\$
30	29	eqcomi 2456	. . . . . . . 8 $\$
31	30	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
32		mblss 21920	. . . . . . . . . 10
33	6, 32	syl 16	. . . . . . . . 9 $/\$ $/\$
34	33	sselda 3489	. . . . . . . 8 $/\$ $/\$ $/\$
35	9	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
36	35	ffvelrnda 6016	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
37		elrege0 11638	. . . . . . . . . . . 12 $/\$
38	36, 37	sylib 196	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
39	38	simpld 459	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	39	rexrd 9646	. . . . . . . . 9 $/\$ $/\$ $/\$
41	38	simprd 463	. . . . . . . . 9 $/\$ $/\$ $/\$
42		elxrge0 11640	. . . . . . . . 9 $/\$
43	40, 41, 42	sylanbrc 664	. . . . . . . 8 $/\$ $/\$ $/\$
44	34, 43	syldan 470	. . . . . . 7 $/\$ $/\$ $/\$
45		eqid 2443	. . . . . . 7
46		eqid 2443	. . . . . . 7 $\$ $\$
47		eqid 2443	. . . . . . 7
48		0e0iccpnf 11642	. . . . . . . . . 10
49		ifcl 3968	. . . . . . . . . 10 $/\$
50	43, 48, 49	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$
51	50, 45	fmptd 6040	. . . . . . . 8 $/\$ $/\$
52		itg2cn.3	. . . . . . . . 9
53	52	adantr 465	. . . . . . . 8 $/\$ $/\$
54		icossicc 11622	. . . . . . . . . 10
55		fss 5729	. . . . . . . . . 10 $/\$
56	35, 54, 55	sylancl 662	. . . . . . . . 9 $/\$ $/\$
57	39	leidd 10126	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		breq1 4440	. . . . . . . . . . . . 13
59		breq1 4440	. . . . . . . . . . . . 13
60	58, 59	ifboth 3962	. . . . . . . . . . . 12 $/\$
61	57, 41, 60	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
62	61	ralrimiva 2857	. . . . . . . . . 10 $/\$ $/\$
63		reex 9586	. . . . . . . . . . . 12
64	63	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
65		eqidd 2444	. . . . . . . . . . 11 $/\$ $/\$
66	35	feqmptd 5911	. . . . . . . . . . 11 $/\$ $/\$
67	64, 50, 39, 65, 66	ofrfval2 6542	. . . . . . . . . 10 $/\$ $/\$
68	62, 67	mpbird 232	. . . . . . . . 9 $/\$ $/\$
69		itg2le 22124	. . . . . . . . 9 $/\$ $/\$
70	51, 56, 68, 69	syl3anc 1229	. . . . . . . 8 $/\$ $/\$
71		itg2lecl 22123	. . . . . . . 8 $/\$ $/\$
72	51, 53, 70, 71	syl3anc 1229	. . . . . . 7 $/\$ $/\$
73		ifcl 3968	. . . . . . . . . 10 $/\$ $\$
74	43, 48, 73	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
75	74, 46	fmptd 6040	. . . . . . . 8 $/\$ $/\$ $\$
76		breq1 4440	. . . . . . . . . . . . 13 $\$ $\$
77		breq1 4440	. . . . . . . . . . . . 13 $\$ $\$
78	76, 77	ifboth 3962	. . . . . . . . . . . 12 $/\$ $\$
79	57, 41, 78	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
80	79	ralrimiva 2857	. . . . . . . . . 10 $/\$ $/\$ $\$
81		eqidd 2444	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
82	64, 74, 39, 81, 66	ofrfval2 6542	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
83	80, 82	mpbird 232	. . . . . . . . 9 $/\$ $/\$ $\$
84		itg2le 22124	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $\$
85	75, 56, 83, 84	syl3anc 1229	. . . . . . . 8 $/\$ $/\$ $\$
86		itg2lecl 22123	. . . . . . . 8 $\$ $/\$ $/\$ $\$ $\$
87	75, 53, 85, 86	syl3anc 1229	. . . . . . 7 $/\$ $/\$ $\$
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 22134	. . . . . 6 $/\$ $/\$ $\$
89	1	adantr 465	. . . . . . . . 9 $/\$ $/\$
90	89	rphalfcld 11279	. . . . . . . 8 $/\$ $/\$
91	90	rpred 11267	. . . . . . 7 $/\$ $/\$
92		ifcl 3968	. . . . . . . . . . 11 $/\$
93	43, 48, 92	sylancl 662	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		eqid 2443	. . . . . . . . . 10
95	93, 94	fmptd 6040	. . . . . . . . 9 $/\$ $/\$
96		breq1 4440	. . . . . . . . . . . . . 14
97		breq1 4440	. . . . . . . . . . . . . 14
98	96, 97	ifboth 3962	. . . . . . . . . . . . 13 $/\$
99	57, 41, 98	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
100	99	ralrimiva 2857	. . . . . . . . . . 11 $/\$ $/\$
101		eqidd 2444	. . . . . . . . . . . 12 $/\$ $/\$
102	64, 93, 43, 101, 66	ofrfval2 6542	. . . . . . . . . . 11 $/\$ $/\$
103	100, 102	mpbird 232	. . . . . . . . . 10 $/\$ $/\$
104		itg2le 22124	. . . . . . . . . 10 $/\$ $/\$
105	95, 56, 103, 104	syl3anc 1229	. . . . . . . . 9 $/\$ $/\$
106		itg2lecl 22123	. . . . . . . . 9 $/\$ $/\$
107	95, 53, 105, 106	syl3anc 1229	. . . . . . . 8 $/\$ $/\$
108		0red 9600	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109		inss2 3704	. . . . . . . . . . . . . 14
110	109	sseli 3485	. . . . . . . . . . . . 13
111	110	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
112		ifle 11407	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113	39, 108, 41, 111, 112	syl31anc 1232	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	113	ralrimiva 2857	. . . . . . . . . 10 $/\$ $/\$
115	64, 50, 93, 65, 101	ofrfval2 6542	. . . . . . . . . 10 $/\$ $/\$
116	114, 115	mpbird 232	. . . . . . . . 9 $/\$ $/\$
117		itg2le 22124	. . . . . . . . 9 $/\$ $/\$
118	51, 95, 116, 117	syl3anc 1229	. . . . . . . 8 $/\$ $/\$
119	66	fveq2d 5860	. . . . . . . . . . 11 $/\$ $/\$
120		cmmbl 21923	. . . . . . . . . . . . 13 $\$
121	15, 120	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $\$
122		disjdif 3886	. . . . . . . . . . . . . . 15 $\$
123	122	fveq2i 5859	. . . . . . . . . . . . . 14 $\$
124	123, 26	eqtri 2472	. . . . . . . . . . . . 13 $\$
125	124	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $\$
126		undif2 3890	. . . . . . . . . . . . 13 $\$
127		mblss 21920	. . . . . . . . . . . . . . 15
128	15, 127	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
129		ssequn1 3659	. . . . . . . . . . . . . 14
130	128, 129	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
131	126, 130	syl5req 2497	. . . . . . . . . . . 12 $/\$ $/\$ $\$
132		eqid 2443	. . . . . . . . . . . 12 $\$ $\$
133		iftrue 3932	. . . . . . . . . . . . . 14
134	133	mpteq2ia 4519	. . . . . . . . . . . . 13
135	134	eqcomi 2456	. . . . . . . . . . . 12
136		ifcl 3968	. . . . . . . . . . . . . . 15 $/\$ $\$
137	43, 48, 136	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
138	137, 132	fmptd 6040	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
139		breq1 4440	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140		breq1 4440	. . . . . . . . . . . . . . . . . 18 $\$ $\$
141	139, 140	ifboth 3962	. . . . . . . . . . . . . . . . 17 $/\$ $\$
142	57, 41, 141	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
143	142	ralrimiva 2857	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
144		eqidd 2444	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
145	64, 137, 43, 144, 66	ofrfval2 6542	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
146	143, 145	mpbird 232	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
147		itg2le 22124	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $\$
148	138, 56, 146, 147	syl3anc 1229	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
149		itg2lecl 22123	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $\$
150	138, 53, 148, 149	syl3anc 1229	. . . . . . . . . . . 12 $/\$ $/\$ $\$
151	15, 121, 125, 131, 43, 94, 132, 135, 107, 150	itg2split 22134	. . . . . . . . . . 11 $/\$ $/\$ $\$
152	119, 151	eqtrd 2484	. . . . . . . . . 10 $/\$ $/\$ $\$
153		itg2cn.6	. . . . . . . . . . . . . 14
154	153	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
155		eldif 3471	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
156	155	baib 903	. . . . . . . . . . . . . . . . . . 19 $\$
157	156	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$
158		ffn 5721	. . . . . . . . . . . . . . . . . . . . . . 23
159	9, 158	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
160	159	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
161		elpreima 5992	. . . . . . . . . . . . . . . . . . . . 21 $/\$
162	160, 161	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
163	39	biantrurd 508	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
164	3	nnred 10558	. . . . . . . . . . . . . . . . . . . . . . . 24
165	164	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
166	165	rexrd 9646	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
167		elioopnf 11629	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
168	166, 167	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
169		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
170	169	biantrurd 508	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
171	163, 168, 170	3bitr2d 281	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
172	165, 39	ltnled 9735	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	162, 171, 172	3bitr2rd 282	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174	173	con1bid 330	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175	157, 174	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
176	175	ifbid 3948	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
177	176	mpteq2dva 4523	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
178	177	fveq2d 5860	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
179	178	breq1d 4447	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
180	154, 179	mtbird 301	. . . . . . . . . . . 12 $/\$ $/\$ $\$
181	53, 91	resubcld 9994	. . . . . . . . . . . . 13 $/\$ $/\$
182	181, 150	ltnled 9735	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
183	180, 182	mpbird 232	. . . . . . . . . . 11 $/\$ $/\$ $\$
184	53, 91, 150	ltsubadd2d 10157	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
185	183, 184	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $\$
186	152, 185	eqbrtrrd 4459	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
187	107, 91, 150	ltadd1d 10152	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
188	186, 187	mpbird 232	. . . . . . . 8 $/\$ $/\$
189	72, 107, 91, 118, 188	lelttrd 9743	. . . . . . 7 $/\$ $/\$
190	164	adantr 465	. . . . . . . . 9 $/\$ $/\$
191		mblvol 21919	. . . . . . . . . . 11
192	6, 191	syl 16	. . . . . . . . . 10 $/\$ $/\$
193	5	rpred 11267	. . . . . . . . . . . 12
194	193	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
195		simprr 757	. . . . . . . . . . . . 13 $/\$ $/\$
196	192, 195	eqbrtrrd 4459	. . . . . . . . . . . 12 $/\$ $/\$
197		ovolcl 21867	. . . . . . . . . . . . . 14
198	33, 197	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
199	194	rexrd 9646	. . . . . . . . . . . . 13 $/\$ $/\$
200		xrltle 11366	. . . . . . . . . . . . 13 $/\$
201	198, 199, 200	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
202	196, 201	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
203		ovollecl 21872	. . . . . . . . . . 11 $/\$ $/\$
204	33, 194, 202, 203	syl3anc 1229	. . . . . . . . . 10 $/\$ $/\$
205	192, 204	eqeltrd 2531	. . . . . . . . 9 $/\$ $/\$
206	190, 205	remulcld 9627	. . . . . . . 8 $/\$ $/\$
207	190	rexrd 9646	. . . . . . . . . . . . . 14 $/\$ $/\$
208	3	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
209	208	nnnn0d 10859	. . . . . . . . . . . . . . 15 $/\$ $/\$
210	209	nn0ge0d 10862	. . . . . . . . . . . . . 14 $/\$ $/\$
211		elxrge0 11640	. . . . . . . . . . . . . 14 $/\$
212	207, 210, 211	sylanbrc 664	. . . . . . . . . . . . 13 $/\$ $/\$
213		ifcl 3968	. . . . . . . . . . . . 13 $/\$
214	212, 48, 213	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$
215	214	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
216		eqid 2443	. . . . . . . . . . 11
217	215, 216	fmptd 6040	. . . . . . . . . 10 $/\$ $/\$
218		eldifn 3612	. . . . . . . . . . . . . . . 16 $\$
219	218	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
220		difssd 3617	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
221	220	sselda 3489	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
222	34, 173	syldan 470	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	221, 222	syldan 470	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
224	223	con1bid 330	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
225	219, 224	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
226		iftrue 3932	. . . . . . . . . . . . . . 15 $\$ $\$
227	226	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
228	221	iftrued 3934	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
229	225, 227, 228	3brtr4d 4467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
230		iffalse 3935	. . . . . . . . . . . . . . 15 $\$ $\$
231	230	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
232		0le0 10632	. . . . . . . . . . . . . . . 16
233		breq2 4441	. . . . . . . . . . . . . . . . 17
234		breq2 4441	. . . . . . . . . . . . . . . . 17
235	233, 234	ifboth 3962	. . . . . . . . . . . . . . . 16 $/\$
236	210, 232, 235	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$
237	236	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
238	231, 237	eqbrtrd 4457	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
239	229, 238	pm2.61dan 791	. . . . . . . . . . . 12 $/\$ $/\$ $\$
240	239	ralrimivw 2858	. . . . . . . . . . 11 $/\$ $/\$ $\$
241		eqidd 2444	. . . . . . . . . . . 12 $/\$ $/\$
242	64, 74, 215, 81, 241	ofrfval2 6542	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
243	240, 242	mpbird 232	. . . . . . . . . 10 $/\$ $/\$ $\$
244		itg2le 22124	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $\$
245	75, 217, 243, 244	syl3anc 1229	. . . . . . . . 9 $/\$ $/\$ $\$
246		elrege0 11638	. . . . . . . . . . 11 $/\$
247	190, 210, 246	sylanbrc 664	. . . . . . . . . 10 $/\$ $/\$
248		itg2const 22125	. . . . . . . . . 10 $/\$ $/\$
249	6, 205, 247, 248	syl3anc 1229	. . . . . . . . 9 $/\$ $/\$
250	245, 249	breqtrd 4461	. . . . . . . 8 $/\$ $/\$ $\$
251	208	nngt0d 10586	. . . . . . . . . 10 $/\$ $/\$
252		ltmuldiv2 10423	. . . . . . . . . 10 $/\$ $/\$ $/\$
253	205, 91, 190, 251, 252	syl112anc 1233	. . . . . . . . 9 $/\$ $/\$
254	195, 253	mpbird 232	. . . . . . . 8 $/\$ $/\$
255	87, 206, 91, 250, 254	lelttrd 9743	. . . . . . 7 $/\$ $/\$ $\$
256	72, 87, 91, 91, 189, 255	lt2addd 10181	. . . . . 6 $/\$ $/\$ $\$
257	88, 256	eqbrtrd 4457	. . . . 5 $/\$ $/\$
258	89	rpcnd 11269	. . . . . 6 $/\$ $/\$
259	258	2halvesd 10791	. . . . 5 $/\$ $/\$
260	257, 259	breqtrd 4461	. . . 4 $/\$ $/\$
261	260	expr 615	. . 3 $/\$
262	261	ralrimiva 2857	. 2
263		breq2 4441	. . . . 5
264	263	imbi1d 317	. . . 4
265	264	ralbidv 2882	. . 3
266	265	rspcev 3196	. 2 $/\$
267	5, 262, 266	syl2anc 661	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1383

wcel 1804

wral 2793

wrex 2794

cvv 3095 $\$ cdif 3458

cun 3459

cin 3460

wss 3461

c0 3770

cif 3926 class class class wbr 4437

cmpt 4495

ccnv 4988

cdm 4989

cima 4992

wfn 5573

wf 5574

cfv 5578 (class class class)co 6281

cofr 6524

cr 9494

cc0 9495

caddc 9498

cmul 9500

cpnf 9628

cxr 9630

clt 9631

cle 9632

cmin 9810

cdiv 10213

cn 10543

c2 10592

crp 11231

cioo 11540

cico 11542

cicc 11543

covol 21852

cvol 21853 MblFncmbf 22001

citg2 22003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573 ax-addf 9574

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-fal 1389 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-disj 4408 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-of 6525 df-ofr 6526 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-2o 7133 df-oadd 7136 df-er 7313 df-map 7424 df-pm 7425 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-fi 7873 df-sup 7903 df-oi 7938 df-card 8323 df-cda 8551 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10214 df-nn 10544 df-2 10601 df-3 10602 df-n0 10803 df-z 10872 df-uz 11093 df-q 11194 df-rp 11232 df-xneg 11329 df-xadd 11330 df-xmul 11331 df-ioo 11544 df-ico 11546 df-icc 11547 df-fz 11684 df-fzo 11807 df-fl 11911 df-seq 12090 df-exp 12149 df-hash 12388 df-cj 12914 df-re 12915 df-im 12916 df-sqrt 13050 df-abs 13051 df-clim 13293 df-sum 13491 df-rest 14802 df-topgen