itg2seq - Metamath Proof Explorer

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

Theorem itg2seq 21884

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 21897, 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 10539	. . . . . . . . . . . 12
2	1	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
3		ltpnf 11327	. . . . . . . . . . 11
4	2, 3	syl 16	. . . . . . . . . 10 $/\$ $/\$
5		iftrue 3945	. . . . . . . . . . 11
6	5	adantl 466	. . . . . . . . . 10 $/\$ $/\$
7		simpr 461	. . . . . . . . . 10 $/\$ $/\$
8	4, 6, 7	3brtr4d 4477	. . . . . . . . 9 $/\$ $/\$
9		iffalse 3948	. . . . . . . . . . 11
10	9	adantl 466	. . . . . . . . . 10 $/\$ $/\$
11		itg2cl 21874	. . . . . . . . . . . . . . 15
12		xrrebnd 11365	. . . . . . . . . . . . . . 15 $/\$
13	11, 12	syl 16	. . . . . . . . . . . . . 14 $/\$
14		itg2ge0 21877	. . . . . . . . . . . . . . . 16
15		mnflt0 11330	. . . . . . . . . . . . . . . . 17
16		mnfxr 11319	. . . . . . . . . . . . . . . . . . 19
17		0xr 9636	. . . . . . . . . . . . . . . . . . 19
18		xrltletr 11356	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
19	16, 17, 18	mp3an12 1314	. . . . . . . . . . . . . . . . . 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 11363	. . . . . . . . . . . . . . . 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 11225	. . . . . . . . . . . . 13
31	30	rpreccld 11262	. . . . . . . . . . . 12
32	31	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
33	29, 32	ltsubrpd 11280	. . . . . . . . . 10 $/\$ $/\$
34	10, 33	eqbrtrd 4467	. . . . . . . . 9 $/\$ $/\$
35	8, 34	pm2.61dan 789	. . . . . . . 8 $/\$
36		nnrecre 10568	. . . . . . . . . . . . 13
37	36	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$
38	29, 37	resubcld 9983	. . . . . . . . . . 11 $/\$ $/\$
39	2, 38	ifclda 3971	. . . . . . . . . 10 $/\$
40	39	rexrd 9639	. . . . . . . . 9 $/\$
41	11	adantr 465	. . . . . . . . 9 $/\$
42		xrltnle 9649	. . . . . . . . 9 $/\$
43	40, 41, 42	syl2anc 661	. . . . . . . 8 $/\$
44	35, 43	mpbid 210	. . . . . . 7 $/\$
45		itg2leub 21876	. . . . . . . 8 $/\$
46	40, 45	syldan 470	. . . . . . 7 $/\$
47	44, 46	mtbid 300	. . . . . 6 $/\$
48		rexanali 2917	. . . . . 6 $/\$
49	47, 48	sylibr 212	. . . . 5 $/\$ $/\$
50		itg1cl 21827	. . . . . . . 8
51		ltnle 9660	. . . . . . . 8 $/\$
52	39, 50, 51	syl2an 477	. . . . . . 7 $/\$ $/\$
53	52	anbi2d 703	. . . . . 6 $/\$ $/\$ $/\$ $/\$
54	53	rexbidva 2970	. . . . 5 $/\$ $/\$ $/\$
55	49, 54	mpbird 232	. . . 4 $/\$ $/\$
56	55	ralrimiva 2878	. . 3 $/\$
57		ovex 6307	. . . . 5
58		i1ff 21818	. . . . . . 7
59		reex 9579	. . . . . . . 8
60	59, 59	elmap 7444	. . . . . . 7
61	58, 60	sylibr 212	. . . . . 6
62	61	ssriv 3508	. . . . 5
63	57, 62	ssexi 4592	. . . 4
64		nnenom 12054	. . . 4
65		breq1 4450	. . . . 5
66		fveq2 5864	. . . . . 6
67	66	breq2d 4459	. . . . 5
68	65, 67	anbi12d 710	. . . 4 $/\$ $/\$
69	63, 64, 68	axcc4 8815	. . 3 $/\$ $/\$ $/\$
70	56, 69	syl 16	. 2 $/\$ $/\$
71		simprl 755	. . . . 5 $/\$ $/\$ $/\$
72		simpl 457	. . . . . . 7 $/\$
73	72	ralimi 2857	. . . . . 6 $/\$
74	73	ad2antll 728	. . . . 5 $/\$ $/\$ $/\$
75		fveq2 5864	. . . . . . . . . . . . 13
76	75	fveq2d 5868	. . . . . . . . . . . 12
77	76	cbvmptv 4538	. . . . . . . . . . 11
78	77	rneqi 5227	. . . . . . . . . 10
79	78	supeq1i 7903	. . . . . . . . 9
80		ffvelrn 6017	. . . . . . . . . . . . . . 15 $/\$
81		itg1cl 21827	. . . . . . . . . . . . . . 15
82	80, 81	syl 16	. . . . . . . . . . . . . 14 $/\$
83		eqid 2467	. . . . . . . . . . . . . 14
84	82, 83	fmptd 6043	. . . . . . . . . . . . 13
85	84	ad2antrl 727	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
86		frn 5735	. . . . . . . . . . . 12
87	85, 86	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88		ressxr 9633	. . . . . . . . . . 11
89	87, 88	syl6ss 3516	. . . . . . . . . 10 $/\$ $/\$ $/\$
90		supxrcl 11502	. . . . . . . . . 10
91	89, 90	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
92	79, 91	syl5eqelr 2560	. . . . . . . 8 $/\$ $/\$ $/\$
93		elxr 11321	. . . . . . . . . . 11 $\/$ $\/$
94		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95		arch 10788	. . . . . . . . . . . . . . . . . 18
96	94, 95	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
97	5	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
98	97	breq2d 4459	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
99	98	rexbidv 2973	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
100	96, 99	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
101	28	adantlr 714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
103	101, 102	resubcld 9983	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104		simplrr 760	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
105	102, 101	posdifd 10135	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
106	104, 105	mpbid 210	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
107		nnrecl 10789	. . . . . . . . . . . . . . . . . 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 10029	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
113	109, 110, 111, 112	syl3anc 1228	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
114	9	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
115	114	breq2d 4459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
116	113, 115	bitr4d 256	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
117	116	rexbidva 2970	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	108, 117	mpbid 210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	100, 118	pm2.61dan 789	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	expr 615	. . . . . . . . . . . . . 14 $/\$
121		rexr 9635	. . . . . . . . . . . . . . 15
122		xrltnle 9649	. . . . . . . . . . . . . . 15 $/\$
123	121, 11, 122	syl2anr 478	. . . . . . . . . . . . . 14 $/\$
124	121	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
125	40	adantlr 714	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
126		xrltnle 9649	. . . . . . . . . . . . . . . . 17 $/\$
127	124, 125, 126	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	127	rexbidva 2970	. . . . . . . . . . . . . . 15 $/\$
129		rexnal 2912	. . . . . . . . . . . . . . 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 11335	. . . . . . . . . . . . . . 15
135	133, 134	syl 16	. . . . . . . . . . . . . 14 $/\$
136		simpr 461	. . . . . . . . . . . . . 14 $/\$
137	135, 136	breqtrrd 4473	. . . . . . . . . . . . 13 $/\$
138	137	a1d 25	. . . . . . . . . . . 12 $/\$
139		1nn 10543	. . . . . . . . . . . . . . 15
140		ne0i 3791	. . . . . . . . . . . . . . 15
141	139, 140	ax-mp 5	. . . . . . . . . . . . . 14
142		r19.2z 3917	. . . . . . . . . . . . . 14 $/\$
143	141, 142	mpan 670	. . . . . . . . . . . . 13
144	39	adantlr 714	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
145		mnflt 11329	. . . . . . . . . . . . . . . . . 18
146		rexr 9635	. . . . . . . . . . . . . . . . . . 19
147		xrltnle 9649	. . . . . . . . . . . . . . . . . . 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 4459	. . . . . . . . . . . . . . . 16 $/\$ $/\$
153	150, 152	mtbird 301	. . . . . . . . . . . . . . 15 $/\$ $/\$
154	153	nrexdv 2920	. . . . . . . . . . . . . 14 $/\$
155	154	pm2.21d 106	. . . . . . . . . . . . 13 $/\$
156	143, 155	syl5 32	. . . . . . . . . . . 12 $/\$
157	132, 138, 156	3jaodan 1294	. . . . . . . . . . 11 $/\$ $\/$ $\/$
158	93, 157	sylan2b 475	. . . . . . . . . 10 $/\$
159	158	ralrimiva 2878	. . . . . . . . 9
160	159	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
161	40	adantlr 714	. . . . . . . . . . . . 13 $/\$ $/\$
162	82	adantll 713	. . . . . . . . . . . . . 14 $/\$ $/\$
163	162	rexrd 9639	. . . . . . . . . . . . 13 $/\$ $/\$
164		xrltle 11351	. . . . . . . . . . . . 13 $/\$
165	161, 163, 164	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
166	84	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
167	166, 86	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
168	167, 88	syl6ss 3516	. . . . . . . . . . . . . . . 16 $/\$
169	168	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
170	78, 169	syl5eqssr 3549	. . . . . . . . . . . . . 14 $/\$ $/\$
171		fveq2 5864	. . . . . . . . . . . . . . . . . 18
172	171	fveq2d 5868	. . . . . . . . . . . . . . . . 17
173		eqid 2467	. . . . . . . . . . . . . . . . 17
174		fvex 5874	. . . . . . . . . . . . . . . . 17
175	172, 173, 174	fvmpt 5948	. . . . . . . . . . . . . . . 16
176		fvex 5874	. . . . . . . . . . . . . . . . . 18
177	176, 173	fnmpti 5707	. . . . . . . . . . . . . . . . 17
178		fnfvelrn 6016	. . . . . . . . . . . . . . . . 17 $/\$
179	177, 178	mpan 670	. . . . . . . . . . . . . . . 16
180	175, 179	eqeltrrd 2556	. . . . . . . . . . . . . . 15
181	180	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
182		supxrub 11512	. . . . . . . . . . . . . 14 $/\$
183	170, 181, 182	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$
184	169, 90	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
185	79, 184	syl5eqelr 2560	. . . . . . . . . . . . . 14 $/\$ $/\$
186		xrletr 11357	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187	161, 163, 185, 186	syl3anc 1228	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	183, 187	mpan2d 674	. . . . . . . . . . . 12 $/\$ $/\$
189	165, 188	syld 44	. . . . . . . . . . 11 $/\$ $/\$
190	189	adantld 467	. . . . . . . . . 10 $/\$ $/\$ $/\$
191	190	ralimdva 2872	. . . . . . . . 9 $/\$ $/\$
192	191	impr 619	. . . . . . . 8 $/\$ $/\$ $/\$
193		breq2 4451	. . . . . . . . . . 11
194	193	ralbidv 2903	. . . . . . . . . 10
195		breq2 4451	. . . . . . . . . 10
196	194, 195	imbi12d 320	. . . . . . . . 9
197	196	rspcv 3210	. . . . . . . 8
198	92, 160, 192, 197	syl3c 61	. . . . . . 7 $/\$ $/\$ $/\$
199	198, 79	syl6breqr 4487	. . . . . 6 $/\$ $/\$ $/\$
200		itg2ub 21875	. . . . . . . . . . . . . . 15 $/\$ $/\$
201	200	3expia 1198	. . . . . . . . . . . . . 14 $/\$
202	80, 201	sylan2 474	. . . . . . . . . . . . 13 $/\$ $/\$
203	202	anassrs 648	. . . . . . . . . . . 12 $/\$ $/\$
204	203	adantrd 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$
205	204	ralimdva 2872	. . . . . . . . . 10 $/\$ $/\$
206	205	impr 619	. . . . . . . . 9 $/\$ $/\$ $/\$
207	76, 83, 176	fvmpt 5948	. . . . . . . . . . . 12
208	207	breq1d 4457	. . . . . . . . . . 11
209	208	ralbiia 2894	. . . . . . . . . 10
210	76	breq1d 4457	. . . . . . . . . . 11
211	210	cbvralv 3088	. . . . . . . . . 10
212	209, 211	bitr4i 252	. . . . . . . . 9
213	206, 212	sylibr 212	. . . . . . . 8 $/\$ $/\$ $/\$
214		ffn 5729	. . . . . . . . 9
215		breq1 4450	. . . . . . . . . 10
216	215	ralrn 6022	. . . . . . . . 9
217	85, 214, 216	3syl 20	. . . . . . . 8 $/\$ $/\$ $/\$
218	213, 217	mpbird 232	. . . . . . 7 $/\$ $/\$ $/\$
219	11	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
220		supxrleub 11514	. . . . . . . 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 11354	. . . . . . . 8 $/\$ $/\$
226	223, 224, 225	syl2anc 661	. . . . . . 7 $/\$ $/\$
227	226	adantrr 716	. . . . . 6 $/\$ $/\$ $/\$ $/\$
228	199, 222, 227	mpbir2and 920	. . . . 5 $/\$ $/\$ $/\$
229	71, 74, 228	3jca 1176	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
230	229	ex 434	. . 3 $/\$ $/\$ $/\$ $/\$
231	230	eximdv 1686	. 2 $/\$ $/\$ $/\$ $/\$
232	70, 231	mpd 15	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $\/$ w3o 972 $/\$ w3a 973

wceq 1379

wex 1596

wcel 1767

wne 2662

wral 2814

wrex 2815

wss 3476

c0 3785

cif 3939 class class class wbr 4447

cmpt 4505

cdm 4999

crn 5000

wfn 5581

wf 5582

cfv 5586 (class class class)co 6282

cofr 6521

cmap 7417

csup 7896

cr 9487

cc0 9488

c1 9489

cpnf 9621

cmnf 9622

cxr 9623

clt 9624

cle 9625

cmin 9801

cdiv 10202

cn 10532

crp 11216

cicc 11528

citg1 21759

citg2 21760

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cc 8811 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-ofr 6523 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-n0 10792 df-z 10861 df-uz 11079 df-q 11179 df-rp 11217 df-xadd 11315 df-ioo 11529 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-seq 12072 df-exp 12131 df-hash 12370 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-clim 13270 df-sum 13468 df-xmet 18183 df-met 18184 df-ovol 21611 df-vol 21612 df-mbf 21763 df-itg1 21764 df-itg2 21765

This theorem is referenced by: (None)

W3C validator