itg2seq - Metamath Proof Explorer

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

Theorem itg2seq 21346

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 21359, 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 10433	. . . . . . . . . . . 12
2	1	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
3		ltpnf 11206	. . . . . . . . . . 11
4	2, 3	syl 16	. . . . . . . . . 10 $/\$ $/\$
5		iftrue 3898	. . . . . . . . . . 11
6	5	adantl 466	. . . . . . . . . 10 $/\$ $/\$
7		simpr 461	. . . . . . . . . 10 $/\$ $/\$
8	4, 6, 7	3brtr4d 4423	. . . . . . . . 9 $/\$ $/\$
9		iffalse 3900	. . . . . . . . . . 11
10	9	adantl 466	. . . . . . . . . 10 $/\$ $/\$
11		itg2cl 21336	. . . . . . . . . . . . . . 15
12		xrrebnd 11244	. . . . . . . . . . . . . . 15 $/\$
13	11, 12	syl 16	. . . . . . . . . . . . . 14 $/\$
14		itg2ge0 21339	. . . . . . . . . . . . . . . 16
15		mnflt0 11209	. . . . . . . . . . . . . . . . 17
16		mnfxr 11198	. . . . . . . . . . . . . . . . . . 19
17		0xr 9534	. . . . . . . . . . . . . . . . . . 19
18		xrltletr 11235	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
19	16, 17, 18	mp3an12 1305	. . . . . . . . . . . . . . . . . 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 11242	. . . . . . . . . . . . . . . 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 11104	. . . . . . . . . . . . 13
31	30	rpreccld 11141	. . . . . . . . . . . 12
32	31	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
33	29, 32	ltsubrpd 11159	. . . . . . . . . 10 $/\$ $/\$
34	10, 33	eqbrtrd 4413	. . . . . . . . 9 $/\$ $/\$
35	8, 34	pm2.61dan 789	. . . . . . . 8 $/\$
36		nnrecre 10462	. . . . . . . . . . . . 13
37	36	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$
38	29, 37	resubcld 9880	. . . . . . . . . . 11 $/\$ $/\$
39	2, 38	ifclda 3922	. . . . . . . . . 10 $/\$
40	39	rexrd 9537	. . . . . . . . 9 $/\$
41	11	adantr 465	. . . . . . . . 9 $/\$
42		xrltnle 9547	. . . . . . . . 9 $/\$
43	40, 41, 42	syl2anc 661	. . . . . . . 8 $/\$
44	35, 43	mpbid 210	. . . . . . 7 $/\$
45		itg2leub 21338	. . . . . . . 8 $/\$
46	40, 45	syldan 470	. . . . . . 7 $/\$
47	44, 46	mtbid 300	. . . . . 6 $/\$
48		rexanali 2875	. . . . . 6 $/\$
49	47, 48	sylibr 212	. . . . 5 $/\$ $/\$
50		itg1cl 21289	. . . . . . . 8
51		ltnle 9558	. . . . . . . 8 $/\$
52	39, 50, 51	syl2an 477	. . . . . . 7 $/\$ $/\$
53	52	anbi2d 703	. . . . . 6 $/\$ $/\$ $/\$ $/\$
54	53	rexbidva 2852	. . . . 5 $/\$ $/\$ $/\$
55	49, 54	mpbird 232	. . . 4 $/\$ $/\$
56	55	ralrimiva 2825	. . 3 $/\$
57		ovex 6218	. . . . 5
58		i1ff 21280	. . . . . . 7
59		reex 9477	. . . . . . . 8
60	59, 59	elmap 7344	. . . . . . 7
61	58, 60	sylibr 212	. . . . . 6
62	61	ssriv 3461	. . . . 5
63	57, 62	ssexi 4538	. . . 4
64		nnenom 11912	. . . 4
65		breq1 4396	. . . . 5
66		fveq2 5792	. . . . . 6
67	66	breq2d 4405	. . . . 5
68	65, 67	anbi12d 710	. . . 4 $/\$ $/\$
69	63, 64, 68	axcc4 8712	. . 3 $/\$ $/\$ $/\$
70	56, 69	syl 16	. 2 $/\$ $/\$
71		simprl 755	. . . . 5 $/\$ $/\$ $/\$
72		simpl 457	. . . . . . 7 $/\$
73	72	ralimi 2814	. . . . . 6 $/\$
74	73	ad2antll 728	. . . . 5 $/\$ $/\$ $/\$
75		fveq2 5792	. . . . . . . . . . . . 13
76	75	fveq2d 5796	. . . . . . . . . . . 12
77	76	cbvmptv 4484	. . . . . . . . . . 11
78	77	rneqi 5167	. . . . . . . . . 10
79	78	supeq1i 7801	. . . . . . . . 9
80		ffvelrn 5943	. . . . . . . . . . . . . . 15 $/\$
81		itg1cl 21289	. . . . . . . . . . . . . . 15
82	80, 81	syl 16	. . . . . . . . . . . . . 14 $/\$
83		eqid 2451	. . . . . . . . . . . . . 14
84	82, 83	fmptd 5969	. . . . . . . . . . . . 13
85	84	ad2antrl 727	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
86		frn 5666	. . . . . . . . . . . 12
87	85, 86	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88		ressxr 9531	. . . . . . . . . . 11
89	87, 88	syl6ss 3469	. . . . . . . . . 10 $/\$ $/\$ $/\$
90		supxrcl 11381	. . . . . . . . . 10
91	89, 90	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
92	79, 91	syl5eqelr 2544	. . . . . . . 8 $/\$ $/\$ $/\$
93		elxr 11200	. . . . . . . . . . 11 $\/$ $\/$
94		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95		arch 10680	. . . . . . . . . . . . . . . . . 18
96	94, 95	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
97	5	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
98	97	breq2d 4405	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
99	98	rexbidv 2855	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
100	96, 99	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
101	28	adantlr 714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
103	101, 102	resubcld 9880	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104		simplrr 760	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
105	102, 101	posdifd 10030	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
106	104, 105	mpbid 210	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
107		nnrecl 10681	. . . . . . . . . . . . . . . . . 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 9924	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
113	109, 110, 111, 112	syl3anc 1219	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
114	9	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
115	114	breq2d 4405	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
116	113, 115	bitr4d 256	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
117	116	rexbidva 2852	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	108, 117	mpbid 210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	100, 118	pm2.61dan 789	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	119	expr 615	. . . . . . . . . . . . . 14 $/\$
121		rexr 9533	. . . . . . . . . . . . . . 15
122		xrltnle 9547	. . . . . . . . . . . . . . 15 $/\$
123	121, 11, 122	syl2anr 478	. . . . . . . . . . . . . 14 $/\$
124	121	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
125	40	adantlr 714	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
126		xrltnle 9547	. . . . . . . . . . . . . . . . 17 $/\$
127	124, 125, 126	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
128	127	rexbidva 2852	. . . . . . . . . . . . . . 15 $/\$
129		rexnal 2847	. . . . . . . . . . . . . . 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 11214	. . . . . . . . . . . . . . 15
135	133, 134	syl 16	. . . . . . . . . . . . . 14 $/\$
136		simpr 461	. . . . . . . . . . . . . 14 $/\$
137	135, 136	breqtrrd 4419	. . . . . . . . . . . . 13 $/\$
138	137	a1d 25	. . . . . . . . . . . 12 $/\$
139		1nn 10437	. . . . . . . . . . . . . . 15
140		ne0i 3744	. . . . . . . . . . . . . . 15
141	139, 140	ax-mp 5	. . . . . . . . . . . . . 14
142		r19.2z 3870	. . . . . . . . . . . . . 14 $/\$
143	141, 142	mpan 670	. . . . . . . . . . . . 13
144	39	adantlr 714	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
145		mnflt 11208	. . . . . . . . . . . . . . . . . 18
146		rexr 9533	. . . . . . . . . . . . . . . . . . 19
147		xrltnle 9547	. . . . . . . . . . . . . . . . . . 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 4405	. . . . . . . . . . . . . . . 16 $/\$ $/\$
153	150, 152	mtbird 301	. . . . . . . . . . . . . . 15 $/\$ $/\$
154	153	nrexdv 2918	. . . . . . . . . . . . . 14 $/\$
155	154	pm2.21d 106	. . . . . . . . . . . . 13 $/\$
156	143, 155	syl5 32	. . . . . . . . . . . 12 $/\$
157	132, 138, 156	3jaodan 1285	. . . . . . . . . . 11 $/\$ $\/$ $\/$
158	93, 157	sylan2b 475	. . . . . . . . . 10 $/\$
159	158	ralrimiva 2825	. . . . . . . . 9
160	159	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
161	40	adantlr 714	. . . . . . . . . . . . 13 $/\$ $/\$
162	82	adantll 713	. . . . . . . . . . . . . 14 $/\$ $/\$
163	162	rexrd 9537	. . . . . . . . . . . . 13 $/\$ $/\$
164		xrltle 11230	. . . . . . . . . . . . 13 $/\$
165	161, 163, 164	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
166	84	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
167	166, 86	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
168	167, 88	syl6ss 3469	. . . . . . . . . . . . . . . 16 $/\$
169	168	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
170	78, 169	syl5eqssr 3502	. . . . . . . . . . . . . 14 $/\$ $/\$
171		fveq2 5792	. . . . . . . . . . . . . . . . . 18
172	171	fveq2d 5796	. . . . . . . . . . . . . . . . 17
173		eqid 2451	. . . . . . . . . . . . . . . . 17
174		fvex 5802	. . . . . . . . . . . . . . . . 17
175	172, 173, 174	fvmpt 5876	. . . . . . . . . . . . . . . 16
176		fvex 5802	. . . . . . . . . . . . . . . . . 18
177	176, 173	fnmpti 5640	. . . . . . . . . . . . . . . . 17
178		fnfvelrn 5942	. . . . . . . . . . . . . . . . 17 $/\$
179	177, 178	mpan 670	. . . . . . . . . . . . . . . 16
180	175, 179	eqeltrrd 2540	. . . . . . . . . . . . . . 15
181	180	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
182		supxrub 11391	. . . . . . . . . . . . . 14 $/\$
183	170, 181, 182	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$
184	169, 90	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
185	79, 184	syl5eqelr 2544	. . . . . . . . . . . . . 14 $/\$ $/\$
186		xrletr 11236	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187	161, 163, 185, 186	syl3anc 1219	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	183, 187	mpan2d 674	. . . . . . . . . . . 12 $/\$ $/\$
189	165, 188	syld 44	. . . . . . . . . . 11 $/\$ $/\$
190	189	adantld 467	. . . . . . . . . 10 $/\$ $/\$ $/\$
191	190	ralimdva 2827	. . . . . . . . 9 $/\$ $/\$
192	191	impr 619	. . . . . . . 8 $/\$ $/\$ $/\$
193		breq2 4397	. . . . . . . . . . 11
194	193	ralbidv 2841	. . . . . . . . . 10
195		breq2 4397	. . . . . . . . . 10
196	194, 195	imbi12d 320	. . . . . . . . 9
197	196	rspcv 3168	. . . . . . . 8
198	92, 160, 192, 197	syl3c 61	. . . . . . 7 $/\$ $/\$ $/\$
199	198, 79	syl6breqr 4433	. . . . . 6 $/\$ $/\$ $/\$
200		itg2ub 21337	. . . . . . . . . . . . . . 15 $/\$ $/\$
201	200	3expia 1190	. . . . . . . . . . . . . 14 $/\$
202	80, 201	sylan2 474	. . . . . . . . . . . . 13 $/\$ $/\$
203	202	anassrs 648	. . . . . . . . . . . 12 $/\$ $/\$
204	203	adantrd 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$
205	204	ralimdva 2827	. . . . . . . . . 10 $/\$ $/\$
206	205	impr 619	. . . . . . . . 9 $/\$ $/\$ $/\$
207	76, 83, 176	fvmpt 5876	. . . . . . . . . . . 12
208	207	breq1d 4403	. . . . . . . . . . 11
209	208	ralbiia 2833	. . . . . . . . . 10
210	76	breq1d 4403	. . . . . . . . . . 11
211	210	cbvralv 3046	. . . . . . . . . 10
212	209, 211	bitr4i 252	. . . . . . . . 9
213	206, 212	sylibr 212	. . . . . . . 8 $/\$ $/\$ $/\$
214		ffn 5660	. . . . . . . . 9
215		breq1 4396	. . . . . . . . . 10
216	215	ralrn 5948	. . . . . . . . 9
217	85, 214, 216	3syl 20	. . . . . . . 8 $/\$ $/\$ $/\$
218	213, 217	mpbird 232	. . . . . . 7 $/\$ $/\$ $/\$
219	11	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
220		supxrleub 11393	. . . . . . . 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 11233	. . . . . . . 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 1677	. 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 1370

