Metamath Proof Explorer

Theorem psercn2

Description: Since by pserulm the series converges uniformly, it is also continuous by ulmcn . (Contributed by Mario Carneiro, 3-Mar-2015) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses pserf.g 
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
pserf.f 
|- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
pserf.a 
|- ( ph -> A : NN0 --> CC )
pserf.r 
|- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
pserulm.h 
|- H = ( i e. NN0 |-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
pserulm.m 
|- ( ph -> M e. RR )
pserulm.l 
|- ( ph -> M < R )
pserulm.y 
|- ( ph -> S C_ ( `' abs " ( 0 [,] M ) ) )
Assertion psercn2 
|- ( ph -> F e. ( S -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 pserf.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 pserf.f 
 |-  F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
3 pserf.a 
 |-  ( ph -> A : NN0 --> CC )
4 pserf.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
5 pserulm.h 
 |-  H = ( i e. NN0 |-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
6 pserulm.m 
 |-  ( ph -> M e. RR )
7 pserulm.l 
 |-  ( ph -> M < R )
8 pserulm.y 
 |-  ( ph -> S C_ ( `' abs " ( 0 [,] M ) ) )
9 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
10 0zd 
 |-  ( ph -> 0 e. ZZ )
11 cnvimass 
 |-  ( `' abs " ( 0 [,] M ) ) C_ dom abs
12 absf 
 |-  abs : CC --> RR
13 12 fdmi 
 |-  dom abs = CC
14 11 13 sseqtri 
 |-  ( `' abs " ( 0 [,] M ) ) C_ CC
15 8 14 sstrdi 
 |-  ( ph -> S C_ CC )
16 15 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> S C_ CC )
17 16 resmptd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( y e. CC |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) |` S ) = ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
18 simplr 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) /\ k e. ( 0 ... i ) ) -> y e. CC )
19 elfznn0 
 |-  ( k e. ( 0 ... i ) -> k e. NN0 )
20 19 adantl 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) /\ k e. ( 0 ... i ) ) -> k e. NN0 )
21 1 pserval2 
 |-  ( ( y e. CC /\ k e. NN0 ) -> ( ( G ` y ) ` k ) = ( ( A ` k ) x. ( y ^ k ) ) )
22 18 20 21 syl2anc 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) /\ k e. ( 0 ... i ) ) -> ( ( G ` y ) ` k ) = ( ( A ` k ) x. ( y ^ k ) ) )
23 simpr 
 |-  ( ( ph /\ i e. NN0 ) -> i e. NN0 )
24 23 9 eleqtrdi 
 |-  ( ( ph /\ i e. NN0 ) -> i e. ( ZZ>= ` 0 ) )
25 24 adantr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) -> i e. ( ZZ>= ` 0 ) )
26 3 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> A : NN0 --> CC )
27 26 ffvelcdmda 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
28 27 adantlr 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
29 expcl 
 |-  ( ( y e. CC /\ k e. NN0 ) -> ( y ^ k ) e. CC )
30 29 adantll 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) /\ k e. NN0 ) -> ( y ^ k ) e. CC )
31 28 30 mulcld 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( y ^ k ) ) e. CC )
32 19 31 sylan2 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) /\ k e. ( 0 ... i ) ) -> ( ( A ` k ) x. ( y ^ k ) ) e. CC )
33 22 25 32 fsumser 
 |-  ( ( ( ph /\ i e. NN0 ) /\ y e. CC ) -> sum_ k e. ( 0 ... i ) ( ( A ` k ) x. ( y ^ k ) ) = ( seq 0 ( + , ( G ` y ) ) ` i ) )
34 33 mpteq2dva 
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. CC |-> sum_ k e. ( 0 ... i ) ( ( A ` k ) x. ( y ^ k ) ) ) = ( y e. CC |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
35 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
36 35 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
37 36 a1i 
 |-  ( ( ph /\ i e. NN0 ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
38 fzfid 
 |-  ( ( ph /\ i e. NN0 ) -> ( 0 ... i ) e. Fin )
39 36 a1i 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
40 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
41 26 19 40 syl2an 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( A ` k ) e. CC )
42 39 39 41 cnmptc 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( y e. CC |-> ( A ` k ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
43 19 adantl 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> k e. NN0 )
44 35 expcn 
 |-  ( k e. NN0 -> ( y e. CC |-> ( y ^ k ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
45 43 44 syl 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( y e. CC |-> ( y ^ k ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
46 35 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
47 46 a1i 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
48 oveq12 
 |-  ( ( u = ( A ` k ) /\ v = ( y ^ k ) ) -> ( u x. v ) = ( ( A ` k ) x. ( y ^ k ) ) )
49 39 42 45 39 39 47 48 cnmpt12 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( y e. CC |-> ( ( A ` k ) x. ( y ^ k ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
50 35 37 38 49 fsumcn 
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. CC |-> sum_ k e. ( 0 ... i ) ( ( A ` k ) x. ( y ^ k ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
51 35 cncfcn1 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
52 50 51 eleqtrrdi 
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. CC |-> sum_ k e. ( 0 ... i ) ( ( A ` k ) x. ( y ^ k ) ) ) e. ( CC -cn-> CC ) )
53 34 52 eqeltrrd 
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. CC |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. ( CC -cn-> CC ) )
54 rescncf 
 |-  ( S C_ CC -> ( ( y e. CC |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. ( CC -cn-> CC ) -> ( ( y e. CC |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) |` S ) e. ( S -cn-> CC ) ) )
55 16 53 54 sylc 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( y e. CC |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) |` S ) e. ( S -cn-> CC ) )
56 17 55 eqeltrrd 
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. ( S -cn-> CC ) )
57 56 5 fmptd 
 |-  ( ph -> H : NN0 --> ( S -cn-> CC ) )
58 1 2 3 4 5 6 7 8 pserulm 
 |-  ( ph -> H ( ~~>u ` S ) F )
59 9 10 57 58 ulmcn 
 |-  ( ph -> F e. ( S -cn-> CC ) )