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

Theorem itg1climres 19598
 Description: Restricting the simple function to the increasing sequence of measurable sets whose union is yields a sequence of simple functions whose integrals approach the integral of . (Contributed by Mario Carneiro, 15-Aug-2014.)
Hypotheses
Ref Expression
itg1climres.1
itg1climres.2
itg1climres.3
itg1climres.4
itg1climres.5
Assertion
Ref Expression
itg1climres
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem itg1climres
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10513 . . 3
2 1z 10303 . . . 4
32a1i 11 . . 3
4 itg1climres.4 . . . . 5
5 i1frn 19561 . . . . 5
64, 5syl 16 . . . 4
7 difss 3466 . . . 4
8 ssfi 7321 . . . 4
96, 7, 8sylancl 644 . . 3
102a1i 11 . . . 4
11 i1fima 19562 . . . . . . . . . . . 12
124, 11syl 16 . . . . . . . . . . 11
1312ad2antrr 707 . . . . . . . . . 10
14 itg1climres.1 . . . . . . . . . . . 12
1514ffvelrnda 5862 . . . . . . . . . . 11
1615adantlr 696 . . . . . . . . . 10
17 inmbl 19428 . . . . . . . . . 10
1813, 16, 17syl2anc 643 . . . . . . . . 9
19 mblvol 19418 . . . . . . . . 9
2018, 19syl 16 . . . . . . . 8
21 inss1 3553 . . . . . . . . . 10
2221a1i 11 . . . . . . . . 9
23 mblss 19419 . . . . . . . . . 10
2413, 23syl 16 . . . . . . . . 9
25 mblvol 19418 . . . . . . . . . . 11
2613, 25syl 16 . . . . . . . . . 10
27 i1fima2sn 19564 . . . . . . . . . . . 12
284, 27sylan 458 . . . . . . . . . . 11
2928adantr 452 . . . . . . . . . 10
3026, 29eqeltrrd 2510 . . . . . . . . 9
31 ovolsscl 19374 . . . . . . . . 9
3222, 24, 30, 31syl3anc 1184 . . . . . . . 8
3320, 32eqeltrd 2509 . . . . . . 7
34 eqid 2435 . . . . . . 7
3533, 34fmptd 5885 . . . . . 6
36 itg1climres.2 . . . . . . . . . . . . 13
3736adantlr 696 . . . . . . . . . . . 12
38 sslin 3559 . . . . . . . . . . . 12
3937, 38syl 16 . . . . . . . . . . 11
4014adantr 452 . . . . . . . . . . . . . 14
41 peano2nn 10004 . . . . . . . . . . . . . 14
42 ffvelrn 5860 . . . . . . . . . . . . . 14
4340, 41, 42syl2an 464 . . . . . . . . . . . . 13
44 inmbl 19428 . . . . . . . . . . . . 13
4513, 43, 44syl2anc 643 . . . . . . . . . . . 12
46 mblss 19419 . . . . . . . . . . . 12
4745, 46syl 16 . . . . . . . . . . 11
48 ovolss 19373 . . . . . . . . . . 11
4939, 47, 48syl2anc 643 . . . . . . . . . 10
50 mblvol 19418 . . . . . . . . . . 11
5145, 50syl 16 . . . . . . . . . 10
5249, 20, 513brtr4d 4234 . . . . . . . . 9
5352ralrimiva 2781 . . . . . . . 8
54 fveq2 5720 . . . . . . . . . . . . . 14
5554ineq2d 3534 . . . . . . . . . . . . 13
5655fveq2d 5724 . . . . . . . . . . . 12
57 fvex 5734 . . . . . . . . . . . 12
5856, 34, 57fvmpt 5798 . . . . . . . . . . 11
59 peano2nn 10004 . . . . . . . . . . . 12
60 fveq2 5720 . . . . . . . . . . . . . . 15
6160ineq2d 3534 . . . . . . . . . . . . . 14
6261fveq2d 5724 . . . . . . . . . . . . 13
63 fvex 5734 . . . . . . . . . . . . 13
6462, 34, 63fvmpt 5798 . . . . . . . . . . . 12
6559, 64syl 16 . . . . . . . . . . 11
6658, 65breq12d 4217 . . . . . . . . . 10
6766ralbiia 2729 . . . . . . . . 9
68 oveq1 6080 . . . . . . . . . . . . . 14
6968fveq2d 5724 . . . . . . . . . . . . 13
7069ineq2d 3534 . . . . . . . . . . . 12
7170fveq2d 5724 . . . . . . . . . . 11
7256, 71breq12d 4217 . . . . . . . . . 10
7372cbvralv 2924 . . . . . . . . 9
7467, 73bitr4i 244 . . . . . . . 8
7553, 74sylibr 204 . . . . . . 7
7675r19.21bi 2796 . . . . . 6
77 ovolss 19373 . . . . . . . . . . 11
7821, 24, 77sylancr 645 . . . . . . . . . 10
7978, 20, 263brtr4d 4234 . . . . . . . . 9
8079ralrimiva 2781 . . . . . . . 8
8158breq1d 4214 . . . . . . . . . 10
8281ralbiia 2729 . . . . . . . . 9
8356breq1d 4214 . . . . . . . . . 10
8483cbvralv 2924 . . . . . . . . 9
8582, 84bitr4i 244 . . . . . . . 8
8680, 85sylibr 204 . . . . . . 7
87 breq2 4208 . . . . . . . . 9
8887ralbidv 2717 . . . . . . . 8
8988rspcev 3044 . . . . . . 7
9028, 86, 89syl2anc 643 . . . . . 6
911, 10, 35, 76, 90climsup 12455 . . . . 5
92 eqid 2435 . . . . . . . 8
9318, 92fmptd 5885 . . . . . . 7
9439ralrimiva 2781 . . . . . . . 8
95 fvex 5734 . . . . . . . . . . . . 13
9695inex2 4337 . . . . . . . . . . . 12
9755, 92, 96fvmpt 5798 . . . . . . . . . . 11
98 fvex 5734 . . . . . . . . . . . . . 14
9998inex2 4337 . . . . . . . . . . . . 13
10061, 92, 99fvmpt 5798 . . . . . . . . . . . 12
10159, 100syl 16 . . . . . . . . . . 11
10297, 101sseq12d 3369 . . . . . . . . . 10
103102ralbiia 2729 . . . . . . . . 9
10455, 70sseq12d 3369 . . . . . . . . . 10
105104cbvralv 2924 . . . . . . . . 9
106103, 105bitr4i 244 . . . . . . . 8
10794, 106sylibr 204 . . . . . . 7
108 volsup 19442 . . . . . . 7
10993, 107, 108syl2anc 643 . . . . . 6
11097iuneq2i 4103 . . . . . . . . . 10
11155cbviunv 4122 . . . . . . . . . 10
112 iunin2 4147 . . . . . . . . . 10
113110, 111, 1123eqtr2i 2461 . . . . . . . . 9
114 ffn 5583 . . . . . . . . . . . . . 14
115 fniunfv 5986 . . . . . . . . . . . . . 14
11614, 114, 1153syl 19 . . . . . . . . . . . . 13
117 itg1climres.3 . . . . . . . . . . . . 13
118116, 117eqtrd 2467 . . . . . . . . . . . 12
119118adantr 452 . . . . . . . . . . 11
120119ineq2d 3534 . . . . . . . . . 10
12112adantr 452 . . . . . . . . . . . 12
122121, 23syl 16 . . . . . . . . . . 11
123 df-ss 3326 . . . . . . . . . . 11
124122, 123sylib 189 . . . . . . . . . 10
125120, 124eqtrd 2467 . . . . . . . . 9
126113, 125syl5eq 2479 . . . . . . . 8
127 ffn 5583 . . . . . . . . 9
128 fniunfv 5986 . . . . . . . . 9
12993, 127, 1283syl 19 . . . . . . . 8
130126, 129eqtr3d 2469 . . . . . . 7
131130fveq2d 5724 . . . . . 6
132 frn 5589 . . . . . . . . 9
13335, 132syl 16 . . . . . . . 8
134 fdm 5587 . . . . . . . . . . 11
13535, 134syl 16 . . . . . . . . . 10
136 1nn 10003 . . . . . . . . . . 11
137 ne0i 3626 . . . . . . . . . . 11
138136, 137mp1i 12 . . . . . . . . . 10
139135, 138eqnetrd 2616 . . . . . . . . 9
140 dm0rn0 5078 . . . . . . . . . 10
141140necon3bii 2630 . . . . . . . . 9
142139, 141sylib 189 . . . . . . . 8
143 ffn 5583 . . . . . . . . . . 11
144 breq1 4207 . . . . . . . . . . . 12
145144ralrn 5865 . . . . . . . . . . 11
14635, 143, 1453syl 19 . . . . . . . . . 10
147146rexbidv 2718 . . . . . . . . 9
14890, 147mpbird 224 . . . . . . . 8
149 supxrre 10898 . . . . . . . 8
150133, 142, 148, 149syl3anc 1184 . . . . . . 7
151 rnco2 5369 . . . . . . . . 9
152 eqidd 2436 . . . . . . . . . . 11
153 volf 19417 . . . . . . . . . . . . 13
154153a1i 11 . . . . . . . . . . . 12
155154feqmptd 5771 . . . . . . . . . . 11
156 fveq2 5720 . . . . . . . . . . 11
15718, 152, 155, 156fmptco 5893 . . . . . . . . . 10
158157rneqd 5089 . . . . . . . . 9
159151, 158syl5reqr 2482 . . . . . . . 8
160159supeq1d 7443 . . . . . . 7
161150, 160eqtr3d 2469 . . . . . 6
162109, 131, 1613eqtr4d 2477 . . . . 5
16391, 162breqtrrd 4230 . . . 4
164 i1ff 19560 . . . . . . . 8
165 frn 5589 . . . . . . . 8
1664, 164, 1653syl 19 . . . . . . 7
167166ssdifssd 3477 . . . . . 6
168167sselda 3340 . . . . 5
169168recnd 9106 . . . 4
170 nnex 9998 . . . . . 6
171170mptex 5958 . . . . 5
172171a1i 11 . . . 4
17335ffvelrnda 5862 . . . . 5
174173recnd 9106 . . . 4
17556oveq2d 6089 . . . . . . 7
176 eqid 2435 . . . . . . 7
177 ovex 6098 . . . . . . 7
178175, 176, 177fvmpt 5798 . . . . . 6
17958oveq2d 6089 . . . . . 6
180178, 179eqtr4d 2470 . . . . 5
181180adantl 453 . . . 4
1821, 10, 163, 169, 172, 174, 181climmulc2 12422 . . 3
183170mptex 5958 . . . 4
184183a1i 11 . . 3
185168adantr 452 . . . . . . . 8
186185, 33remulcld 9108 . . . . . . 7
187186, 176fmptd 5885 . . . . . 6
188187ffvelrnda 5862 . . . . 5
189188recnd 9106 . . . 4
190189anasss 629 . . 3
1914adantr 452 . . . . . . . . 9
192 itg1climres.5 . . . . . . . . . 10
193192i1fres 19589 . . . . . . . . 9
194191, 15, 193syl2anc 643 . . . . . . . 8
1959adantr 452 . . . . . . . 8
196 ffn 5583 . . . . . . . . . . . . . 14
1974, 164, 1963syl 19 . . . . . . . . . . . . 13
198197adantr 452 . . . . . . . . . . . 12
199 fnfvelrn 5859 . . . . . . . . . . . 12
200198, 199sylan 458 . . . . . . . . . . 11
201 i1f0rn 19566 . . . . . . . . . . . . 13
2024, 201syl 16 . . . . . . . . . . . 12
203202ad2antrr 707 . . . . . . . . . . 11
204 ifcl 3767 . . . . . . . . . . 11
205200, 203, 204syl2anc 643 . . . . . . . . . 10
206205, 192fmptd 5885 . . . . . . . . 9
207 frn 5589 . . . . . . . . 9
208 ssdif 3474 . . . . . . . . 9
209206, 207, 2083syl 19 . . . . . . . 8
210166adantr 452 . . . . . . . . 9
211210ssdifd 3475 . . . . . . . 8
212 itg1val2 19568 . . . . . . . 8
213194, 195, 209, 211, 212syl13anc 1186 . . . . . . 7
214 fvex 5734 . . . . . . . . . . . . . . . . . . . . 21
215 c0ex 9077 . . . . . . . . . . . . . . . . . . . . 21
216214, 215ifex 3789 . . . . . . . . . . . . . . . . . . . 20
217192fvmpt2 5804 . . . . . . . . . . . . . . . . . . . 20
218216, 217mpan2 653 . . . . . . . . . . . . . . . . . . 19
219218adantl 453 . . . . . . . . . . . . . . . . . 18
220219eqeq1d 2443 . . . . . . . . . . . . . . . . 17
221 eldifsni 3920 . . . . . . . . . . . . . . . . . . . . 21
222221ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20
223 neeq1 2606 . . . . . . . . . . . . . . . . . . . 20
224222, 223syl5ibrcom 214 . . . . . . . . . . . . . . . . . . 19
225 iffalse 3738 . . . . . . . . . . . . . . . . . . . 20
226225necon1ai 2640 . . . . . . . . . . . . . . . . . . 19
227224, 226syl6 31 . . . . . . . . . . . . . . . . . 18
228227pm4.71rd 617 . . . . . . . . . . . . . . . . 17
229220, 228bitrd 245 . . . . . . . . . . . . . . . 16
230 iftrue 3737 . . . . . . . . . . . . . . . . . . 19
231230eqeq1d 2443 . . . . . . . . . . . . . . . . . 18
232231pm5.32i 619 . . . . . . . . . . . . . . . . 17
233 ancom 438 . . . . . . . . . . . . . . . . 17
234232, 233bitri 241 . . . . . . . . . . . . . . . 16
235229, 234syl6bb 253 . . . . . . . . . . . . . . 15
236235pm5.32da 623 . . . . . . . . . . . . . 14
237 anass 631 . . . . . . . . . . . . . 14
238236, 237syl6bbr 255 . . . . . . . . . . . . 13
239 i1ff 19560 . . . . . . . . . . . . . . . 16
240 ffn 5583 . . . . . . . . . . . . . . . 16
241194, 239, 2403syl 19 . . . . . . . . . . . . . . 15
242241adantr 452 . . . . . . . . . . . . . 14
243 fniniseg 5843 . . . . . . . . . . . . . 14
244242, 243syl 16 . . . . . . . . . . . . 13
245 elin 3522 . . . . . . . . . . . . . 14
246198adantr 452 . . . . . . . . . . . . . . . 16
247 fniniseg 5843 . . . . . . . . . . . . . . . 16
248246, 247syl 16 . . . . . . . . . . . . . . 15
249248anbi1d 686 . . . . . . . . . . . . . 14
250245, 249syl5bb 249 . . . . . . . . . . . . 13
251238, 244, 2503bitr4d 277 . . . . . . . . . . . 12
252251alrimiv 1641 . . . . . . . . . . 11
253 nfmpt1 4290 . . . . . . . . . . . . . . 15
254192, 253nfcxfr 2568 . . . . . . . . . . . . . 14
255254nfcnv 5043 . . . . . . . . . . . . 13
256 nfcv 2571 . . . . . . . . . . . . 13
257255, 256nfima 5203 . . . . . . . . . . . 12
258 nfcv 2571 . . . . . . . . . . . 12
259257, 258cleqf 2595 . . . . . . . . . . 11
260252, 259sylibr 204 . . . . . . . . . 10
261260fveq2d 5724 . . . . . . . . 9
262261oveq2d 6089 . . . . . . . 8
263262sumeq2dv 12489 . . . . . . 7
264213, 263eqtrd 2467 . . . . . 6
265264mpteq2dva 4287 . . . . 5
266265fveq1d 5722 . . . 4
267175sumeq2sdv 12490 . . . . . 6
268 eqid 2435 . . . . . 6
269 sumex 12473 . . . . . 6
270267, 268, 269fvmpt 5798 . . . . 5
271178sumeq2sdv 12490 . . . . 5
272270, 271eqtr4d 2470 . . . 4
273266, 272sylan9eq 2487 . . 3
2741, 3, 9, 182, 184, 190, 273climfsum 12591 . 2
275 itg1val 19567 . . 3
2764, 275syl 16 . 2
277274, 276breqtrrd 4230 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wal 1549   wceq 1652   wcel 1725   wne 2598  wral 2697  wrex 2698  cvv 2948   cdif 3309   cin 3311   wss 3312  c0 3620  cif 3731  csn 3806  cuni 4007  ciun 4085   class class class wbr 4204   cmpt 4258  ccnv 4869   cdm 4870   crn 4871  cima 4873   ccom 4874   wfn 5441  wf 5442  cfv 5446  (class class class)co 6073  cfn 7101  csup 7437  cc 8980  cr 8981  cc0 8982  c1 8983   caddc 8985   cmul 8987   cpnf 9109  cxr 9111   clt 9112   cle 9113  cn 9992  cz 10274  cicc 10911   cli 12270  csu 12471  covol 19351  cvol 19352  citg1 19499 This theorem is referenced by:  itg2monolem1  19634 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-inf2 7588  ax-cc 8307  ax-cnex 9038  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-mulcom 9046  ax-addass 9047  ax-mulass 9048  ax-distr 9049  ax-i2m1 9050  ax-1ne0 9051  ax-1rid 9052  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055  ax-pre-lttri 9056  ax-pre-lttrn 9057  ax-pre-ltadd 9058  ax-pre-mulgt0 9059  ax-pre-sup 9060  ax-addf 9061 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-disj 4175  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-of 6297  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-er 6897  df-map 7012  df-pm 7013  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-fi 7408  df-sup 7438  df-oi 7471  df-card 7818  df-cda 8040  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-sub 9285  df-neg 9286  df-div 9670  df-nn 9993  df-2 10050  df-3 10051  df-n0 10214  df-z 10275  df-uz 10481  df-q 10567  df-rp 10605  df-xneg 10702  df-xadd 10703  df-xmul 10704  df-ioo 10912  df-ico 10914  df-icc 10915  df-fz 11036  df-fzo 11128  df-fl 11194  df-seq 11316  df-exp 11375  df-hash 11611  df-cj 11896  df-re 11897  df-im 11898  df-sqr 12032  df-abs 12033  df-clim 12274  df-rlim 12275  df-sum 12472  df-rest 13642  df-topgen 13659  df-psmet 16686  df-xmet 16687  df-met 16688  df-bl 16689  df-mopn 16690  df-top 16955  df-bases 16957  df-topon 16958  df-cmp 17442  df-ovol 19353  df-vol 19354  df-mbf 19504  df-itg1 19505
 Copyright terms: Public domain W3C validator