wex 1587

wcel 1758

wne 2644

wral 2795

wrex 2796

wss 3429

c0 3738

cif 3892 class class class wbr 4393

cmpt 4451

cdm 4941

crn 4942

wfn 5514

wf 5515

cfv 5519 (class class class)co 6193

cofr 6422

cmap 7317

csup 7794

cr 9385

cc0 9386

c1 9387

cpnf 9519

cmnf 9520

cxr 9521

clt 9522

cle 9523

cmin 9699

cdiv 10097

cn 10426

crp 11095

cicc 11407

citg1 21221

citg2 21222

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4504 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 ax-inf2 7951 ax-cc 8708 ax-cnex 9442 ax-resscn 9443 ax-1cn 9444 ax-icn 9445 ax-addcl 9446 ax-addrcl 9447 ax-mulcl 9448 ax-mulrcl 9449 ax-mulcom 9450 ax-addass 9451 ax-mulass 9452 ax-distr 9453 ax-i2m1 9454 ax-1ne0 9455 ax-1rid 9456 ax-rnegex 9457 ax-rrecex 9458 ax-cnre 9459 ax-pre-lttri 9460 ax-pre-lttrn 9461 ax-pre-ltadd 9462 ax-pre-mulgt0 9463 ax-pre-sup 9464

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-int 4230 df-iun 4274 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-se 4781 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-isom 5528 df-riota 6154 df-ov 6196 df-oprab 6197 df-mpt2 6198 df-of 6423 df-ofr 6424 df-om 6580 df-1st 6680 df-2nd 6681 df-recs 6935 df-rdg 6969 df-1o 7023 df-2o 7024 df-oadd 7027 df-er 7204 df-map 7319 df-pm 7320 df-en 7414 df-dom 7415 df-sdom 7416 df-fin 7417 df-sup 7795 df-oi 7828 df-card 8213 df-cda 8441 df-pnf 9524 df-mnf 9525 df-xr 9526 df-ltxr 9527 df-le 9528 df-sub 9701 df-neg 9702 df-div 10098 df-nn 10427 df-2 10484 df-3 10485 df-n0 10684 df-z 10751 df-uz 10966 df-q 11058 df-rp 11096 df-xadd 11194 df-ioo 11408 df-ico 11410 df-icc 11411 df-fz 11548 df-fzo 11659 df-fl 11752 df-seq 11917 df-exp 11976 df-hash 12214 df-cj 12699 df-re 12700 df-im 12701 df-sqr 12835 df-abs 12836 df-clim 13077 df-sum 13275 df-xmet 17928 df-met 17929 df-ovol 21073 df-vol 21074 df-mbf 21225 df-itg1 21226 df-itg2 21227

This theorem is referenced by: (None)

W3C validator