itg2seq - Metamath Proof Explorer

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

Theorem itg2seq 21195

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 21208, 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 10321	. . . . . . . . . . . 12
2	1	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
3		ltpnf 11094	. . . . . . . . . . 11
4	2, 3	syl 16	. . . . . . . . . 10 $/\$ $/\$
5		iftrue 3792	. . . . . . . . . . 11
6	5	adantl 466	. . . . . . . . . 10 $/\$ $/\$
7		simpr 461	. . . . . . . . . 10 $/\$ $/\$
8	4, 6, 7	3brtr4d 4317	. . . . . . . . 9 $/\$ $/\$
9		iffalse 3794	. . . . . . . . . . 11
10	9	adantl 466	. . . . . . . . . 10 $/\$ $/\$
11		itg2cl 21185	. . . . . . . . . . . . . . 15
12		xrrebnd 11132	. . . . . . . . . . . . . . 15 $/\$
13	11, 12	syl 16	. . . . . . . . . . . . . 14 $/\$
14		itg2ge0 21188	. . . . . . . . . . . . . . . 16
15		mnflt0 11097	. . . . . . . . . . . . . . . . 17
16		mnfxr 11086	. . . . . . . . . . . . . . . . . . 19
17		0xr 9422	. . . . . . . . . . . . . . . . . . 19
18		xrltletr 11123	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
19	16, 17, 18	mp3an12 1304	. . . . . . . . . . . . . . . . . 18 $/\$
20	11, 19	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
21	15, 20	mpani 676	. . . . . . . . . . . . . . . 16
22	14, 21	mpd 15	. . . . . . . . . . . . . . 15
23	22	biantrurd 508	. . . . . . . . . . . . . 14 $/\$
24		nltpnft 11130	. . . . . . . . . . . . . . . 16
25	11, 24	syl 16	. . . . . . . . . . . . . . 15
26	25	con2bid 329	. . . . . . . . . . . . . 14
27	13, 23, 26	3bitr2rd 282	. . . . . . . . . . . . 13
28	27	biimpa 484	. . . . . . . . . . . 12 $/\$
29	28	adantlr 714	. . . . . . . . . . 11 $/\$ $/\$
30		nnrp 10992	. . . . . . . . . . . . 13
31	30	rpreccld 11029	. . . . . . . . . . . 12
32	31	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
33	29, 32	ltsubrpd 11047	. . . . . . . . . 10 $/\$ $/\$
34	10, 33	eqbrtrd 4307	. . . . . . . . 9 $/\$ $/\$
35	8, 34	pm2.61dan 789	. . . . . . . 8 $/\$
36		nnrecre 10350	. . . . . . . . . . . . 13
37	36	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$
38	29, 37	resubcld 9768	. . . . . . . . . . 11 $/\$ $/\$
39	2, 38	ifclda 3816	. . . . . . . . . 10 $/\$
40	39	rexrd 9425	. . . . . . . . 9 $/\$
41	11	adantr 465	. . . . . . . . 9 $/\$
42		xrltnle 9435	. . . . . . . . 9 $/\$
43	40, 41, 42	syl2anc 661	. . . . . . . 8 $/\$
44	35, 43	mpbid 210	. . . . . . 7 $/\$
45		itg2leub 21187	. . . . . . . 8 $/\$
46	40, 45	syldan 470	. . . . . . 7 $/\$
47	44, 46	mtbid 300	. . . . . 6 $/\$
48		rexanali 2756	. . . . . 6 $/\$
49	47, 48	sylibr 212	. . . . 5 $/\$ $/\$
50		itg1cl 21138	. . . . . . . 8
51		ltnle 9446	. . . . . . . 8 $/\$
52	39, 50, 51	syl2an 477	. . . . . . 7 $/\$ $/\$
53	52	anbi2d 703	. . . . . 6 $/\$ $/\$ $/\$ $/\$
54	53	rexbidva 2727	. . . . 5 $/\$ $/\$ $/\$
55	49, 54	mpbird 232	. . . 4 $/\$ $/\$
56	55	ralrimiva 2794	. . 3 $/\$
57		ovex 6111	. . . . 5
58		i1ff 21129	. . . . . . 7
59		reex 9365	. . . . . . . 8
60	59, 59	elmap 7233	. . . . . . 7
61	58, 60	sylibr 212	. . . . . 6
62	61	ssriv 3355	. . . . 5
63	57, 62	ssexi 4432	. . . 4
64		nnenom 11794	. . . 4
65		breq1 4290	. . . . 5
66		fveq2 5686	. . . . . 6
67	66	breq2d 4299	. . . . 5
68	65, 67	anbi12d 710	. . . 4 $/\$ $/\$
69	63, 64, 68	axcc4 8600	. . 3 $/\$ $/\$ $/\$
70	56, 69	syl 16	. 2 $/\$ $/\$
71		simprl 755	. . . . 5 $/\$ $/\$ $/\$
72		simpl 457	. . . . . . 7 $/\$
73	72	ralimi 2786	. . . . . 6 $/\$
74	73	ad2antll 728	. . . . 5 $/\$ $/\$ $/\$
75		fveq2 5686	. . . . . . . . . . . . 13
76	75	fveq2d 5690	. . . . . . . . . . . 12
77	76	cbvmptv 4378	. . . . . . . . . . 11
78	77	rneqi 5061	. . . . . . . . . 10
79	78	supeq1i 7689	. . . . . . . . 9
80		ffvelrn 5836	. . . . . . . . . . . . . . 15 $/\$
81		itg1cl 21138	. . . . . . . . . . . . . . 15
82	80, 81	syl 16	. . . . . . . . . . . . . 14 $/\$
83		eqid 2438	. . . . . . . . . . . . . 14
84	82, 83	fmptd 5862	. . . . . . . . . . . . 13
85	84	ad2antrl 727	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
86		frn 5560	. . . . . . . . . . . 12
87	85, 86	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88		ressxr 9419	. . . . . . . . . . 11
89	87, 88	syl6ss 3363	. . . . . . . . . 10 $/\$ $/\$ $/\$
90		supxrcl 11269	. . . . . . . . . 10
91	89, 90	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
92	79, 91	syl5eqelr 2523	. . . . . . . 8 $/\$ $/\$ $/\$
93		elxr 11088	. . . . . . . . . . 11 $\/$ $\/$
94		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95		arch 10568	. . . . . . . . . . . . . . . . . 18
96	94, 95	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
97	5	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
98	97	breq2d 4299	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
99	98	rexbidv 2731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
100	96, 99	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
101	28	adantlr 714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
103	101, 102	resubcld 9768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104		simplrr 760	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
105	102, 101	posdifd 9918	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
106	104, 105	mpbid 210	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
107		nnrecl 10569	. . . . . . . . . . . . . . . . . 18 $/\$
108	103, 106, 107	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
109	36	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
110	101	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
111	102	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
112		ltsub13 9812	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
113	109, 110, 111, 112	syl3anc 1218	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
114	9	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
115	114	breq2d 4299	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
116	113, 115	bitr4d 256	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
117	116	rexbidva 2727	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	108, 117	mpbid 210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	100, 118	pm2.61dan 789	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	expr 615	. . . . . . . . . . . . . 14 $/\$
121		rexr 9421	. . . . . . . . . . . . . . 15
122		xrltnle 9435	. . . . . . . . . . . . . . 15 $/\$
123	121, 11, 122	syl2anr 478	. . . . . . . . . . . . . 14 $/\$
124	121	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
125	40	adantlr 714	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
126		xrltnle 9435	. . . . . . . . . . . . . . . . 17 $/\$
127	124, 125, 126	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	127	rexbidva 2727	. . . . . . . . . . . . . . 15 $/\$
129		rexnal 2721	. . . . . . . . . . . . . . 15
130	128, 129	syl6bb 261	. . . . . . . . . . . . . 14 $/\$
131	120, 123, 130	3imtr3d 267	. . . . . . . . . . . . 13 $/\$
132	131	con4d 105	. . . . . . . . . . . 12 $/\$
133	11	adantr 465	. . . . . . . . . . . . . . 15 $/\$
134		pnfge 11102	. . . . . . . . . . . . . . 15
135	133, 134	syl 16	. . . . . . . . . . . . . 14 $/\$
136		simpr 461	. . . . . . . . . . . . . 14 $/\$
137	135, 136	breqtrrd 4313	. . . . . . . . . . . . 13 $/\$
138	137	a1d 25	. . . . . . . . . . . 12 $/\$
139		1nn 10325	. . . . . . . . . . . . . . 15
140		ne0i 3638	. . . . . . . . . . . . . . 15
141	139, 140	ax-mp 5	. . . . . . . . . . . . . 14
142		r19.2z 3764	. . . . . . . . . . . . . 14 $/\$
143	141, 142	mpan 670	. . . . . . . . . . . . 13
144	39	adantlr 714	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
145		mnflt 11096	. . . . . . . . . . . . . . . . . 18
146		rexr 9421	. . . . . . . . . . . . . . . . . . 19
147		xrltnle 9435	. . . . . . . . . . . . . . . . . . 19 $/\$
148	16, 146, 147	sylancr 663	. . . . . . . . . . . . . . . . . 18
149	145, 148	mpbid 210	. . . . . . . . . . . . . . . . 17
150	144, 149	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
151		simplr 754	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
152	151	breq2d 4299	. . . . . . . . . . . . . . . 16 $/\$ $/\$
153	150, 152	mtbird 301	. . . . . . . . . . . . . . 15 $/\$ $/\$
154	153	nrexdv 2814	. . . . . . . . . . . . . 14 $/\$
155	154	pm2.21d 106	. . . . . . . . . . . . 13 $/\$
156	143, 155	syl5 32	. . . . . . . . . . . 12 $/\$
157	132, 138, 156	3jaodan 1284	. . . . . . . . . . 11 $/\$ $\/$ $\/$
158	93, 157	sylan2b 475	. . . . . . . . . 10 $/\$
159	158	ralrimiva 2794	. . . . . . . . 9
160	159	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
161	40	adantlr 714	. . . . . . . . . . . . 13 $/\$ $/\$
162	82	adantll 713	. . . . . . . . . . . . . 14 $/\$ $/\$
163	162	rexrd 9425	. . . . . . . . . . . . 13 $/\$ $/\$
164		xrltle 11118	. . . . . . . . . . . . 13 $/\$
165	161, 163, 164	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
166	84	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
167	166, 86	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
168	167, 88	syl6ss 3363	. . . . . . . . . . . . . . . 16 $/\$
169	168	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
170	78, 169	syl5eqssr 3396	. . . . . . . . . . . . . 14 $/\$ $/\$
171		fveq2 5686	. . . . . . . . . . . . . . . . . 18
172	171	fveq2d 5690	. . . . . . . . . . . . . . . . 17
173		eqid 2438	. . . . . . . . . . . . . . . . 17
174		fvex 5696	. . . . . . . . . . . . . . . . 17
175	172, 173, 174	fvmpt 5769	. . . . . . . . . . . . . . . 16
176		fvex 5696	. . . . . . . . . . . . . . . . . 18
177	176, 173	fnmpti 5534	. . . . . . . . . . . . . . . . 17
178		fnfvelrn 5835	. . . . . . . . . . . . . . . . 17 $/\$
179	177, 178	mpan 670	. . . . . . . . . . . . . . . 16
180	175, 179	eqeltrrd 2513	. . . . . . . . . . . . . . 15
181	180	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
182		supxrub 11279	. . . . . . . . . . . . . 14 $/\$
183	170, 181, 182	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$
184	169, 90	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
185	79, 184	syl5eqelr 2523	. . . . . . . . . . . . . 14 $/\$ $/\$
186		xrletr 11124	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187	161, 163, 185, 186	syl3anc 1218	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	183, 187	mpan2d 674	. . . . . . . . . . . 12 $/\$ $/\$
189	165, 188	syld 44	. . . . . . . . . . 11 $/\$ $/\$
190	189	adantld 467	. . . . . . . . . 10 $/\$ $/\$ $/\$
191	190	ralimdva 2789	. . . . . . . . 9 $/\$ $/\$
192	191	impr 619	. . . . . . . 8 $/\$ $/\$ $/\$
193		breq2 4291	. . . . . . . . . . 11
194	193	ralbidv 2730	. . . . . . . . . 10
195		breq2 4291	. . . . . . . . . 10
196	194, 195	imbi12d 320	. . . . . . . . 9
197	196	rspcv 3064	. . . . . . . 8
198	92, 160, 192, 197	syl3c 61	. . . . . . 7 $/\$ $/\$ $/\$
199	198, 79	syl6breqr 4327	. . . . . 6 $/\$ $/\$ $/\$
200		itg2ub 21186	. . . . . . . . . . . . . . 15 $/\$ $/\$
201	200	3expia 1189	. . . . . . . . . . . . . 14 $/\$
202	80, 201	sylan2 474	. . . . . . . . . . . . 13 $/\$ $/\$
203	202	anassrs 648	. . . . . . . . . . . 12 $/\$ $/\$
204	203	adantrd 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$
205	204	ralimdva 2789	. . . . . . . . . 10 $/\$ $/\$
206	205	impr 619	. . . . . . . . 9 $/\$ $/\$ $/\$
207	76, 83, 176	fvmpt 5769	. . . . . . . . . . . 12
208	207	breq1d 4297	. . . . . . . . . . 11
209	208	ralbiia 2742	. . . . . . . . . 10
210	76	breq1d 4297	. . . . . . . . . . 11
211	210	cbvralv 2942	. . . . . . . . . 10
212	209, 211	bitr4i 252	. . . . . . . . 9
213	206, 212	sylibr 212	. . . . . . . 8 $/\$ $/\$ $/\$
214		ffn 5554	. . . . . . . . 9
215		breq1 4290	. . . . . . . . . 10
216	215	ralrn 5841	. . . . . . . . 9
217	85, 214, 216	3syl 20	. . . . . . . 8 $/\$ $/\$ $/\$
218	213, 217	mpbird 232	. . . . . . 7 $/\$ $/\$ $/\$
219	11	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
220		supxrleub 11281	. . . . . . . 8 $/\$
221	89, 219, 220	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
222	218, 221	mpbird 232	. . . . . 6 $/\$ $/\$ $/\$
223	11	adantr 465	. . . . . . . 8 $/\$
224	168, 90	syl 16	. . . . . . . 8 $/\$
225		xrletri3 11121	. . . . . . . 8 $/\$ $/\$
226	223, 224, 225	syl2anc 661	. . . . . . 7 $/\$ $/\$
227	226	adantrr 716	. . . . . 6 $/\$ $/\$ $/\$ $/\$
228	199, 222, 227	mpbir2and 913	. . . . 5 $/\$ $/\$ $/\$
229	71, 74, 228	3jca 1168	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
230	229	ex 434	. . 3 $/\$ $/\$ $/\$ $/\$
231	230	eximdv 1676	. 2 $/\$ $/\$ $/\$ $/\$
232	70, 231	mpd 15	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $\/$ w3o 964 $/\$ w3a 965

wceq 1369

wex 1586

wcel 1756

wne 2601

wral 2710

wrex 2711

wss 3323

c0 3632

cif 3786 class class class wbr 4287

cmpt 4345

cdm 4835

crn 4836

wfn 5408

wf 5409

cfv 5413 (class class class)co 6086

cofr 6314

cmap 7206

csup 7682

cr 9273

cc0 9274

c1 9275

cpnf 9407

cmnf 9408

cxr 9409

clt 9410

cle 9411

cmin 9587

cdiv 9985

cn 10314

crp 10983

cicc 11295

citg1 21070

citg2 21071

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cc 8596 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 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-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-ofr 6316 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-map 7208 df-pm 7209 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-sup 7683 df-oi 7716 df-card 8101 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-n0 10572 df-z 10639 df-uz 10854 df-q 10946 df-rp 10984 df-xadd 11082 df-ioo 11296 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-fl 11634 df-seq 11799 df-exp 11858 df-hash 12096 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-clim 12958 df-sum 13156 df-xmet 17785 df-met 17786 df-ovol 20923 df-vol 20924 df-mbf 21074 df-itg1 21075 df-itg2 21076

This theorem is referenced by: (None)

W3C validator