itg2seq - Metamath Proof Explorer

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

Theorem itg2seq 22635

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 22648, 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 10560	. . . . . . . . . . . 12
2	1	ad2antlr 731	. . . . . . . . . . 11 $/\$ $/\$
3		ltpnf 11366	. . . . . . . . . . 11
4	2, 3	syl 17	. . . . . . . . . 10 $/\$ $/\$
5		iftrue 3853	. . . . . . . . . . 11
6	5	adantl 467	. . . . . . . . . 10 $/\$ $/\$
7		simpr 462	. . . . . . . . . 10 $/\$ $/\$
8	4, 6, 7	3brtr4d 4390	. . . . . . . . 9 $/\$ $/\$
9		iffalse 3856	. . . . . . . . . . 11
10	9	adantl 467	. . . . . . . . . 10 $/\$ $/\$
11		itg2cl 22625	. . . . . . . . . . . . . . 15
12		xrrebnd 11407	. . . . . . . . . . . . . . 15 $/\$
13	11, 12	syl 17	. . . . . . . . . . . . . 14 $/\$
14		itg2ge0 22628	. . . . . . . . . . . . . . . 16
15		mnflt0 11371	. . . . . . . . . . . . . . . . 17
16		mnfxr 11358	. . . . . . . . . . . . . . . . . . 19
17		0xr 9631	. . . . . . . . . . . . . . . . . . 19
18		xrltletr 11398	. . . . . . . . . . . . . . . . . . 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 11405	. . . . . . . . . . . . . . . 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 11255	. . . . . . . . . . . . 13
31	30	rpreccld 11295	. . . . . . . . . . . 12
32	31	ad2antlr 731	. . . . . . . . . . 11 $/\$ $/\$
33	29, 32	ltsubrpd 11314	. . . . . . . . . 10 $/\$ $/\$
34	10, 33	eqbrtrd 4380	. . . . . . . . 9 $/\$ $/\$
35	8, 34	pm2.61dan 798	. . . . . . . 8 $/\$
36		nnrecre 10590	. . . . . . . . . . . . 13
37	36	ad2antlr 731	. . . . . . . . . . . 12 $/\$ $/\$
38	29, 37	resubcld 9991	. . . . . . . . . . 11 $/\$ $/\$
39	2, 38	ifclda 3879	. . . . . . . . . 10 $/\$
40	39	rexrd 9634	. . . . . . . . 9 $/\$
41	11	adantr 466	. . . . . . . . 9 $/\$
42		xrltnle 9645	. . . . . . . . 9 $/\$
43	40, 41, 42	syl2anc 665	. . . . . . . 8 $/\$
44	35, 43	mpbid 213	. . . . . . 7 $/\$
45		itg2leub 22627	. . . . . . . 8 $/\$
46	40, 45	syldan 472	. . . . . . 7 $/\$
47	44, 46	mtbid 301	. . . . . 6 $/\$
48		rexanali 2811	. . . . . 6 $/\$
49	47, 48	sylibr 215	. . . . 5 $/\$ $/\$
50		itg1cl 22578	. . . . . . . 8
51		ltnle 9657	. . . . . . . 8 $/\$
52	39, 50, 51	syl2an 479	. . . . . . 7 $/\$ $/\$
53	52	anbi2d 708	. . . . . 6 $/\$ $/\$ $/\$ $/\$
54	53	rexbidva 2869	. . . . 5 $/\$ $/\$ $/\$
55	49, 54	mpbird 235	. . . 4 $/\$ $/\$
56	55	ralrimiva 2773	. . 3 $/\$
57		ovex 6270	. . . . 5
58		i1ff 22569	. . . . . . 7
59		reex 9574	. . . . . . . 8
60	59, 59	elmap 7448	. . . . . . 7
61	58, 60	sylibr 215	. . . . . 6
62	61	ssriv 3404	. . . . 5
63	57, 62	ssexi 4505	. . . 4
64		nnenom 12136	. . . 4
65		breq1 4362	. . . . 5
66		fveq2 5818	. . . . . 6
67	66	breq2d 4371	. . . . 5
68	65, 67	anbi12d 715	. . . 4 $/\$ $/\$
69	63, 64, 68	axcc4 8813	. . 3 $/\$ $/\$ $/\$
70	56, 69	syl 17	. 2 $/\$ $/\$
71		simprl 762	. . . . 5 $/\$ $/\$ $/\$
72		simpl 458	. . . . . . 7 $/\$
73	72	ralimi 2752	. . . . . 6 $/\$
74	73	ad2antll 733	. . . . 5 $/\$ $/\$ $/\$
75		fveq2 5818	. . . . . . . . . . . . 13
76	75	fveq2d 5822	. . . . . . . . . . . 12
77	76	cbvmptv 4452	. . . . . . . . . . 11
78	77	rneqi 5016	. . . . . . . . . 10
79	78	supeq1i 7907	. . . . . . . . 9
80		ffvelrn 5972	. . . . . . . . . . . . . . 15 $/\$
81		itg1cl 22578	. . . . . . . . . . . . . . 15
82	80, 81	syl 17	. . . . . . . . . . . . . 14 $/\$
83		eqid 2422	. . . . . . . . . . . . . 14
84	82, 83	fmptd 5998	. . . . . . . . . . . . 13
85	84	ad2antrl 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
86		frn 5688	. . . . . . . . . . . 12
87	85, 86	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88		ressxr 9628	. . . . . . . . . . 11
89	87, 88	syl6ss 3412	. . . . . . . . . 10 $/\$ $/\$ $/\$
90		supxrcl 11544	. . . . . . . . . 10
91	89, 90	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
92	79, 91	syl5eqelr 2505	. . . . . . . 8 $/\$ $/\$ $/\$
93		elxr 11360	. . . . . . . . . . 11 $\/$ $\/$
94		simplrl 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95		arch 10810	. . . . . . . . . . . . . . . . . 18
96	94, 95	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
97	5	adantl 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
98	97	breq2d 4371	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
99	98	rexbidv 2872	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
100	96, 99	mpbird 235	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
101	28	adantlr 719	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		simplrl 768	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
103	101, 102	resubcld 9991	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104		simplrr 769	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
105	102, 101	posdifd 10144	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
106	104, 105	mpbid 213	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
107		nnrecl 10811	. . . . . . . . . . . . . . . . . 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 10039	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
113	109, 110, 111, 112	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
114	9	ad2antlr 731	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
115	114	breq2d 4371	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
116	113, 115	bitr4d 259	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
117	116	rexbidva 2869	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	108, 117	mpbid 213	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	100, 118	pm2.61dan 798	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	expr 618	. . . . . . . . . . . . . 14 $/\$
121		rexr 9630	. . . . . . . . . . . . . . 15
122		xrltnle 9645	. . . . . . . . . . . . . . 15 $/\$
123	121, 11, 122	syl2anr 480	. . . . . . . . . . . . . 14 $/\$
124	121	ad2antlr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
125	40	adantlr 719	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
126		xrltnle 9645	. . . . . . . . . . . . . . . . 17 $/\$
127	124, 125, 126	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	127	rexbidva 2869	. . . . . . . . . . . . . . 15 $/\$
129		rexnal 2807	. . . . . . . . . . . . . . 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 11376	. . . . . . . . . . . . . . 15
135	133, 134	syl 17	. . . . . . . . . . . . . 14 $/\$
136		simpr 462	. . . . . . . . . . . . . 14 $/\$
137	135, 136	breqtrrd 4386	. . . . . . . . . . . . 13 $/\$
138	137	a1d 26	. . . . . . . . . . . 12 $/\$
139		1nn 10564	. . . . . . . . . . . . . . 15
140	139	ne0ii 3704	. . . . . . . . . . . . . 14
141		r19.2z 3824	. . . . . . . . . . . . . 14 $/\$
142	140, 141	mpan 674	. . . . . . . . . . . . 13
143	39	adantlr 719	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		mnflt 11369	. . . . . . . . . . . . . . . . . 18
145		rexr 9630	. . . . . . . . . . . . . . . . . . 19
146		xrltnle 9645	. . . . . . . . . . . . . . . . . . 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 4371	. . . . . . . . . . . . . . . 16 $/\$ $/\$
152	149, 151	mtbird 302	. . . . . . . . . . . . . . 15 $/\$ $/\$
153	152	nrexdv 2814	. . . . . . . . . . . . . 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 2773	. . . . . . . . 9
159	158	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$
160	40	adantlr 719	. . . . . . . . . . . . 13 $/\$ $/\$
161	82	adantll 718	. . . . . . . . . . . . . 14 $/\$ $/\$
162	161	rexrd 9634	. . . . . . . . . . . . 13 $/\$ $/\$
163		xrltle 11392	. . . . . . . . . . . . 13 $/\$
164	160, 162, 163	syl2anc 665	. . . . . . . . . . . 12 $/\$ $/\$
165	84	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$
166	165, 86	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
167	166, 88	syl6ss 3412	. . . . . . . . . . . . . . . 16 $/\$
168	167	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
169	78, 168	syl5eqssr 3445	. . . . . . . . . . . . . 14 $/\$ $/\$
170		fveq2 5818	. . . . . . . . . . . . . . . . . 18
171	170	fveq2d 5822	. . . . . . . . . . . . . . . . 17
172		eqid 2422	. . . . . . . . . . . . . . . . 17
173		fvex 5828	. . . . . . . . . . . . . . . . 17
174	171, 172, 173	fvmpt 5901	. . . . . . . . . . . . . . . 16
175		fvex 5828	. . . . . . . . . . . . . . . . . 18
176	175, 172	fnmpti 5660	. . . . . . . . . . . . . . . . 17
177		fnfvelrn 5971	. . . . . . . . . . . . . . . . 17 $/\$
178	176, 177	mpan 674	. . . . . . . . . . . . . . . 16
179	174, 178	eqeltrrd 2501	. . . . . . . . . . . . . . 15
180	179	adantl 467	. . . . . . . . . . . . . 14 $/\$ $/\$
181		supxrub 11554	. . . . . . . . . . . . . 14 $/\$
182	169, 180, 181	syl2anc 665	. . . . . . . . . . . . 13 $/\$ $/\$
183	168, 90	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
184	79, 183	syl5eqelr 2505	. . . . . . . . . . . . . 14 $/\$ $/\$
185		xrletr 11399	. . . . . . . . . . . . . 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 2767	. . . . . . . . 9 $/\$ $/\$
191	190	impr 623	. . . . . . . 8 $/\$ $/\$ $/\$
192		breq2 4363	. . . . . . . . . . 11
193	192	ralbidv 2798	. . . . . . . . . 10
194		breq2 4363	. . . . . . . . . 10
195	193, 194	imbi12d 321	. . . . . . . . 9
196	195	rspcv 3114	. . . . . . . 8
197	92, 159, 191, 196	syl3c 63	. . . . . . 7 $/\$ $/\$ $/\$
198	197, 79	syl6breqr 4400	. . . . . 6 $/\$ $/\$ $/\$
199		itg2ub 22626	. . . . . . . . . . . . . . 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 2767	. . . . . . . . . 10 $/\$ $/\$
205	204	impr 623	. . . . . . . . 9 $/\$ $/\$ $/\$
206	76, 83, 175	fvmpt 5901	. . . . . . . . . . . 12
207	206	breq1d 4369	. . . . . . . . . . 11
208	207	ralbiia 2789	. . . . . . . . . 10
209	76	breq1d 4369	. . . . . . . . . . 11
210	209	cbvralv 2990	. . . . . . . . . 10
211	208, 210	bitr4i 255	. . . . . . . . 9
212	205, 211	sylibr 215	. . . . . . . 8 $/\$ $/\$ $/\$
213		ffn 5682	. . . . . . . . 9
214		breq1 4362	. . . . . . . . . 10
215	214	ralrn 5977	. . . . . . . . 9
216	85, 213, 215	3syl 18	. . . . . . . 8 $/\$ $/\$ $/\$
217	212, 216	mpbird 235	. . . . . . 7 $/\$ $/\$ $/\$
218	11	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$
219		supxrleub 11556	. . . . . . . 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 11395	. . . . . . . 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 1758	. 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 1657

