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

Theorem pserulm 23456
 Description: If is a region contained in a circle of radius , then the sequence of partial sums of the infinite series converges uniformly on . (Contributed by Mario Carneiro, 26-Feb-2015.)
Hypotheses
Ref Expression
pserf.g
pserf.f
pserf.a
pserf.r
pserulm.h
pserulm.m
pserulm.l
pserulm.y
Assertion
Ref Expression
pserulm
Distinct variable groups:   ,,,,,   ,,,   ,,,   ,,   ,,,,   ,,,   ,,,
Allowed substitution hints:   (,,)   ()   (,,,,,)   (,,)   (,,,,,)   (,)   (,,)   (,,)

Proof of Theorem pserulm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pserulm.y . . . . . 6
21adantr 472 . . . . 5
3 0xr 9705 . . . . . . . . 9
4 pserulm.m . . . . . . . . . 10
54rexrd 9708 . . . . . . . . 9
6 icc0 11709 . . . . . . . . 9
73, 5, 6sylancr 676 . . . . . . . 8
87biimpar 493 . . . . . . 7
98imaeq2d 5174 . . . . . 6
10 ima0 5189 . . . . . 6
119, 10syl6eq 2521 . . . . 5
122, 11sseqtrd 3454 . . . 4
13 ss0 3768 . . . 4
1412, 13syl 17 . . 3
15 nn0uz 11217 . . . 4
16 0zd 10973 . . . 4
17 0zd 10973 . . . . . . . . . 10
18 pserf.g . . . . . . . . . . . 12
19 pserf.a . . . . . . . . . . . . 13
2019adantr 472 . . . . . . . . . . . 12
21 cnvimass 5194 . . . . . . . . . . . . . . 15
22 absf 13477 . . . . . . . . . . . . . . . 16
2322fdmi 5746 . . . . . . . . . . . . . . 15
2421, 23sseqtri 3450 . . . . . . . . . . . . . 14
251, 24syl6ss 3430 . . . . . . . . . . . . 13
2625sselda 3418 . . . . . . . . . . . 12
2718, 20, 26psergf 23446 . . . . . . . . . . 11
2827ffvelrnda 6037 . . . . . . . . . 10
2915, 17, 28serf 12279 . . . . . . . . 9
3029ffvelrnda 6037 . . . . . . . 8
3130an32s 821 . . . . . . 7
32 eqid 2471 . . . . . . 7
3331, 32fmptd 6061 . . . . . 6
34 cnex 9638 . . . . . . 7
35 ssexg 4542 . . . . . . . . 9
3625, 34, 35sylancl 675 . . . . . . . 8
3736adantr 472 . . . . . . 7
38 elmapg 7503 . . . . . . 7
3934, 37, 38sylancr 676 . . . . . 6
4033, 39mpbird 240 . . . . 5
41 pserulm.h . . . . 5
4240, 41fmptd 6061 . . . 4
43 eqidd 2472 . . . . . 6
44 pserf.r . . . . . . 7
451sselda 3418 . . . . . . . . . . . . 13
46 ffn 5739 . . . . . . . . . . . . . 14
47 elpreima 6017 . . . . . . . . . . . . . 14
4822, 46, 47mp2b 10 . . . . . . . . . . . . 13
4945, 48sylib 201 . . . . . . . . . . . 12
5049simprd 470 . . . . . . . . . . 11
51 0re 9661 . . . . . . . . . . . 12
524adantr 472 . . . . . . . . . . . 12
53 elicc2 11724 . . . . . . . . . . . 12
5451, 52, 53sylancr 676 . . . . . . . . . . 11
5550, 54mpbid 215 . . . . . . . . . 10
5655simp1d 1042 . . . . . . . . 9
5756rexrd 9708 . . . . . . . 8
585adantr 472 . . . . . . . 8
59 iccssxr 11742 . . . . . . . . . 10
6018, 19, 44radcnvcl 23451 . . . . . . . . . 10
6159, 60sseldi 3416 . . . . . . . . 9
6261adantr 472 . . . . . . . 8
6355simp3d 1044 . . . . . . . 8
64 pserulm.l . . . . . . . . 9
6564adantr 472 . . . . . . . 8
6657, 58, 62, 63, 65xrlelttrd 11480 . . . . . . 7
6718, 20, 44, 26, 66radcnvlt2 23453 . . . . . 6
6815, 17, 43, 28, 67isumcl 13899 . . . . 5
69 pserf.f . . . . 5
7068, 69fmptd 6061 . . . 4
7115, 16, 42, 70ulm0 23425 . . 3
7214, 71syldan 478 . 2
73 simpr 468 . . . . . . . . . 10
7473, 15syl6eleq 2559 . . . . . . . . 9
75 elfznn0 11913 . . . . . . . . . . 11
7675adantl 473 . . . . . . . . . 10
7736ad2antrr 740 . . . . . . . . . . 11
78 mptexg 6151 . . . . . . . . . . 11
7977, 78syl 17 . . . . . . . . . 10
80 fveq2 5879 . . . . . . . . . . . . . 14
8180fveq1d 5881 . . . . . . . . . . . . 13
8281cbvmptv 4488 . . . . . . . . . . . 12
83 fveq2 5879 . . . . . . . . . . . . 13
8483mpteq2dv 4483 . . . . . . . . . . . 12
8582, 84syl5eq 2517 . . . . . . . . . . 11
86 eqid 2471 . . . . . . . . . . 11
8785, 86fvmptg 5961 . . . . . . . . . 10
8876, 79, 87syl2anc 673 . . . . . . . . 9
8937, 74, 88seqof 12308 . . . . . . . 8
9089eqcomd 2477 . . . . . . 7
9190mpteq2dva 4482 . . . . . 6
92 0z 10972 . . . . . . . . 9
93 seqfn 12263 . . . . . . . . 9
9492, 93ax-mp 5 . . . . . . . 8
9515fneq2i 5681 . . . . . . . 8
9694, 95mpbir 214 . . . . . . 7
97 dffn5 5924 . . . . . . 7
9896, 97mpbi 213 . . . . . 6
9991, 41, 983eqtr4g 2530 . . . . 5
10099adantr 472 . . . 4
101 0zd 10973 . . . . 5
10236adantr 472 . . . . 5
10319adantr 472 . . . . . . . . . . . 12
10425sselda 3418 . . . . . . . . . . . 12
10518, 103, 104psergf 23446 . . . . . . . . . . 11
106105ffvelrnda 6037 . . . . . . . . . 10
107106an32s 821 . . . . . . . . 9
108 eqid 2471 . . . . . . . . 9
109107, 108fmptd 6061 . . . . . . . 8
11036adantr 472 . . . . . . . . 9
111 elmapg 7503 . . . . . . . . 9
11234, 110, 111sylancr 676 . . . . . . . 8
113109, 112mpbird 240 . . . . . . 7
114113, 86fmptd 6061 . . . . . 6
115114adantr 472 . . . . 5
116 fex 6155 . . . . . . . 8
11722, 34, 116mp2an 686 . . . . . . 7
118 fvex 5889 . . . . . . 7
119117, 118coex 6764 . . . . . 6
120119a1i 11 . . . . 5
12119adantr 472 . . . . . . . 8
1224adantr 472 . . . . . . . . 9
123122recnd 9687 . . . . . . . 8
12418, 121, 123psergf 23446 . . . . . . 7
125 fco 5751 . . . . . . 7
12622, 124, 125sylancr 676 . . . . . 6
127126ffvelrnda 6037 . . . . 5
12825ad2antrr 740 . . . . . . . . . . 11
129 simprr 774 . . . . . . . . . . 11
130128, 129sseldd 3419 . . . . . . . . . 10
131 simprl 772 . . . . . . . . . 10
132130, 131expcld 12454 . . . . . . . . 9
133132abscld 13575 . . . . . . . 8
134123adantr 472 . . . . . . . . . 10
135134, 131expcld 12454 . . . . . . . . 9
136135abscld 13575 . . . . . . . 8
13719ad2antrr 740 . . . . . . . . . 10
138137, 131ffvelrnd 6038 . . . . . . . . 9
139138abscld 13575 . . . . . . . 8
140138absge0d 13583 . . . . . . . 8
141130abscld 13575 . . . . . . . . . 10
1424ad2antrr 740 . . . . . . . . . 10
143130absge0d 13583 . . . . . . . . . 10
14463ralrimiva 2809 . . . . . . . . . . . 12
145144ad2antrr 740 . . . . . . . . . . 11
146 fveq2 5879 . . . . . . . . . . . . 13
147146breq1d 4405 . . . . . . . . . . . 12
148147rspcv 3132 . . . . . . . . . . 11
149129, 145, 148sylc 61 . . . . . . . . . 10
150 leexp1a 12369 . . . . . . . . . 10
151141, 142, 131, 143, 149, 150syl32anc 1300 . . . . . . . . 9
152130, 131absexpd 13591 . . . . . . . . 9
153134, 131absexpd 13591 . . . . . . . . . 10
154 absid 13436 . . . . . . . . . . . . 13
1554, 154sylan 479 . . . . . . . . . . . 12
156155adantr 472 . . . . . . . . . . 11
157156oveq1d 6323 . . . . . . . . . 10
158153, 157eqtrd 2505 . . . . . . . . 9
159151, 152, 1583brtr4d 4426 . . . . . . . 8
160133, 136, 139, 140, 159lemul2ad 10569 . . . . . . 7
161138, 132absmuld 13593 . . . . . . 7
162138, 135absmuld 13593 . . . . . . 7
163160, 161, 1623brtr4d 4426 . . . . . 6
16436ad2antrr 740 . . . . . . . . . . 11
165164, 78syl 17 . . . . . . . . . 10
166131, 165, 87syl2anc 673 . . . . . . . . 9
167166fveq1d 5881 . . . . . . . 8
168 fveq2 5879 . . . . . . . . . . 11
169168fveq1d 5881 . . . . . . . . . 10
170 eqid 2471 . . . . . . . . . 10
171 fvex 5889 . . . . . . . . . 10
172169, 170, 171fvmpt 5963 . . . . . . . . 9
173172ad2antll 743 . . . . . . . 8
17418pserval2 23445 . . . . . . . . 9
175130, 131, 174syl2anc 673 . . . . . . . 8
176167, 173, 1753eqtrd 2509 . . . . . . 7
177176fveq2d 5883 . . . . . 6
178124adantr 472 . . . . . . . 8
179 fvco3 5957 . . . . . . . 8
180178, 131, 179syl2anc 673 . . . . . . 7
18118pserval2 23445 . . . . . . . . 9
182134, 131, 181syl2anc 673 . . . . . . . 8
183182fveq2d 5883 . . . . . . 7
184180, 183eqtrd 2505 . . . . . 6
185163, 177, 1843brtr4d 4426 . . . . 5
18664adantr 472 . . . . . . . 8
187155, 186eqbrtrd 4416 . . . . . . 7
188 id 22 . . . . . . . . 9
189 fveq2 5879 . . . . . . . . . 10
190189fveq2d 5883 . . . . . . . . 9
191188, 190oveq12d 6326 . . . . . . . 8
192191cbvmptv 4488 . . . . . . 7
19318, 121, 44, 123, 187, 192radcnvlt1 23452 . . . . . 6
194193simprd 470 . . . . 5
19515, 101, 102, 115, 120, 127, 185, 194mtest 23438 . . . 4
196100, 195eqeltrd 2549 . . 3
197 eldmg 5035 . . . . . 6
198197ibi 249 . . . . 5
199 simpr 468 . . . . . . . 8
200 ulmcl 23415 . . . . . . . . . . 11
201200adantl 473 . . . . . . . . . 10
202201feqmptd 5932 . . . . . . . . 9
203 0zd 10973 . . . . . . . . . . . 12
204 eqidd 2472 . . . . . . . . . . . 12
20527adantlr 729 . . . . . . . . . . . . 13
206205ffvelrnda 6037 . . . . . . . . . . . 12
20742ad2antrr 740 . . . . . . . . . . . . 13
208 simpr 468 . . . . . . . . . . . . 13
209 seqex 12253 . . . . . . . . . . . . . 14
210209a1i 11 . . . . . . . . . . . . 13
211 simpr 468 . . . . . . . . . . . . . . . 16
21236ad3antrrr 744 . . . . . . . . . . . . . . . . 17
213 mptexg 6151 . . . . . . . . . . . . . . . . 17
214212, 213syl 17 . . . . . . . . . . . . . . . 16
21541fvmpt2 5972 . . . . . . . . . . . . . . . 16
216211, 214, 215syl2anc 673 . . . . . . . . . . . . . . 15
217216fveq1d 5881 . . . . . . . . . . . . . 14
218 simplr 770 . . . . . . . . . . . . . . 15
219 fvex 5889 . . . . . . . . . . . . . . 15
22032fvmpt2 5972 . . . . . . . . . . . . . . 15
221218, 219, 220sylancl 675 . . . . . . . . . . . . . 14
222217, 221eqtrd 2505 . . . . . . . . . . . . 13
223 simplr 770 . . . . . . . . . . . . 13
22415, 203, 207, 208, 210, 222, 223ulmclm 23421 . . . . . . . . . . . 12
22515, 203, 204, 206, 224isumclim 13895 . . . . . . . . . . 11
226225mpteq2dva 4482 . . . . . . . . . 10
22769, 226syl5eq 2517 . . . . . . . . 9
228202, 227eqtr4d 2508 . . . . . . . 8
229199, 228breqtrd 4420 . . . . . . 7
230229ex 441 . . . . . 6
231230exlimdv 1787 . . . . 5
232198, 231syl5 32 . . . 4
233232imp 436 . . 3
234196, 233syldan 478 . 2
235 0red 9662 . 2
23672, 234, 4, 235ltlecasei 9760 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904  wral 2756  crab 2760  cvv 3031   wss 3390  c0 3722   class class class wbr 4395   cmpt 4454  ccnv 4838   cdm 4839  cima 4842   ccom 4843   wfn 5584  wf 5585  cfv 5589  (class class class)co 6308   cof 6548   cmap 7490  csup 7972  cc 9555  cr 9556  cc0 9557   caddc 9560   cmul 9562   cpnf 9690  cxr 9692   clt 9693   cle 9694  cn0 10893  cz 10961  cuz 11182  cicc 11663  cfz 11810   cseq 12251  cexp 12310  cabs 13374   cli 13625  csu 13829  culm 23410 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-rp 11326  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-limsup 13603  df-clim 13629  df-rlim 13630  df-sum 13830  df-ulm 23411 This theorem is referenced by:  psercn2  23457  pserdvlem2  23462
 Copyright terms: Public domain W3C validator