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 ) ) |