wcel 1872

wne 2593

wral 2708

wrex 2709

wss 3372

c0 3697

cif 3847 class class class wbr 4359

cmpt 4418

cdm 4789

crn 4790

wfn 5532

wf 5533

cfv 5537 (class class class)co 6242

cofr 6481

cmap 7420

csup 7900

cr 9482

cc0 9483

c1 9484

cpnf 9616

cmnf 9617

cxr 9618

clt 9619

cle 9620

cmin 9804

cdiv 10213

cn 10553

crp 11246

cicc 11582

citg1 22508

citg2 22509

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2058 ax-ext 2402 ax-rep 4472 ax-sep 4482 ax-nul 4491 ax-pow 4538 ax-pr 4596 ax-un 6534 ax-inf2 8092 ax-cc 8809 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560 ax-pre-sup 9561

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 1658 df-nf 1662 df-sb 1791 df-eu 2274 df-mo 2275 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2552 df-ne 2595 df-nel 2596 df-ral 2713 df-rex 2714 df-reu 2715 df-rmo 2716 df-rab 2717 df-v 3018 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-pss 3388 df-nul 3698 df-if 3848 df-pw 3919 df-sn 3935 df-pr 3937 df-tp 3939 df-op 3941 df-uni 4156 df-int 4192 df-iun 4237 df-br 4360 df-opab 4419 df-mpt 4420 df-tr 4455 df-eprel 4700 df-id 4704 df-po 4710 df-so 4711 df-fr 4748 df-se 4749 df-we 4750 df-xp 4795 df-rel 4796 df-cnv 4797 df-co 4798 df-dm 4799 df-rn 4800 df-res 4801 df-ima 4802 df-pred 5335 df-ord 5381 df-on 5382 df-lim 5383 df-suc 5384 df-iota 5501 df-fun 5539 df-fn 5540 df-f 5541 df-f1 5542 df-fo 5543 df-f1o 5544 df-fv 5545 df-isom 5546 df-riota 6204 df-ov 6245 df-oprab 6246 df-mpt2 6247 df-of 6482 df-ofr 6483 df-om 6644 df-1st 6744 df-2nd 6745 df-wrecs 6976 df-recs 7038 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-en 7518 df-dom 7519 df-sdom 7520 df-fin 7521 df-sup 7902 df-inf 7903 df-oi 7971 df-card 8318 df-cda 8542 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9806 df-neg 9807 df-div 10214 df-nn 10554 df-2 10612 df-3 10613 df-n0 10814 df-z 10882 df-uz 11104 df-q 11209 df-rp 11247 df-xadd 11354 df-ioo 11583 df-ico 11585 df-icc 11586 df-fz 11729 df-fzo 11860 df-fl 11971 df-seq 12157 df-exp 12216 df-hash 12459 df-cj 13099 df-re 13100 df-im 13101 df-sqrt 13235 df-abs 13236 df-clim 13488 df-sum 13689 df-xmet 18899 df-met 18900 df-ovol 22351 df-vol 22353 df-mbf 22512 df-itg1 22513 df-itg2 22514

This theorem is referenced by: (None)

W3C validator