itg2cnlem2 - Metamath Proof Explorer

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

Theorem itg2cnlem2 22799

Description: Lemma for itgcn 22879. (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 11376	. . 3
3		itg2cn.5	. . . 4
4	3	nnrpd 11362	. . 3
5	2, 4	rpdivcld 11381	. 2
6		simprl 772	. . . . . . . 8 $/\$ $/\$
7		itg2cn.2	. . . . . . . . . 10 MblFn
8	7	adantr 472	. . . . . . . . 9 $/\$ $/\$ MblFn
9		itg2cn.1	. . . . . . . . . . 11
10		rge0ssre 11766	. . . . . . . . . . 11
11		fss 5749	. . . . . . . . . . 11 $/\$
12	9, 10, 11	sylancl 675	. . . . . . . . . 10
13	12	adantr 472	. . . . . . . . 9 $/\$ $/\$
14		mbfima 22667	. . . . . . . . 9 MblFn $/\$
15	8, 13, 14	syl2anc 673	. . . . . . . 8 $/\$ $/\$
16		inmbl 22574	. . . . . . . 8 $/\$
17	6, 15, 16	syl2anc 673	. . . . . . 7 $/\$ $/\$
18		difmbl 22575	. . . . . . . 8 $/\$ $\$
19	6, 15, 18	syl2anc 673	. . . . . . 7 $/\$ $/\$ $\$
20		inass 3633	. . . . . . . . . . 11 $\$ $\$
21		disjdif 3830	. . . . . . . . . . . 12 $\$
22	21	ineq2i 3622	. . . . . . . . . . 11 $\$
23		in0 3763	. . . . . . . . . . 11
24	20, 22, 23	3eqtri 2497	. . . . . . . . . 10 $\$
25	24	fveq2i 5882	. . . . . . . . 9 $\$
26		ovol0 22524	. . . . . . . . 9
27	25, 26	eqtri 2493	. . . . . . . 8 $\$
28	27	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
29		inundif 3836	. . . . . . . . 9 $\$
30	29	eqcomi 2480	. . . . . . . 8 $\$
31	30	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
32		mblss 22563	. . . . . . . . . 10
33	6, 32	syl 17	. . . . . . . . 9 $/\$ $/\$
34	33	sselda 3418	. . . . . . . 8 $/\$ $/\$ $/\$
35	9	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$
36	35	ffvelrnda 6037	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
37		elrege0 11764	. . . . . . . . . . . 12 $/\$
38	36, 37	sylib 201	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
39	38	simpld 466	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	39	rexrd 9708	. . . . . . . . 9 $/\$ $/\$ $/\$
41	38	simprd 470	. . . . . . . . 9 $/\$ $/\$ $/\$
42		elxrge0 11767	. . . . . . . . 9 $/\$
43	40, 41, 42	sylanbrc 677	. . . . . . . 8 $/\$ $/\$ $/\$
44	34, 43	syldan 478	. . . . . . 7 $/\$ $/\$ $/\$
45		eqid 2471	. . . . . . 7
46		eqid 2471	. . . . . . 7 $\$ $\$
47		eqid 2471	. . . . . . 7
48		0e0iccpnf 11769	. . . . . . . . . 10
49		ifcl 3914	. . . . . . . . . 10 $/\$
50	43, 48, 49	sylancl 675	. . . . . . . . 9 $/\$ $/\$ $/\$
51	50, 45	fmptd 6061	. . . . . . . 8 $/\$ $/\$
52		itg2cn.3	. . . . . . . . 9
53	52	adantr 472	. . . . . . . 8 $/\$ $/\$
54		icossicc 11746	. . . . . . . . . 10
55		fss 5749	. . . . . . . . . 10 $/\$
56	35, 54, 55	sylancl 675	. . . . . . . . 9 $/\$ $/\$
57	39	leidd 10201	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		breq1 4398	. . . . . . . . . . . . 13
59		breq1 4398	. . . . . . . . . . . . 13
60	58, 59	ifboth 3908	. . . . . . . . . . . 12 $/\$
61	57, 41, 60	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$
62	61	ralrimiva 2809	. . . . . . . . . 10 $/\$ $/\$
63		reex 9648	. . . . . . . . . . . 12
64	63	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
65		eqidd 2472	. . . . . . . . . . 11 $/\$ $/\$
66	35	feqmptd 5932	. . . . . . . . . . 11 $/\$ $/\$
67	64, 50, 39, 65, 66	ofrfval2 6568	. . . . . . . . . 10 $/\$ $/\$
68	62, 67	mpbird 240	. . . . . . . . 9 $/\$ $/\$
69		itg2le 22776	. . . . . . . . 9 $/\$ $/\$
70	51, 56, 68, 69	syl3anc 1292	. . . . . . . 8 $/\$ $/\$
71		itg2lecl 22775	. . . . . . . 8 $/\$ $/\$
72	51, 53, 70, 71	syl3anc 1292	. . . . . . 7 $/\$ $/\$
73		ifcl 3914	. . . . . . . . . 10 $/\$ $\$
74	43, 48, 73	sylancl 675	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
75	74, 46	fmptd 6061	. . . . . . . 8 $/\$ $/\$ $\$
76		breq1 4398	. . . . . . . . . . . . 13 $\$ $\$
77		breq1 4398	. . . . . . . . . . . . 13 $\$ $\$
78	76, 77	ifboth 3908	. . . . . . . . . . . 12 $/\$ $\$
79	57, 41, 78	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
80	79	ralrimiva 2809	. . . . . . . . . 10 $/\$ $/\$ $\$
81		eqidd 2472	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
82	64, 74, 39, 81, 66	ofrfval2 6568	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
83	80, 82	mpbird 240	. . . . . . . . 9 $/\$ $/\$ $\$
84		itg2le 22776	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $\$
85	75, 56, 83, 84	syl3anc 1292	. . . . . . . 8 $/\$ $/\$ $\$
86		itg2lecl 22775	. . . . . . . 8 $\$ $/\$ $/\$ $\$ $\$
87	75, 53, 85, 86	syl3anc 1292	. . . . . . 7 $/\$ $/\$ $\$
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 22786	. . . . . 6 $/\$ $/\$ $\$
89	1	adantr 472	. . . . . . . . 9 $/\$ $/\$
90	89	rphalfcld 11376	. . . . . . . 8 $/\$ $/\$
91	90	rpred 11364	. . . . . . 7 $/\$ $/\$
92		ifcl 3914	. . . . . . . . . . 11 $/\$
93	43, 48, 92	sylancl 675	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		eqid 2471	. . . . . . . . . 10
95	93, 94	fmptd 6061	. . . . . . . . 9 $/\$ $/\$
96		breq1 4398	. . . . . . . . . . . . . 14
97		breq1 4398	. . . . . . . . . . . . . 14
98	96, 97	ifboth 3908	. . . . . . . . . . . . 13 $/\$
99	57, 41, 98	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
100	99	ralrimiva 2809	. . . . . . . . . . 11 $/\$ $/\$
101		eqidd 2472	. . . . . . . . . . . 12 $/\$ $/\$
102	64, 93, 43, 101, 66	ofrfval2 6568	. . . . . . . . . . 11 $/\$ $/\$
103	100, 102	mpbird 240	. . . . . . . . . 10 $/\$ $/\$
104		itg2le 22776	. . . . . . . . . 10 $/\$ $/\$
105	95, 56, 103, 104	syl3anc 1292	. . . . . . . . 9 $/\$ $/\$
106		itg2lecl 22775	. . . . . . . . 9 $/\$ $/\$
107	95, 53, 105, 106	syl3anc 1292	. . . . . . . 8 $/\$ $/\$
108		0red 9662	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109		inss2 3644	. . . . . . . . . . . . . 14
110	109	sseli 3414	. . . . . . . . . . . . 13
111	110	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
112		ifle 11513	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113	39, 108, 41, 111, 112	syl31anc 1295	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	113	ralrimiva 2809	. . . . . . . . . 10 $/\$ $/\$
115	64, 50, 93, 65, 101	ofrfval2 6568	. . . . . . . . . 10 $/\$ $/\$
116	114, 115	mpbird 240	. . . . . . . . 9 $/\$ $/\$
117		itg2le 22776	. . . . . . . . 9 $/\$ $/\$
118	51, 95, 116, 117	syl3anc 1292	. . . . . . . 8 $/\$ $/\$
119	66	fveq2d 5883	. . . . . . . . . . 11 $/\$ $/\$
120		cmmbl 22566	. . . . . . . . . . . . 13 $\$
121	15, 120	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $\$
122		disjdif 3830	. . . . . . . . . . . . . . 15 $\$
123	122	fveq2i 5882	. . . . . . . . . . . . . 14 $\$
124	123, 26	eqtri 2493	. . . . . . . . . . . . 13 $\$
125	124	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $\$
126		undif2 3834	. . . . . . . . . . . . 13 $\$
127		mblss 22563	. . . . . . . . . . . . . . 15
128	15, 127	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
129		ssequn1 3595	. . . . . . . . . . . . . 14
130	128, 129	sylib 201	. . . . . . . . . . . . 13 $/\$ $/\$
131	126, 130	syl5req 2518	. . . . . . . . . . . 12 $/\$ $/\$ $\$
132		eqid 2471	. . . . . . . . . . . 12 $\$ $\$
133		iftrue 3878	. . . . . . . . . . . . . 14
134	133	mpteq2ia 4478	. . . . . . . . . . . . 13
135	134	eqcomi 2480	. . . . . . . . . . . 12
136		ifcl 3914	. . . . . . . . . . . . . . 15 $/\$ $\$
137	43, 48, 136	sylancl 675	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
138	137, 132	fmptd 6061	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
139		breq1 4398	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140		breq1 4398	. . . . . . . . . . . . . . . . . 18 $\$ $\$
141	139, 140	ifboth 3908	. . . . . . . . . . . . . . . . 17 $/\$ $\$
142	57, 41, 141	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
143	142	ralrimiva 2809	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
144		eqidd 2472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
145	64, 137, 43, 144, 66	ofrfval2 6568	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
146	143, 145	mpbird 240	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
147		itg2le 22776	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $\$
148	138, 56, 146, 147	syl3anc 1292	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
149		itg2lecl 22775	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $\$
150	138, 53, 148, 149	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $\$
151	15, 121, 125, 131, 43, 94, 132, 135, 107, 150	itg2split 22786	. . . . . . . . . . 11 $/\$ $/\$ $\$
152	119, 151	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$ $\$
153		itg2cn.6	. . . . . . . . . . . . . 14
154	153	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$
155		eldif 3400	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
156	155	baib 919	. . . . . . . . . . . . . . . . . . 19 $\$
157	156	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$
158		ffn 5739	. . . . . . . . . . . . . . . . . . . . . . 23
159	9, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
160	159	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
161		elpreima 6017	. . . . . . . . . . . . . . . . . . . . 21 $/\$
162	160, 161	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
163	39	biantrurd 516	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
164	3	nnred 10646	. . . . . . . . . . . . . . . . . . . . . . . 24
165	164	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
166	165	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
167		elioopnf 11753	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
168	166, 167	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
169		simpr 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
170	169	biantrurd 516	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
171	163, 168, 170	3bitr2d 289	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
172	165, 39	ltnled 9799	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	162, 171, 172	3bitr2rd 290	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174	173	con1bid 337	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175	157, 174	bitrd 261	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
176	175	ifbid 3894	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
177	176	mpteq2dva 4482	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
178	177	fveq2d 5883	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
179	178	breq1d 4405	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
180	154, 179	mtbird 308	. . . . . . . . . . . 12 $/\$ $/\$ $\$
181	53, 91	resubcld 10068	. . . . . . . . . . . . 13 $/\$ $/\$
182	181, 150	ltnled 9799	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
183	180, 182	mpbird 240	. . . . . . . . . . 11 $/\$ $/\$ $\$
184	53, 91, 150	ltsubadd2d 10232	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
185	183, 184	mpbid 215	. . . . . . . . . 10 $/\$ $/\$ $\$
186	152, 185	eqbrtrrd 4418	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
187	107, 91, 150	ltadd1d 10227	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
188	186, 187	mpbird 240	. . . . . . . 8 $/\$ $/\$
189	72, 107, 91, 118, 188	lelttrd 9810	. . . . . . 7 $/\$ $/\$
190	164	adantr 472	. . . . . . . . 9 $/\$ $/\$
191		mblvol 22562	. . . . . . . . . . 11
192	6, 191	syl 17	. . . . . . . . . 10 $/\$ $/\$
193	5	rpred 11364	. . . . . . . . . . . 12
194	193	adantr 472	. . . . . . . . . . 11 $/\$ $/\$
195		simprr 774	. . . . . . . . . . . . 13 $/\$ $/\$
196	192, 195	eqbrtrrd 4418	. . . . . . . . . . . 12 $/\$ $/\$
197		ovolcl 22509	. . . . . . . . . . . . . 14
198	33, 197	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
199	194	rexrd 9708	. . . . . . . . . . . . 13 $/\$ $/\$
200		xrltle 11471	. . . . . . . . . . . . 13 $/\$
201	198, 199, 200	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$
202	196, 201	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
203		ovollecl 22514	. . . . . . . . . . 11 $/\$ $/\$
204	33, 194, 202, 203	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$
205	192, 204	eqeltrd 2549	. . . . . . . . 9 $/\$ $/\$
206	190, 205	remulcld 9689	. . . . . . . 8 $/\$ $/\$
207	190	rexrd 9708	. . . . . . . . . . . . . 14 $/\$ $/\$
208	3	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$
209	208	nnnn0d 10949	. . . . . . . . . . . . . . 15 $/\$ $/\$
210	209	nn0ge0d 10952	. . . . . . . . . . . . . 14 $/\$ $/\$
211		elxrge0 11767	. . . . . . . . . . . . . 14 $/\$
212	207, 210, 211	sylanbrc 677	. . . . . . . . . . . . 13 $/\$ $/\$
213		ifcl 3914	. . . . . . . . . . . . 13 $/\$
214	212, 48, 213	sylancl 675	. . . . . . . . . . . 12 $/\$ $/\$
215	214	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$
216		eqid 2471	. . . . . . . . . . 11
217	215, 216	fmptd 6061	. . . . . . . . . 10 $/\$ $/\$
218		eldifn 3545	. . . . . . . . . . . . . . . 16 $\$
219	218	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
220		difssd 3550	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
221	220	sselda 3418	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
222	34, 173	syldan 478	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
223	221, 222	syldan 478	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
224	223	con1bid 337	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
225	219, 224	mpbid 215	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
226		iftrue 3878	. . . . . . . . . . . . . . 15 $\$ $\$
227	226	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
228	221	iftrued 3880	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
229	225, 227, 228	3brtr4d 4426	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
230		iffalse 3881	. . . . . . . . . . . . . . 15 $\$ $\$
231	230	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
232		0le0 10721	. . . . . . . . . . . . . . . 16
233		breq2 4399	. . . . . . . . . . . . . . . . 17
234		breq2 4399	. . . . . . . . . . . . . . . . 17
235	233, 234	ifboth 3908	. . . . . . . . . . . . . . . 16 $/\$
236	210, 232, 235	sylancl 675	. . . . . . . . . . . . . . 15 $/\$ $/\$
237	236	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
238	231, 237	eqbrtrd 4416	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
239	229, 238	pm2.61dan 808	. . . . . . . . . . . 12 $/\$ $/\$ $\$
240	239	ralrimivw 2810	. . . . . . . . . . 11 $/\$ $/\$ $\$
241		eqidd 2472	. . . . . . . . . . . 12 $/\$ $/\$
242	64, 74, 215, 81, 241	ofrfval2 6568	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
243	240, 242	mpbird 240	. . . . . . . . . 10 $/\$ $/\$ $\$
244		itg2le 22776	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $\$
245	75, 217, 243, 244	syl3anc 1292	. . . . . . . . 9 $/\$ $/\$ $\$
246		elrege0 11764	. . . . . . . . . . 11 $/\$
247	190, 210, 246	sylanbrc 677	. . . . . . . . . 10 $/\$ $/\$
248		itg2const 22777	. . . . . . . . . 10 $/\$ $/\$
249	6, 205, 247, 248	syl3anc 1292	. . . . . . . . 9 $/\$ $/\$
250	245, 249	breqtrd 4420	. . . . . . . 8 $/\$ $/\$ $\$
251	208	nngt0d 10675	. . . . . . . . . 10 $/\$ $/\$
252		ltmuldiv2 10501	. . . . . . . . . 10 $/\$ $/\$ $/\$
253	205, 91, 190, 251, 252	syl112anc 1296	. . . . . . . . 9 $/\$ $/\$
254	195, 253	mpbird 240	. . . . . . . 8 $/\$ $/\$
255	87, 206, 91, 250, 254	lelttrd 9810	. . . . . . 7 $/\$ $/\$ $\$
256	72, 87, 91, 91, 189, 255	lt2addd 10257	. . . . . 6 $/\$ $/\$ $\$
257	88, 256	eqbrtrd 4416	. . . . 5 $/\$ $/\$
258	89	rpcnd 11366	. . . . . 6 $/\$ $/\$
259	258	2halvesd 10881	. . . . 5 $/\$ $/\$
260	257, 259	breqtrd 4420	. . . 4 $/\$ $/\$
261	260	expr 626	. . 3 $/\$
262	261	ralrimiva 2809	. 2
263		breq2 4399	. . . . 5
264	263	imbi1d 324	. . . 4
265	264	ralbidv 2829	. . 3
266	265	rspcev 3136	. 2 $/\$
267	5, 262, 266	syl2anc 673	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376

wceq 1452

wcel 1904

wral 2756

wrex 2757

cvv 3031 $\$ cdif 3387

cun 3388

cin 3389

wss 3390

c0 3722

cif 3872 class class class wbr 4395

cmpt 4454

ccnv 4838

cdm 4839

cima 4842

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cofr 6549

cr 9556

cc0 9557

caddc 9560

cmul 9562

cpnf 9690

cxr 9692

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

c2 10681

crp 11325

cioo 11660

cico 11662

cicc 11663

covol 22491

cvol 22493 MblFncmbf 22651

citg2 22653

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-disj 4367 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-ofr 6551 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs