itg2seq - Metamath Proof Explorer

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

Theorem itg2seq 19587

Description: Definitional property of the

integral: for any function

there is a countable sequence

of simple functions less than

whose integrals converge to the integral of

. (This theorem is for the most part unnecessary in lieu of itg2i1fseq 19600, but unlike that theorem this one doesn't require

to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014.)

**Assertion**
Ref	Expression
itg2seq	$/\$ $/\$

Distinct variable group:

Proof of Theorem itg2seq Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnre 9963	. . . . . . . . . . . 12
2	1	ad2antlr 708	. . . . . . . . . . 11 $/\$ $/\$
3		ltpnf 10677	. . . . . . . . . . 11
4	2, 3	syl 16	. . . . . . . . . 10 $/\$ $/\$
5		iftrue 3705	. . . . . . . . . . 11
6	5	adantl 453	. . . . . . . . . 10 $/\$ $/\$
7		simpr 448	. . . . . . . . . 10 $/\$ $/\$
8	4, 6, 7	3brtr4d 4202	. . . . . . . . 9 $/\$ $/\$
9		iffalse 3706	. . . . . . . . . . 11
10	9	adantl 453	. . . . . . . . . 10 $/\$ $/\$
11		itg2cl 19577	. . . . . . . . . . . . . . 15
12		xrrebnd 10712	. . . . . . . . . . . . . . 15 $/\$
13	11, 12	syl 16	. . . . . . . . . . . . . 14 $/\$
14		itg2ge0 19580	. . . . . . . . . . . . . . . 16
15		0re 9047	. . . . . . . . . . . . . . . . . 18
16		mnflt 10678	. . . . . . . . . . . . . . . . . 18
17	15, 16	ax-mp 8	. . . . . . . . . . . . . . . . 17
18		mnfxr 10670	. . . . . . . . . . . . . . . . . . 19
19		0xr 9087	. . . . . . . . . . . . . . . . . . 19
20		xrltletr 10703	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
21	18, 19, 20	mp3an12 1269	. . . . . . . . . . . . . . . . . 18 $/\$
22	11, 21	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
23	17, 22	mpani 658	. . . . . . . . . . . . . . . 16
24	14, 23	mpd 15	. . . . . . . . . . . . . . 15
25	24	biantrurd 495	. . . . . . . . . . . . . 14 $/\$
26		nltpnft 10710	. . . . . . . . . . . . . . . 16
27	11, 26	syl 16	. . . . . . . . . . . . . . 15
28	27	con2bid 320	. . . . . . . . . . . . . 14
29	13, 25, 28	3bitr2rd 274	. . . . . . . . . . . . 13
30	29	biimpa 471	. . . . . . . . . . . 12 $/\$
31	30	adantlr 696	. . . . . . . . . . 11 $/\$ $/\$
32		nnrp 10577	. . . . . . . . . . . . 13
33	32	rpreccld 10614	. . . . . . . . . . . 12
34	33	ad2antlr 708	. . . . . . . . . . 11 $/\$ $/\$
35	31, 34	ltsubrpd 10632	. . . . . . . . . 10 $/\$ $/\$
36	10, 35	eqbrtrd 4192	. . . . . . . . 9 $/\$ $/\$
37	8, 36	pm2.61dan 767	. . . . . . . 8 $/\$
38		nnrecre 9992	. . . . . . . . . . . . 13
39	38	ad2antlr 708	. . . . . . . . . . . 12 $/\$ $/\$
40	31, 39	resubcld 9421	. . . . . . . . . . 11 $/\$ $/\$
41	2, 40	ifclda 3726	. . . . . . . . . 10 $/\$
42	41	rexrd 9090	. . . . . . . . 9 $/\$
43	11	adantr 452	. . . . . . . . 9 $/\$
44		xrltnle 9100	. . . . . . . . 9 $/\$
45	42, 43, 44	syl2anc 643	. . . . . . . 8 $/\$
46	37, 45	mpbid 202	. . . . . . 7 $/\$
47		itg2leub 19579	. . . . . . . 8 $/\$
48	42, 47	syldan 457	. . . . . . 7 $/\$
49	46, 48	mtbid 292	. . . . . 6 $/\$
50		rexanali 2712	. . . . . 6 $/\$
51	49, 50	sylibr 204	. . . . 5 $/\$ $/\$
52		itg1cl 19530	. . . . . . . 8
53		ltnle 9111	. . . . . . . 8 $/\$
54	41, 52, 53	syl2an 464	. . . . . . 7 $/\$ $/\$
55	54	anbi2d 685	. . . . . 6 $/\$ $/\$ $/\$ $/\$
56	55	rexbidva 2683	. . . . 5 $/\$ $/\$ $/\$
57	51, 56	mpbird 224	. . . 4 $/\$ $/\$
58	57	ralrimiva 2749	. . 3 $/\$
59		ovex 6065	. . . . 5
60		i1ff 19521	. . . . . . 7
61		reex 9037	. . . . . . . 8
62	61, 61	elmap 7001	. . . . . . 7
63	60, 62	sylibr 204	. . . . . 6
64	63	ssriv 3312	. . . . 5
65	59, 64	ssexi 4308	. . . 4
66		nnenom 11274	. . . 4
67		breq1 4175	. . . . 5
68		fveq2 5687	. . . . . 6
69	68	breq2d 4184	. . . . 5
70	67, 69	anbi12d 692	. . . 4 $/\$ $/\$
71	65, 66, 70	axcc4 8275	. . 3 $/\$ $/\$ $/\$
72	58, 71	syl 16	. 2 $/\$ $/\$
73		simprl 733	. . . . 5 $/\$ $/\$ $/\$
74		simpl 444	. . . . . . 7 $/\$
75	74	ralimi 2741	. . . . . 6 $/\$
76	75	ad2antll 710	. . . . 5 $/\$ $/\$ $/\$
77		fveq2 5687	. . . . . . . . . . . . 13
78	77	fveq2d 5691	. . . . . . . . . . . 12
79	78	cbvmptv 4260	. . . . . . . . . . 11
80	79	rneqi 5055	. . . . . . . . . 10
81	80	supeq1i 7410	. . . . . . . . 9
82		ffvelrn 5827	. . . . . . . . . . . . . . 15 $/\$
83		itg1cl 19530	. . . . . . . . . . . . . . 15
84	82, 83	syl 16	. . . . . . . . . . . . . 14 $/\$
85		eqid 2404	. . . . . . . . . . . . . 14
86	84, 85	fmptd 5852	. . . . . . . . . . . . 13
87	86	ad2antrl 709	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
88		frn 5556	. . . . . . . . . . . 12
89	87, 88	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$
90		ressxr 9085	. . . . . . . . . . 11
91	89, 90	syl6ss 3320	. . . . . . . . . 10 $/\$ $/\$ $/\$
92		supxrcl 10849	. . . . . . . . . 10
93	91, 92	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
94	81, 93	syl5eqelr 2489	. . . . . . . 8 $/\$ $/\$ $/\$
95		elxr 10672	. . . . . . . . . . 11 $\/$ $\/$
96		simplrl 737	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
97		arch 10174	. . . . . . . . . . . . . . . . . 18
98	96, 97	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
99	5	adantl 453	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
100	99	breq2d 4184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
101	100	rexbidv 2687	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
102	98, 101	mpbird 224	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
103	30	adantlr 696	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
104		simplrl 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
105	103, 104	resubcld 9421	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
106		simplrr 738	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
107	104, 103	posdifd 9569	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
108	106, 107	mpbid 202	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
109		nnrecl 10175	. . . . . . . . . . . . . . . . . 18 $/\$
110	105, 108, 109	syl2anc 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
111	38	adantl 453	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
112	103	adantr 452	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
113	104	adantr 452	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
114		ltsub13 9465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
115	111, 112, 113, 114	syl3anc 1184	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
116	9	ad2antlr 708	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
117	116	breq2d 4184	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
118	115, 117	bitr4d 248	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
119	118	rexbidva 2683	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
120	110, 119	mpbid 202	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
121	102, 120	pm2.61dan 767	. . . . . . . . . . . . . . 15 $/\$ $/\$
122	121	expr 599	. . . . . . . . . . . . . 14 $/\$
123		rexr 9086	. . . . . . . . . . . . . . 15
124		xrltnle 9100	. . . . . . . . . . . . . . 15 $/\$
125	123, 11, 124	syl2anr 465	. . . . . . . . . . . . . 14 $/\$
126	123	ad2antlr 708	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
127	42	adantlr 696	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
128		xrltnle 9100	. . . . . . . . . . . . . . . . 17 $/\$
129	126, 127, 128	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$
130	129	rexbidva 2683	. . . . . . . . . . . . . . 15 $/\$
131		rexnal 2677	. . . . . . . . . . . . . . 15
132	130, 131	syl6bb 253	. . . . . . . . . . . . . 14 $/\$
133	122, 125, 132	3imtr3d 259	. . . . . . . . . . . . 13 $/\$
134	133	con4d 99	. . . . . . . . . . . 12 $/\$
135	11	adantr 452	. . . . . . . . . . . . . . 15 $/\$
136		pnfge 10683	. . . . . . . . . . . . . . 15
137	135, 136	syl 16	. . . . . . . . . . . . . 14 $/\$
138		simpr 448	. . . . . . . . . . . . . 14 $/\$
139	137, 138	breqtrrd 4198	. . . . . . . . . . . . 13 $/\$
140	139	a1d 23	. . . . . . . . . . . 12 $/\$
141		1nn 9967	. . . . . . . . . . . . . . 15
142		ne0i 3594	. . . . . . . . . . . . . . 15
143	141, 142	ax-mp 8	. . . . . . . . . . . . . 14
144		r19.2z 3677	. . . . . . . . . . . . . 14 $/\$
145	143, 144	mpan 652	. . . . . . . . . . . . 13
146	41	adantlr 696	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147		mnflt 10678	. . . . . . . . . . . . . . . . . 18
148		rexr 9086	. . . . . . . . . . . . . . . . . . 19
149		xrltnle 9100	. . . . . . . . . . . . . . . . . . 19 $/\$
150	18, 148, 149	sylancr 645	. . . . . . . . . . . . . . . . . 18
151	147, 150	mpbid 202	. . . . . . . . . . . . . . . . 17
152	146, 151	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
153		simplr 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
154	153	breq2d 4184	. . . . . . . . . . . . . . . 16 $/\$ $/\$
155	152, 154	mtbird 293	. . . . . . . . . . . . . . 15 $/\$ $/\$
156	155	nrexdv 2769	. . . . . . . . . . . . . 14 $/\$
157	156	pm2.21d 100	. . . . . . . . . . . . 13 $/\$
158	145, 157	syl5 30	. . . . . . . . . . . 12 $/\$
159	134, 140, 158	3jaodan 1250	. . . . . . . . . . 11 $/\$ $\/$ $\/$
160	95, 159	sylan2b 462	. . . . . . . . . 10 $/\$
161	160	ralrimiva 2749	. . . . . . . . 9
162	161	adantr 452	. . . . . . . 8 $/\$ $/\$ $/\$
163	42	adantlr 696	. . . . . . . . . . . . 13 $/\$ $/\$
164	84	adantll 695	. . . . . . . . . . . . . 14 $/\$ $/\$
165	164	rexrd 9090	. . . . . . . . . . . . 13 $/\$ $/\$
166		xrltle 10698	. . . . . . . . . . . . 13 $/\$
167	163, 165, 166	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$
168	86	adantl 453	. . . . . . . . . . . . . . . . . 18 $/\$
169	168, 88	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
170	169, 90	syl6ss 3320	. . . . . . . . . . . . . . . 16 $/\$
171	170	adantr 452	. . . . . . . . . . . . . . 15 $/\$ $/\$
172	80, 171	syl5eqssr 3353	. . . . . . . . . . . . . 14 $/\$ $/\$
173		fveq2 5687	. . . . . . . . . . . . . . . . . 18
174	173	fveq2d 5691	. . . . . . . . . . . . . . . . 17
175		eqid 2404	. . . . . . . . . . . . . . . . 17
176		fvex 5701	. . . . . . . . . . . . . . . . 17
177	174, 175, 176	fvmpt 5765	. . . . . . . . . . . . . . . 16
178		fvex 5701	. . . . . . . . . . . . . . . . . 18
179	178, 175	fnmpti 5532	. . . . . . . . . . . . . . . . 17
180		fnfvelrn 5826	. . . . . . . . . . . . . . . . 17 $/\$
181	179, 180	mpan 652	. . . . . . . . . . . . . . . 16
182	177, 181	eqeltrrd 2479	. . . . . . . . . . . . . . 15
183	182	adantl 453	. . . . . . . . . . . . . 14 $/\$ $/\$
184		supxrub 10859	. . . . . . . . . . . . . 14 $/\$
185	172, 183, 184	syl2anc 643	. . . . . . . . . . . . 13 $/\$ $/\$
186	171, 92	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
187	81, 186	syl5eqelr 2489	. . . . . . . . . . . . . 14 $/\$ $/\$
188		xrletr 10704	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
189	163, 165, 187, 188	syl3anc 1184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
190	185, 189	mpan2d 656	. . . . . . . . . . . 12 $/\$ $/\$
191	167, 190	syld 42	. . . . . . . . . . 11 $/\$ $/\$
192	191	adantld 454	. . . . . . . . . 10 $/\$ $/\$ $/\$
193	192	ralimdva 2744	. . . . . . . . 9 $/\$ $/\$
194	193	impr 603	. . . . . . . 8 $/\$ $/\$ $/\$
195		breq2 4176	. . . . . . . . . . 11
196	195	ralbidv 2686	. . . . . . . . . 10
197		breq2 4176	. . . . . . . . . 10
198	196, 197	imbi12d 312	. . . . . . . . 9
199	198	rspcv 3008	. . . . . . . 8
200	94, 162, 194, 199	syl3c 59	. . . . . . 7 $/\$ $/\$ $/\$
201	200, 81	syl6breqr 4212	. . . . . 6 $/\$ $/\$ $/\$
202		itg2ub 19578	. . . . . . . . . . . . . . 15 $/\$ $/\$
203	202	3expia 1155	. . . . . . . . . . . . . 14 $/\$
204	82, 203	sylan2 461	. . . . . . . . . . . . 13 $/\$ $/\$
205	204	anassrs 630	. . . . . . . . . . . 12 $/\$ $/\$
206	205	adantrd 455	. . . . . . . . . . 11 $/\$ $/\$ $/\$
207	206	ralimdva 2744	. . . . . . . . . 10 $/\$ $/\$
208	207	impr 603	. . . . . . . . 9 $/\$ $/\$ $/\$
209	78, 85, 178	fvmpt 5765	. . . . . . . . . . . 12
210	209	breq1d 4182	. . . . . . . . . . 11
211	210	ralbiia 2698	. . . . . . . . . 10
212	78	breq1d 4182	. . . . . . . . . . 11
213	212	cbvralv 2892	. . . . . . . . . 10
214	211, 213	bitr4i 244	. . . . . . . . 9
215	208, 214	sylibr 204	. . . . . . . 8 $/\$ $/\$ $/\$
216		ffn 5550	. . . . . . . . 9
217		breq1 4175	. . . . . . . . . 10
218	217	ralrn 5832	. . . . . . . . 9
219	87, 216, 218	3syl 19	. . . . . . . 8 $/\$ $/\$ $/\$
220	215, 219	mpbird 224	. . . . . . 7 $/\$ $/\$ $/\$
221	11	adantr 452	. . . . . . . 8 $/\$ $/\$ $/\$
222		supxrleub 10861	. . . . . . . 8 $/\$
223	91, 221, 222	syl2anc 643	. . . . . . 7 $/\$ $/\$ $/\$
224	220, 223	mpbird 224	. . . . . 6 $/\$ $/\$ $/\$
225	11	adantr 452	. . . . . . . 8 $/\$
226	170, 92	syl 16	. . . . . . . 8 $/\$
227		xrletri3 10701	. . . . . . . 8 $/\$ $/\$
228	225, 226, 227	syl2anc 643	. . . . . . 7 $/\$ $/\$
229	228	adantrr 698	. . . . . 6 $/\$ $/\$ $/\$ $/\$
230	201, 224, 229	mpbir2and 889	. . . . 5 $/\$ $/\$ $/\$
231	73, 76, 230	3jca 1134	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
232	231	ex 424	. . 3 $/\$ $/\$ $/\$ $/\$
233	232	eximdv 1629	. 2 $/\$ $/\$ $/\$ $/\$
234	72, 233	mpd 15	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $\/$ w3o 935 $/\$ w3a 936

wex 1547

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

wss 3280

c0 3588

cif 3699 class class class wbr 4172

cmpt 4226

cdm 4837

crn 4838

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

cofr 6263

cmap 6977

csup 7403

cr 8945

cc0 8946

c1 8947

cpnf 9073

cmnf 9074

cxr 9075

clt 9076

cle 9077

cmin 9247

cdiv 9633

cn 9956

crp 10568

cicc 10875

citg1 19460

citg2 19461

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cc 8271 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-ofr 6265 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-q 10531 df-rp 10569 df-xadd 10667 df-ioo 10876 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-sum 12435 df-xmet 16650 df-met 16651 df-ovol 19314 df-vol 19315 df-mbf 19465 df-itg1 19466 df-itg2 19467

W3C validator