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)

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 ffvelrnda
 |-  ( ( ( 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 ffvelrn
 |-  ( ( 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 mulcn
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
47 46 a1i
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
48 39 42 45 47 cnmpt12f
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( y e. CC |-> ( ( A ` k ) x. ( y ^ k ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
49 35 37 38 48 fsumcn
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. CC |-> sum_ k e. ( 0 ... i ) ( ( A ` k ) x. ( y ^ k ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
50 35 cncfcn1
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
51 49 50 eleqtrrdi
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. CC |-> sum_ k e. ( 0 ... i ) ( ( A ` k ) x. ( y ^ k ) ) ) e. ( CC -cn-> CC ) )
52 34 51 eqeltrrd
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. CC |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. ( CC -cn-> CC ) )
53 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 ) ) )
54 16 52 53 sylc
 |-  ( ( ph /\ i e. NN0 ) -> ( ( y e. CC |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) |` S ) e. ( S -cn-> CC ) )
55 17 54 eqeltrrd
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. ( S -cn-> CC ) )
56 55 5 fmptd
 |-  ( ph -> H : NN0 --> ( S -cn-> CC ) )
57 1 2 3 4 5 6 7 8 pserulm
 |-  ( ph -> H ( ~~>u ` S ) F )
58 9 10 56 57 ulmcn
 |-  ( ph -> F e. ( S -cn-> CC ) )