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 22720

Description: Lemma for itgcn 22800. (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 11353	. . 3
3		itg2cn.5	. . . 4
4	3	nnrpd 11339	. . 3
5	2, 4	rpdivcld 11358	. 2
6		simprl 764	. . . . . . . 8 $/\$ $/\$
7		itg2cn.2	. . . . . . . . . 10 MblFn
8	7	adantr 467	. . . . . . . . 9 $/\$ $/\$ MblFn
9		itg2cn.1	. . . . . . . . . . 11
10		rge0ssre 11740	. . . . . . . . . . 11
11		fss 5737	. . . . . . . . . . 11 $/\$
12	9, 10, 11	sylancl 668	. . . . . . . . . 10
13	12	adantr 467	. . . . . . . . 9 $/\$ $/\$
14		mbfima 22588	. . . . . . . . 9 MblFn $/\$
15	8, 13, 14	syl2anc 667	. . . . . . . 8 $/\$ $/\$
16		inmbl 22495	. . . . . . . 8 $/\$
17	6, 15, 16	syl2anc 667	. . . . . . 7 $/\$ $/\$
18		difmbl 22496	. . . . . . . 8 $/\$ $\$
19	6, 15, 18	syl2anc 667	. . . . . . 7 $/\$ $/\$ $\$
20		inass 3642	. . . . . . . . . . 11 $\$ $\$
21		disjdif 3839	. . . . . . . . . . . 12 $\$
22	21	ineq2i 3631	. . . . . . . . . . 11 $\$
23		in0 3760	. . . . . . . . . . 11
24	20, 22, 23	3eqtri 2477	. . . . . . . . . 10 $\$
25	24	fveq2i 5868	. . . . . . . . 9 $\$
26		ovol0 22446	. . . . . . . . 9
27	25, 26	eqtri 2473	. . . . . . . 8 $\$
28	27	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
29		inundif 3845	. . . . . . . . 9 $\$
30	29	eqcomi 2460	. . . . . . . 8 $\$
31	30	a1i 11	. . . . . . 7 $/\$ $/\$ $\$
32		mblss 22485	. . . . . . . . . 10
33	6, 32	syl 17	. . . . . . . . 9 $/\$ $/\$
34	33	sselda 3432	. . . . . . . 8 $/\$ $/\$ $/\$
35	9	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
36	35	ffvelrnda 6022	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
37		elrege0 11738	. . . . . . . . . . . 12 $/\$
38	36, 37	sylib 200	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
39	38	simpld 461	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	39	rexrd 9690	. . . . . . . . 9 $/\$ $/\$ $/\$
41	38	simprd 465	. . . . . . . . 9 $/\$ $/\$ $/\$
42		elxrge0 11741	. . . . . . . . 9 $/\$
43	40, 41, 42	sylanbrc 670	. . . . . . . 8 $/\$ $/\$ $/\$
44	34, 43	syldan 473	. . . . . . 7 $/\$ $/\$ $/\$
45		eqid 2451	. . . . . . 7
46		eqid 2451	. . . . . . 7 $\$ $\$
47		eqid 2451	. . . . . . 7
48		0e0iccpnf 11743	. . . . . . . . . 10
49		ifcl 3923	. . . . . . . . . 10 $/\$
50	43, 48, 49	sylancl 668	. . . . . . . . 9 $/\$ $/\$ $/\$
51	50, 45	fmptd 6046	. . . . . . . 8 $/\$ $/\$
52		itg2cn.3	. . . . . . . . 9
53	52	adantr 467	. . . . . . . 8 $/\$ $/\$
54		icossicc 11721	. . . . . . . . . 10
55		fss 5737	. . . . . . . . . 10 $/\$
56	35, 54, 55	sylancl 668	. . . . . . . . 9 $/\$ $/\$
57	39	leidd 10180	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		breq1 4405	. . . . . . . . . . . . 13
59		breq1 4405	. . . . . . . . . . . . 13
60	58, 59	ifboth 3917	. . . . . . . . . . . 12 $/\$
61	57, 41, 60	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$
62	61	ralrimiva 2802	. . . . . . . . . 10 $/\$ $/\$
63		reex 9630	. . . . . . . . . . . 12
64	63	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
65		eqidd 2452	. . . . . . . . . . 11 $/\$ $/\$
66	35	feqmptd 5918	. . . . . . . . . . 11 $/\$ $/\$
67	64, 50, 39, 65, 66	ofrfval2 6549	. . . . . . . . . 10 $/\$ $/\$
68	62, 67	mpbird 236	. . . . . . . . 9 $/\$ $/\$
69		itg2le 22697	. . . . . . . . 9 $/\$ $/\$
70	51, 56, 68, 69	syl3anc 1268	. . . . . . . 8 $/\$ $/\$
71		itg2lecl 22696	. . . . . . . 8 $/\$ $/\$
72	51, 53, 70, 71	syl3anc 1268	. . . . . . 7 $/\$ $/\$
73		ifcl 3923	. . . . . . . . . 10 $/\$ $\$
74	43, 48, 73	sylancl 668	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
75	74, 46	fmptd 6046	. . . . . . . 8 $/\$ $/\$ $\$
76		breq1 4405	. . . . . . . . . . . . 13 $\$ $\$
77		breq1 4405	. . . . . . . . . . . . 13 $\$ $\$
78	76, 77	ifboth 3917	. . . . . . . . . . . 12 $/\$ $\$
79	57, 41, 78	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
80	79	ralrimiva 2802	. . . . . . . . . 10 $/\$ $/\$ $\$
81		eqidd 2452	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
82	64, 74, 39, 81, 66	ofrfval2 6549	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
83	80, 82	mpbird 236	. . . . . . . . 9 $/\$ $/\$ $\$
84		itg2le 22697	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $\$
85	75, 56, 83, 84	syl3anc 1268	. . . . . . . 8 $/\$ $/\$ $\$
86		itg2lecl 22696	. . . . . . . 8 $\$ $/\$ $/\$ $\$ $\$
87	75, 53, 85, 86	syl3anc 1268	. . . . . . 7 $/\$ $/\$ $\$
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 22707	. . . . . 6 $/\$ $/\$ $\$
89	1	adantr 467	. . . . . . . . 9 $/\$ $/\$
90	89	rphalfcld 11353	. . . . . . . 8 $/\$ $/\$
91	90	rpred 11341	. . . . . . 7 $/\$ $/\$
92		ifcl 3923	. . . . . . . . . . 11 $/\$
93	43, 48, 92	sylancl 668	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		eqid 2451	. . . . . . . . . 10
95	93, 94	fmptd 6046	. . . . . . . . 9 $/\$ $/\$
96		breq1 4405	. . . . . . . . . . . . . 14
97		breq1 4405	. . . . . . . . . . . . . 14
98	96, 97	ifboth 3917	. . . . . . . . . . . . 13 $/\$
99	57, 41, 98	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
100	99	ralrimiva 2802	. . . . . . . . . . 11 $/\$ $/\$
101		eqidd 2452	. . . . . . . . . . . 12 $/\$ $/\$
102	64, 93, 43, 101, 66	ofrfval2 6549	. . . . . . . . . . 11 $/\$ $/\$
103	100, 102	mpbird 236	. . . . . . . . . 10 $/\$ $/\$
104		itg2le 22697	. . . . . . . . . 10 $/\$ $/\$
105	95, 56, 103, 104	syl3anc 1268	. . . . . . . . 9 $/\$ $/\$
106		itg2lecl 22696	. . . . . . . . 9 $/\$ $/\$
107	95, 53, 105, 106	syl3anc 1268	. . . . . . . 8 $/\$ $/\$
108		0red 9644	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109		inss2 3653	. . . . . . . . . . . . . 14
110	109	sseli 3428	. . . . . . . . . . . . 13
111	110	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
112		ifle 11490	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
113	39, 108, 41, 111, 112	syl31anc 1271	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	113	ralrimiva 2802	. . . . . . . . . 10 $/\$ $/\$
115	64, 50, 93, 65, 101	ofrfval2 6549	. . . . . . . . . 10 $/\$ $/\$
116	114, 115	mpbird 236	. . . . . . . . 9 $/\$ $/\$
117		itg2le 22697	. . . . . . . . 9 $/\$ $/\$
118	51, 95, 116, 117	syl3anc 1268	. . . . . . . 8 $/\$ $/\$
119	66	fveq2d 5869	. . . . . . . . . . 11 $/\$ $/\$
120		cmmbl 22488	. . . . . . . . . . . . 13 $\$
121	15, 120	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $\$
122		disjdif 3839	. . . . . . . . . . . . . . 15 $\$
123	122	fveq2i 5868	. . . . . . . . . . . . . 14 $\$
124	123, 26	eqtri 2473	. . . . . . . . . . . . 13 $\$
125	124	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $\$
126		undif2 3843	. . . . . . . . . . . . 13 $\$
127		mblss 22485	. . . . . . . . . . . . . . 15
128	15, 127	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
129		ssequn1 3604	. . . . . . . . . . . . . 14
130	128, 129	sylib 200	. . . . . . . . . . . . 13 $/\$ $/\$
131	126, 130	syl5req 2498	. . . . . . . . . . . 12 $/\$ $/\$ $\$
132		eqid 2451	. . . . . . . . . . . 12 $\$ $\$
133		iftrue 3887	. . . . . . . . . . . . . 14
134	133	mpteq2ia 4485	. . . . . . . . . . . . 13
135	134	eqcomi 2460	. . . . . . . . . . . 12
136		ifcl 3923	. . . . . . . . . . . . . . 15 $/\$ $\$
137	43, 48, 136	sylancl 668	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
138	137, 132	fmptd 6046	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
139		breq1 4405	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140		breq1 4405	. . . . . . . . . . . . . . . . . 18 $\$ $\$
141	139, 140	ifboth 3917	. . . . . . . . . . . . . . . . 17 $/\$ $\$
142	57, 41, 141	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
143	142	ralrimiva 2802	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
144		eqidd 2452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
145	64, 137, 43, 144, 66	ofrfval2 6549	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
146	143, 145	mpbird 236	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
147		itg2le 22697	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$ $\$
148	138, 56, 146, 147	syl3anc 1268	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
149		itg2lecl 22696	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $\$
150	138, 53, 148, 149	syl3anc 1268	. . . . . . . . . . . 12 $/\$ $/\$ $\$
151	15, 121, 125, 131, 43, 94, 132, 135, 107, 150	itg2split 22707	. . . . . . . . . . 11 $/\$ $/\$ $\$
152	119, 151	eqtrd 2485	. . . . . . . . . 10 $/\$ $/\$ $\$
153		itg2cn.6	. . . . . . . . . . . . . 14
154	153	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
155		eldif 3414	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
156	155	baib 914	. . . . . . . . . . . . . . . . . . 19 $\$
157	156	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$
158		ffn 5728	. . . . . . . . . . . . . . . . . . . . . . 23
159	9, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
160	159	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
161		elpreima 6002	. . . . . . . . . . . . . . . . . . . . 21 $/\$
162	160, 161	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
163	39	biantrurd 511	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
164	3	nnred 10624	. . . . . . . . . . . . . . . . . . . . . . . 24
165	164	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
166	165	rexrd 9690	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
167		elioopnf 11728	. . . . . . . . . . . . . . . . . . . . . 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 9782	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	162, 171, 172	3bitr2rd 286	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174	173	con1bid 332	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
175	157, 174	bitrd 257	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
176	175	ifbid 3903	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
177	176	mpteq2dva 4489	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
178	177	fveq2d 5869	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
179	178	breq1d 4412	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
180	154, 179	mtbird 303	. . . . . . . . . . . 12 $/\$ $/\$ $\$
181	53, 91	resubcld 10047	. . . . . . . . . . . . 13 $/\$ $/\$
182	181, 150	ltnled 9782	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
183	180, 182	mpbird 236	. . . . . . . . . . 11 $/\$ $/\$ $\$
184	53, 91, 150	ltsubadd2d 10211	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
185	183, 184	mpbid 214	. . . . . . . . . 10 $/\$ $/\$ $\$
186	152, 185	eqbrtrrd 4425	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
187	107, 91, 150	ltadd1d 10206	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
188	186, 187	mpbird 236	. . . . . . . 8 $/\$ $/\$
189	72, 107, 91, 118, 188	lelttrd 9793	. . . . . . 7 $/\$ $/\$
190	164	adantr 467	. . . . . . . . 9 $/\$ $/\$
191		mblvol 22484	. . . . . . . . . . 11
192	6, 191	syl 17	. . . . . . . . . 10 $/\$ $/\$
193	5	rpred 11341	. . . . . . . . . . . 12
194	193	adantr 467	. . . . . . . . . . 11 $/\$ $/\$
195		simprr 766	. . . . . . . . . . . . 13 $/\$ $/\$
196	192, 195	eqbrtrrd 4425	. . . . . . . . . . . 12 $/\$ $/\$
197		ovolcl 22431	. . . . . . . . . . . . . 14
198	33, 197	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
199	194	rexrd 9690	. . . . . . . . . . . . 13 $/\$ $/\$
200		xrltle 11448	. . . . . . . . . . . . 13 $/\$
201	198, 199, 200	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$
202	196, 201	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
203		ovollecl 22436	. . . . . . . . . . 11 $/\$ $/\$
204	33, 194, 202, 203	syl3anc 1268	. . . . . . . . . 10 $/\$ $/\$
205	192, 204	eqeltrd 2529	. . . . . . . . 9 $/\$ $/\$
206	190, 205	remulcld 9671	. . . . . . . 8 $/\$ $/\$
207	190	rexrd 9690	. . . . . . . . . . . . . 14 $/\$ $/\$
208	3	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$
209	208	nnnn0d 10925	. . . . . . . . . . . . . . 15 $/\$ $/\$
210	209	nn0ge0d 10928	. . . . . . . . . . . . . 14 $/\$ $/\$
211		elxrge0 11741	. . . . . . . . . . . . . 14 $/\$
212	207, 210, 211	sylanbrc 670	. . . . . . . . . . . . 13 $/\$ $/\$
213		ifcl 3923	. . . . . . . . . . . . 13 $/\$
214	212, 48, 213	sylancl 668	. . . . . . . . . . . 12 $/\$ $/\$
215	214	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$
216		eqid 2451	. . . . . . . . . . 11
217	215, 216	fmptd 6046	. . . . . . . . . 10 $/\$ $/\$
218		eldifn 3556	. . . . . . . . . . . . . . . 16 $\$
219	218	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
220		difssd 3561	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
221	220	sselda 3432	. . . . . . . . . . . . . . . . 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 3887	. . . . . . . . . . . . . . 15 $\$ $\$
227	226	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
228	221	iftrued 3889	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
229	225, 227, 228	3brtr4d 4433	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
230		iffalse 3890	. . . . . . . . . . . . . . 15 $\$ $\$
231	230	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
232		0le0 10699	. . . . . . . . . . . . . . . 16
233		breq2 4406	. . . . . . . . . . . . . . . . 17
234		breq2 4406	. . . . . . . . . . . . . . . . 17
235	233, 234	ifboth 3917	. . . . . . . . . . . . . . . 16 $/\$
236	210, 232, 235	sylancl 668	. . . . . . . . . . . . . . 15 $/\$ $/\$
237	236	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
238	231, 237	eqbrtrd 4423	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
239	229, 238	pm2.61dan 800	. . . . . . . . . . . 12 $/\$ $/\$ $\$
240	239	ralrimivw 2803	. . . . . . . . . . 11 $/\$ $/\$ $\$
241		eqidd 2452	. . . . . . . . . . . 12 $/\$ $/\$
242	64, 74, 215, 81, 241	ofrfval2 6549	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
243	240, 242	mpbird 236	. . . . . . . . . 10 $/\$ $/\$ $\$
244		itg2le 22697	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $\$
245	75, 217, 243, 244	syl3anc 1268	. . . . . . . . 9 $/\$ $/\$ $\$
246		elrege0 11738	. . . . . . . . . . 11 $/\$
247	190, 210, 246	sylanbrc 670	. . . . . . . . . 10 $/\$ $/\$
248		itg2const 22698	. . . . . . . . . 10 $/\$ $/\$
249	6, 205, 247, 248	syl3anc 1268	. . . . . . . . 9 $/\$ $/\$
250	245, 249	breqtrd 4427	. . . . . . . 8 $/\$ $/\$ $\$
251	208	nngt0d 10653	. . . . . . . . . 10 $/\$ $/\$
252		ltmuldiv2 10479	. . . . . . . . . 10 $/\$ $/\$ $/\$
253	205, 91, 190, 251, 252	syl112anc 1272	. . . . . . . . 9 $/\$ $/\$
254	195, 253	mpbird 236	. . . . . . . 8 $/\$ $/\$
255	87, 206, 91, 250, 254	lelttrd 9793	. . . . . . 7 $/\$ $/\$ $\$
256	72, 87, 91, 91, 189, 255	lt2addd 10236	. . . . . 6 $/\$ $/\$ $\$
257	88, 256	eqbrtrd 4423	. . . . 5 $/\$ $/\$
258	89	rpcnd 11343	. . . . . 6 $/\$ $/\$
259	258	2halvesd 10858	. . . . 5 $/\$ $/\$
260	257, 259	breqtrd 4427	. . . 4 $/\$ $/\$
261	260	expr 620	. . 3 $/\$
262	261	ralrimiva 2802	. 2
263		breq2 4406	. . . . 5
264	263	imbi1d 319	. . . 4
265	264	ralbidv 2827	. . 3
266	265	rspcev 3150	. 2 $/\$
267	5, 262, 266	syl2anc 667	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1444

wcel 1887

wral 2737

wrex 2738

cvv 3045 $\$ cdif 3401

cun 3402

cin 3403

wss 3404

c0 3731

cif 3881 class class class wbr 4402

cmpt 4461

ccnv 4833

cdm 4834

cima 4837

wfn 5577

wf 5578

cfv 5582 (class class class)co 6290

cofr 6530

cr 9538

cc0 9539

caddc 9542

cmul 9544

cpnf 9672

cxr 9674

clt 9675

cle 9676

cmin 9860

cdiv 10269

cn 10609

c2 10659

crp 11302

cioo 11635

cico 11637

cicc 11638

covol 22413

cvol 22415 MblFncmbf 22572

citg2 22574

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 ax-addf 9618

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-disj 4374 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-ofr 6532 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs