itg2seq - Metamath Proof Explorer

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

Theorem itg2seq 22577

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 22590, 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 10616	. . . . . . . . . . . 12
2	1	ad2antlr 731	. . . . . . . . . . 11 $/\$ $/\$
3		ltpnf 11422	. . . . . . . . . . 11
4	2, 3	syl 17	. . . . . . . . . 10 $/\$ $/\$
5		iftrue 3921	. . . . . . . . . . 11
6	5	adantl 467	. . . . . . . . . 10 $/\$ $/\$
7		simpr 462	. . . . . . . . . 10 $/\$ $/\$
8	4, 6, 7	3brtr4d 4456	. . . . . . . . 9 $/\$ $/\$
9		iffalse 3924	. . . . . . . . . . 11
10	9	adantl 467	. . . . . . . . . 10 $/\$ $/\$
11		itg2cl 22567	. . . . . . . . . . . . . . 15
12		xrrebnd 11463	. . . . . . . . . . . . . . 15 $/\$
13	11, 12	syl 17	. . . . . . . . . . . . . 14 $/\$
14		itg2ge0 22570	. . . . . . . . . . . . . . . 16
15		mnflt0 11427	. . . . . . . . . . . . . . . . 17
16		mnfxr 11414	. . . . . . . . . . . . . . . . . . 19
17		0xr 9686	. . . . . . . . . . . . . . . . . . 19
18		xrltletr 11454	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
19	16, 17, 18	mp3an12 1350	. . . . . . . . . . . . . . . . . 18 $/\$
20	11, 19	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
21	15, 20	mpani 680	. . . . . . . . . . . . . . . 16
22	14, 21	mpd 15	. . . . . . . . . . . . . . 15
23	22	biantrurd 510	. . . . . . . . . . . . . 14 $/\$
24		nltpnft 11461	. . . . . . . . . . . . . . . 16
25	11, 24	syl 17	. . . . . . . . . . . . . . 15
26	25	con2bid 330	. . . . . . . . . . . . . 14
27	13, 23, 26	3bitr2rd 285	. . . . . . . . . . . . 13
28	27	biimpa 486	. . . . . . . . . . . 12 $/\$
29	28	adantlr 719	. . . . . . . . . . 11 $/\$ $/\$
30		nnrp 11311	. . . . . . . . . . . . 13
31	30	rpreccld 11351	. . . . . . . . . . . 12
32	31	ad2antlr 731	. . . . . . . . . . 11 $/\$ $/\$
33	29, 32	ltsubrpd 11370	. . . . . . . . . 10 $/\$ $/\$
34	10, 33	eqbrtrd 4446	. . . . . . . . 9 $/\$ $/\$
35	8, 34	pm2.61dan 798	. . . . . . . 8 $/\$
36		nnrecre 10646	. . . . . . . . . . . . 13
37	36	ad2antlr 731	. . . . . . . . . . . 12 $/\$ $/\$
38	29, 37	resubcld 10046	. . . . . . . . . . 11 $/\$ $/\$
39	2, 38	ifclda 3947	. . . . . . . . . 10 $/\$
40	39	rexrd 9689	. . . . . . . . 9 $/\$
41	11	adantr 466	. . . . . . . . 9 $/\$
42		xrltnle 9700	. . . . . . . . 9 $/\$
43	40, 41, 42	syl2anc 665	. . . . . . . 8 $/\$
44	35, 43	mpbid 213	. . . . . . 7 $/\$
45		itg2leub 22569	. . . . . . . 8 $/\$
46	40, 45	syldan 472	. . . . . . 7 $/\$
47	44, 46	mtbid 301	. . . . . 6 $/\$
48		rexanali 2885	. . . . . 6 $/\$
49	47, 48	sylibr 215	. . . . 5 $/\$ $/\$
50		itg1cl 22520	. . . . . . . 8
51		ltnle 9712	. . . . . . . 8 $/\$
52	39, 50, 51	syl2an 479	. . . . . . 7 $/\$ $/\$
53	52	anbi2d 708	. . . . . 6 $/\$ $/\$ $/\$ $/\$
54	53	rexbidva 2943	. . . . 5 $/\$ $/\$ $/\$
55	49, 54	mpbird 235	. . . 4 $/\$ $/\$
56	55	ralrimiva 2846	. . 3 $/\$
57		ovex 6333	. . . . 5
58		i1ff 22511	. . . . . . 7
59		reex 9629	. . . . . . . 8
60	59, 59	elmap 7508	. . . . . . 7
61	58, 60	sylibr 215	. . . . . 6
62	61	ssriv 3474	. . . . 5
63	57, 62	ssexi 4570	. . . 4
64		nnenom 12190	. . . 4
65		breq1 4429	. . . . 5
66		fveq2 5881	. . . . . 6
67	66	breq2d 4438	. . . . 5
68	65, 67	anbi12d 715	. . . 4 $/\$ $/\$
69	63, 64, 68	axcc4 8867	. . 3 $/\$ $/\$ $/\$
70	56, 69	syl 17	. 2 $/\$ $/\$
71		simprl 762	. . . . 5 $/\$ $/\$ $/\$
72		simpl 458	. . . . . . 7 $/\$
73	72	ralimi 2825	. . . . . 6 $/\$
74	73	ad2antll 733	. . . . 5 $/\$ $/\$ $/\$
75		fveq2 5881	. . . . . . . . . . . . 13
76	75	fveq2d 5885	. . . . . . . . . . . 12
77	76	cbvmptv 4518	. . . . . . . . . . 11
78	77	rneqi 5081	. . . . . . . . . 10
79	78	supeq1i 7967	. . . . . . . . 9
80		ffvelrn 6035	. . . . . . . . . . . . . . 15 $/\$
81		itg1cl 22520	. . . . . . . . . . . . . . 15
82	80, 81	syl 17	. . . . . . . . . . . . . 14 $/\$
83		eqid 2429	. . . . . . . . . . . . . 14
84	82, 83	fmptd 6061	. . . . . . . . . . . . 13
85	84	ad2antrl 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
86		frn 5752	. . . . . . . . . . . 12
87	85, 86	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88		ressxr 9683	. . . . . . . . . . 11
89	87, 88	syl6ss 3482	. . . . . . . . . 10 $/\$ $/\$ $/\$
90		supxrcl 11600	. . . . . . . . . 10
91	89, 90	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
92	79, 91	syl5eqelr 2522	. . . . . . . 8 $/\$ $/\$ $/\$
93		elxr 11416	. . . . . . . . . . 11 $\/$ $\/$
94		simplrl 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95		arch 10866	. . . . . . . . . . . . . . . . . 18
96	94, 95	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
97	5	adantl 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
98	97	breq2d 4438	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
99	98	rexbidv 2946	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
100	96, 99	mpbird 235	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
101	28	adantlr 719	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		simplrl 768	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
103	101, 102	resubcld 10046	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104		simplrr 769	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
105	102, 101	posdifd 10199	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
106	104, 105	mpbid 213	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
107		nnrecl 10867	. . . . . . . . . . . . . . . . . 18 $/\$
108	103, 106, 107	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
109	36	adantl 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
110	101	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
111	102	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
112		ltsub13 10094	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
113	109, 110, 111, 112	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
114	9	ad2antlr 731	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
115	114	breq2d 4438	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
116	113, 115	bitr4d 259	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
117	116	rexbidva 2943	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	108, 117	mpbid 213	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	100, 118	pm2.61dan 798	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	expr 618	. . . . . . . . . . . . . 14 $/\$
121		rexr 9685	. . . . . . . . . . . . . . 15
122		xrltnle 9700	. . . . . . . . . . . . . . 15 $/\$
123	121, 11, 122	syl2anr 480	. . . . . . . . . . . . . 14 $/\$
124	121	ad2antlr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
125	40	adantlr 719	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
126		xrltnle 9700	. . . . . . . . . . . . . . . . 17 $/\$
127	124, 125, 126	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	127	rexbidva 2943	. . . . . . . . . . . . . . 15 $/\$
129		rexnal 2880	. . . . . . . . . . . . . . 15
130	128, 129	syl6bb 264	. . . . . . . . . . . . . 14 $/\$
131	120, 123, 130	3imtr3d 270	. . . . . . . . . . . . 13 $/\$
132	131	con4d 108	. . . . . . . . . . . 12 $/\$
133	11	adantr 466	. . . . . . . . . . . . . . 15 $/\$
134		pnfge 11432	. . . . . . . . . . . . . . 15
135	133, 134	syl 17	. . . . . . . . . . . . . 14 $/\$
136		simpr 462	. . . . . . . . . . . . . 14 $/\$
137	135, 136	breqtrrd 4452	. . . . . . . . . . . . 13 $/\$
138	137	a1d 26	. . . . . . . . . . . 12 $/\$
139		1nn 10620	. . . . . . . . . . . . . . 15
140	139	ne0ii 3774	. . . . . . . . . . . . . 14
141		r19.2z 3892	. . . . . . . . . . . . . 14 $/\$
142	140, 141	mpan 674	. . . . . . . . . . . . 13
143	39	adantlr 719	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		mnflt 11425	. . . . . . . . . . . . . . . . . 18
145		rexr 9685	. . . . . . . . . . . . . . . . . . 19
146		xrltnle 9700	. . . . . . . . . . . . . . . . . . 19 $/\$
147	16, 145, 146	sylancr 667	. . . . . . . . . . . . . . . . . 18
148	144, 147	mpbid 213	. . . . . . . . . . . . . . . . 17
149	143, 148	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
150		simplr 760	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
151	150	breq2d 4438	. . . . . . . . . . . . . . . 16 $/\$ $/\$
152	149, 151	mtbird 302	. . . . . . . . . . . . . . 15 $/\$ $/\$
153	152	nrexdv 2888	. . . . . . . . . . . . . 14 $/\$
154	153	pm2.21d 109	. . . . . . . . . . . . 13 $/\$
155	142, 154	syl5 33	. . . . . . . . . . . 12 $/\$
156	132, 138, 155	3jaodan 1330	. . . . . . . . . . 11 $/\$ $\/$ $\/$
157	93, 156	sylan2b 477	. . . . . . . . . 10 $/\$
158	157	ralrimiva 2846	. . . . . . . . 9
159	158	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$
160	40	adantlr 719	. . . . . . . . . . . . 13 $/\$ $/\$
161	82	adantll 718	. . . . . . . . . . . . . 14 $/\$ $/\$
162	161	rexrd 9689	. . . . . . . . . . . . 13 $/\$ $/\$
163		xrltle 11448	. . . . . . . . . . . . 13 $/\$
164	160, 162, 163	syl2anc 665	. . . . . . . . . . . 12 $/\$ $/\$
165	84	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$
166	165, 86	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
167	166, 88	syl6ss 3482	. . . . . . . . . . . . . . . 16 $/\$
168	167	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
169	78, 168	syl5eqssr 3515	. . . . . . . . . . . . . 14 $/\$ $/\$
170		fveq2 5881	. . . . . . . . . . . . . . . . . 18
171	170	fveq2d 5885	. . . . . . . . . . . . . . . . 17
172		eqid 2429	. . . . . . . . . . . . . . . . 17
173		fvex 5891	. . . . . . . . . . . . . . . . 17
174	171, 172, 173	fvmpt 5964	. . . . . . . . . . . . . . . 16
175		fvex 5891	. . . . . . . . . . . . . . . . . 18
176	175, 172	fnmpti 5724	. . . . . . . . . . . . . . . . 17
177		fnfvelrn 6034	. . . . . . . . . . . . . . . . 17 $/\$
178	176, 177	mpan 674	. . . . . . . . . . . . . . . 16
179	174, 178	eqeltrrd 2518	. . . . . . . . . . . . . . 15
180	179	adantl 467	. . . . . . . . . . . . . 14 $/\$ $/\$
181		supxrub 11610	. . . . . . . . . . . . . 14 $/\$
182	169, 180, 181	syl2anc 665	. . . . . . . . . . . . 13 $/\$ $/\$
183	168, 90	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
184	79, 183	syl5eqelr 2522	. . . . . . . . . . . . . 14 $/\$ $/\$
185		xrletr 11455	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
186	160, 162, 184, 185	syl3anc 1264	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
187	182, 186	mpan2d 678	. . . . . . . . . . . 12 $/\$ $/\$
188	164, 187	syld 45	. . . . . . . . . . 11 $/\$ $/\$
189	188	adantld 468	. . . . . . . . . 10 $/\$ $/\$ $/\$
190	189	ralimdva 2840	. . . . . . . . 9 $/\$ $/\$
191	190	impr 623	. . . . . . . 8 $/\$ $/\$ $/\$
192		breq2 4430	. . . . . . . . . . 11
193	192	ralbidv 2871	. . . . . . . . . 10
194		breq2 4430	. . . . . . . . . 10
195	193, 194	imbi12d 321	. . . . . . . . 9
196	195	rspcv 3184	. . . . . . . 8
197	92, 159, 191, 196	syl3c 63	. . . . . . 7 $/\$ $/\$ $/\$
198	197, 79	syl6breqr 4466	. . . . . 6 $/\$ $/\$ $/\$
199		itg2ub 22568	. . . . . . . . . . . . . . 15 $/\$ $/\$
200	199	3expia 1207	. . . . . . . . . . . . . 14 $/\$
201	80, 200	sylan2 476	. . . . . . . . . . . . 13 $/\$ $/\$
202	201	anassrs 652	. . . . . . . . . . . 12 $/\$ $/\$
203	202	adantrd 469	. . . . . . . . . . 11 $/\$ $/\$ $/\$
204	203	ralimdva 2840	. . . . . . . . . 10 $/\$ $/\$
205	204	impr 623	. . . . . . . . 9 $/\$ $/\$ $/\$
206	76, 83, 175	fvmpt 5964	. . . . . . . . . . . 12
207	206	breq1d 4436	. . . . . . . . . . 11
208	207	ralbiia 2862	. . . . . . . . . 10
209	76	breq1d 4436	. . . . . . . . . . 11
210	209	cbvralv 3062	. . . . . . . . . 10
211	208, 210	bitr4i 255	. . . . . . . . 9
212	205, 211	sylibr 215	. . . . . . . 8 $/\$ $/\$ $/\$
213		ffn 5746	. . . . . . . . 9
214		breq1 4429	. . . . . . . . . 10
215	214	ralrn 6040	. . . . . . . . 9
216	85, 213, 215	3syl 18	. . . . . . . 8 $/\$ $/\$ $/\$
217	212, 216	mpbird 235	. . . . . . 7 $/\$ $/\$ $/\$
218	11	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$
219		supxrleub 11612	. . . . . . . 8 $/\$
220	89, 218, 219	syl2anc 665	. . . . . . 7 $/\$ $/\$ $/\$
221	217, 220	mpbird 235	. . . . . 6 $/\$ $/\$ $/\$
222	11	adantr 466	. . . . . . . 8 $/\$
223	167, 90	syl 17	. . . . . . . 8 $/\$
224		xrletri3 11451	. . . . . . . 8 $/\$ $/\$
225	222, 223, 224	syl2anc 665	. . . . . . 7 $/\$ $/\$
226	225	adantrr 721	. . . . . 6 $/\$ $/\$ $/\$ $/\$
227	198, 221, 226	mpbir2and 930	. . . . 5 $/\$ $/\$ $/\$
228	71, 74, 227	3jca 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
229	228	ex 435	. . 3 $/\$ $/\$ $/\$ $/\$
230	229	eximdv 1757	. 2 $/\$ $/\$ $/\$ $/\$
231	70, 230	mpd 15	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $\/$ w3o 981 $/\$ w3a 982

wceq 1437

wex 1659

wcel 1870

wne 2625

wral 2782

wrex 2783

wss 3442

c0 3767

cif 3915 class class class wbr 4426

cmpt 4484

cdm 4854

crn 4855

wfn 5596

wf 5597

cfv 5601 (class class class)co 6305

cofr 6544

cmap 7480

csup 7960

cr 9537

cc0 9538

c1 9539

cpnf 9671

cmnf 9672

cxr 9673

clt 9674

cle 9675

cmin 9859

cdiv 10268

cn 10609

crp 11302

cicc 11638

citg1 22450

citg2 22451

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-inf2 8146 ax-cc 8863 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-se 4814 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-ofr 6546 df-om 6707 df-1st 6807 df-2nd 6808 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-1o 7190 df-2o 7191 df-oadd 7194 df-er 7371 df-map 7482 df-pm 7483 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-sup 7962 df-oi 8025 df-card 8372 df-cda 8596 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-div 10269 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-xadd 11410 df-ioo 11639 df-ico 11641 df-icc 11642 df-fz 11783 df-fzo 11914 df-fl 12025 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-clim 13530 df-sum 13731 df-xmet 18898 df-met 18899 df-ovol 22296 df-vol 22297 df-mbf 22454 df-itg1 22455 df-itg2 22456

This theorem is referenced by: (None)

W3C validator