Metamath Proof Explorer

Theorem abelth

Description: Abel's theorem. If the power series sum_ n e. NN0 A ( n ) ( x ^ n ) is convergent at 1 , then it is equal to the limit from "below", along a Stolz angle S (note that the M = 1 case of a Stolz angle is the real line [ 0 , 1 ] ). (Continuity on S \ { 1 } follows more generally from psercn .) (Contributed by Mario Carneiro, 2-Apr-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses abelth.1 
|- ( ph -> A : NN0 --> CC )
abelth.2 
|- ( ph -> seq 0 ( + , A ) e. dom ~~> )
abelth.3 
|- ( ph -> M e. RR )
abelth.4 
|- ( ph -> 0 <_ M )
abelth.5 
|- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }
abelth.6 
|- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
Assertion abelth 
|- ( ph -> F e. ( S -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 abelth.1 
 |-  ( ph -> A : NN0 --> CC )
2 abelth.2 
 |-  ( ph -> seq 0 ( + , A ) e. dom ~~> )
3 abelth.3 
 |-  ( ph -> M e. RR )
4 abelth.4 
 |-  ( ph -> 0 <_ M )
5 abelth.5 
 |-  S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }
6 abelth.6 
 |-  F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
7 1 2 3 4 5 6 abelthlem4 
 |-  ( ph -> F : S --> CC )
8 1 2 3 4 5 6 abelthlem9 
 |-  ( ( ph /\ r e. RR+ ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < r ) )
9 1 2 3 4 5 abelthlem2 
 |-  ( ph -> ( 1 e. S /\ ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
10 9 simpld 
 |-  ( ph -> 1 e. S )
11 10 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> 1 e. S )
12 simpr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> y e. S )
13 11 12 ovresd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) = ( 1 ( abs o. - ) y ) )
14 ax-1cn 
 |-  1 e. CC
15 5 ssrab3 
 |-  S C_ CC
16 15 12 sselid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> y e. CC )
17 eqid 
 |-  ( abs o. - ) = ( abs o. - )
18 17 cnmetdval 
 |-  ( ( 1 e. CC /\ y e. CC ) -> ( 1 ( abs o. - ) y ) = ( abs ` ( 1 - y ) ) )
19 14 16 18 sylancr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( 1 ( abs o. - ) y ) = ( abs ` ( 1 - y ) ) )
20 13 19 eqtrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) = ( abs ` ( 1 - y ) ) )
21 20 breq1d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) < w <-> ( abs ` ( 1 - y ) ) < w ) )
22 7 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> F : S --> CC )
23 22 11 ffvelrnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( F ` 1 ) e. CC )
24 7 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> F : S --> CC )
25 24 ffvelrnda 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( F ` y ) e. CC )
26 17 cnmetdval 
 |-  ( ( ( F ` 1 ) e. CC /\ ( F ` y ) e. CC ) -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) = ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) )
27 23 25 26 syl2anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) = ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) )
28 27 breq1d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) < r <-> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < r ) )
29 21 28 imbi12d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. S ) -> ( ( ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) < w -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) < r ) <-> ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < r ) ) )
30 29 ralbidva 
 |-  ( ( ph /\ r e. RR+ ) -> ( A. y e. S ( ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) < w -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) < r ) <-> A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < r ) ) )
31 30 rexbidv 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. w e. RR+ A. y e. S ( ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) < w -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) < r ) <-> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < r ) ) )
32 8 31 mpbird 
 |-  ( ( ph /\ r e. RR+ ) -> E. w e. RR+ A. y e. S ( ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) < w -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) < r ) )
33 32 ralrimiva 
 |-  ( ph -> A. r e. RR+ E. w e. RR+ A. y e. S ( ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) < w -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) < r ) )
34 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
35 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ S C_ CC ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
36 34 15 35 mp2an 
 |-  ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S )
37 eqid 
 |-  ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( S X. S ) )
38 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
39 38 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
40 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) )
41 37 39 40 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
42 34 15 41 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) )
43 42 39 metcnp 
 |-  ( ( ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) /\ ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. S ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 1 ) <-> ( F : S --> CC /\ A. r e. RR+ E. w e. RR+ A. y e. S ( ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) < w -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) < r ) ) ) )
44 36 34 10 43 mp3an12i 
 |-  ( ph -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 1 ) <-> ( F : S --> CC /\ A. r e. RR+ E. w e. RR+ A. y e. S ( ( 1 ( ( abs o. - ) |` ( S X. S ) ) y ) < w -> ( ( F ` 1 ) ( abs o. - ) ( F ` y ) ) < r ) ) ) )
45 7 33 44 mpbir2and 
 |-  ( ph -> F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 1 ) )
46 45 ad2antrr 
 |-  ( ( ( ph /\ y e. S ) /\ y = 1 ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 1 ) )
47 simpr 
 |-  ( ( ( ph /\ y e. S ) /\ y = 1 ) -> y = 1 )
48 47 fveq2d 
 |-  ( ( ( ph /\ y e. S ) /\ y = 1 ) -> ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) = ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 1 ) )
49 46 48 eleqtrrd 
 |-  ( ( ( ph /\ y e. S ) /\ y = 1 ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) )
50 eldifsn 
 |-  ( y e. ( S \ { 1 } ) <-> ( y e. S /\ y =/= 1 ) )
51 9 simprd 
 |-  ( ph -> ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) )
52 abscl 
 |-  ( w e. CC -> ( abs ` w ) e. RR )
53 52 adantl 
 |-  ( ( ph /\ w e. CC ) -> ( abs ` w ) e. RR )
54 53 a1d 
 |-  ( ( ph /\ w e. CC ) -> ( ( abs ` w ) < 1 -> ( abs ` w ) e. RR ) )
55 absge0 
 |-  ( w e. CC -> 0 <_ ( abs ` w ) )
56 55 adantl 
 |-  ( ( ph /\ w e. CC ) -> 0 <_ ( abs ` w ) )
57 56 a1d 
 |-  ( ( ph /\ w e. CC ) -> ( ( abs ` w ) < 1 -> 0 <_ ( abs ` w ) ) )
58 1 2 abelthlem1 
 |-  ( ph -> 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
59 58 adantr 
 |-  ( ( ph /\ w e. CC ) -> 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
60 53 rexrd 
 |-  ( ( ph /\ w e. CC ) -> ( abs ` w ) e. RR* )
61 1re 
 |-  1 e. RR
62 rexr 
 |-  ( 1 e. RR -> 1 e. RR* )
63 61 62 mp1i 
 |-  ( ( ph /\ w e. CC ) -> 1 e. RR* )
64 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
65 eqid 
 |-  ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) = ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) )
66 eqid 
 |-  sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) = sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < )
67 65 1 66 radcnvcl 
 |-  ( ph -> sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. ( 0 [,] +oo ) )
68 64 67 sselid 
 |-  ( ph -> sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
69 68 adantr 
 |-  ( ( ph /\ w e. CC ) -> sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
70 xrltletr 
 |-  ( ( ( abs ` w ) e. RR* /\ 1 e. RR* /\ sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. RR* ) -> ( ( ( abs ` w ) < 1 /\ 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) -> ( abs ` w ) < sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) )
71 60 63 69 70 syl3anc 
 |-  ( ( ph /\ w e. CC ) -> ( ( ( abs ` w ) < 1 /\ 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) -> ( abs ` w ) < sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) )
72 59 71 mpan2d 
 |-  ( ( ph /\ w e. CC ) -> ( ( abs ` w ) < 1 -> ( abs ` w ) < sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) )
73 54 57 72 3jcad 
 |-  ( ( ph /\ w e. CC ) -> ( ( abs ` w ) < 1 -> ( ( abs ` w ) e. RR /\ 0 <_ ( abs ` w ) /\ ( abs ` w ) < sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) )
74 0cn 
 |-  0 e. CC
75 17 cnmetdval 
 |-  ( ( 0 e. CC /\ w e. CC ) -> ( 0 ( abs o. - ) w ) = ( abs ` ( 0 - w ) ) )
76 74 75 mpan 
 |-  ( w e. CC -> ( 0 ( abs o. - ) w ) = ( abs ` ( 0 - w ) ) )
77 abssub 
 |-  ( ( 0 e. CC /\ w e. CC ) -> ( abs ` ( 0 - w ) ) = ( abs ` ( w - 0 ) ) )
78 74 77 mpan 
 |-  ( w e. CC -> ( abs ` ( 0 - w ) ) = ( abs ` ( w - 0 ) ) )
79 subid1 
 |-  ( w e. CC -> ( w - 0 ) = w )
80 79 fveq2d 
 |-  ( w e. CC -> ( abs ` ( w - 0 ) ) = ( abs ` w ) )
81 76 78 80 3eqtrd 
 |-  ( w e. CC -> ( 0 ( abs o. - ) w ) = ( abs ` w ) )
82 81 breq1d 
 |-  ( w e. CC -> ( ( 0 ( abs o. - ) w ) < 1 <-> ( abs ` w ) < 1 ) )
83 82 adantl 
 |-  ( ( ph /\ w e. CC ) -> ( ( 0 ( abs o. - ) w ) < 1 <-> ( abs ` w ) < 1 ) )
84 0re 
 |-  0 e. RR
85 elico2 
 |-  ( ( 0 e. RR /\ sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. RR* ) -> ( ( abs ` w ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) <-> ( ( abs ` w ) e. RR /\ 0 <_ ( abs ` w ) /\ ( abs ` w ) < sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) )
86 84 69 85 sylancr 
 |-  ( ( ph /\ w e. CC ) -> ( ( abs ` w ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) <-> ( ( abs ` w ) e. RR /\ 0 <_ ( abs ` w ) /\ ( abs ` w ) < sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) )
87 73 83 86 3imtr4d 
 |-  ( ( ph /\ w e. CC ) -> ( ( 0 ( abs o. - ) w ) < 1 -> ( abs ` w ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) )
88 87 imdistanda 
 |-  ( ph -> ( ( w e. CC /\ ( 0 ( abs o. - ) w ) < 1 ) -> ( w e. CC /\ ( abs ` w ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) ) )
89 1xr 
 |-  1 e. RR*
90 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( w e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( w e. CC /\ ( 0 ( abs o. - ) w ) < 1 ) ) )
91 34 74 89 90 mp3an 
 |-  ( w e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( w e. CC /\ ( 0 ( abs o. - ) w ) < 1 ) )
92 absf 
 |-  abs : CC --> RR
93 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
94 elpreima 
 |-  ( abs Fn CC -> ( w e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) <-> ( w e. CC /\ ( abs ` w ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) ) )
95 92 93 94 mp2b 
 |-  ( w e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) <-> ( w e. CC /\ ( abs ` w ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) )
96 88 91 95 3imtr4g 
 |-  ( ph -> ( w e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> w e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) ) )
97 96 ssrdv 
 |-  ( ph -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) )
98 51 97 sstrd 
 |-  ( ph -> ( S \ { 1 } ) C_ ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) )
99 98 resmptd 
 |-  ( ph -> ( ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( S \ { 1 } ) ) = ( x e. ( S \ { 1 } ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) )
100 6 reseq1i 
 |-  ( F |` ( S \ { 1 } ) ) = ( ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( S \ { 1 } ) )
101 difss 
 |-  ( S \ { 1 } ) C_ S
102 resmpt 
 |-  ( ( S \ { 1 } ) C_ S -> ( ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( S \ { 1 } ) ) = ( x e. ( S \ { 1 } ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) )
103 101 102 ax-mp 
 |-  ( ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( S \ { 1 } ) ) = ( x e. ( S \ { 1 } ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
104 100 103 eqtri 
 |-  ( F |` ( S \ { 1 } ) ) = ( x e. ( S \ { 1 } ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
105 99 104 eqtr4di 
 |-  ( ph -> ( ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( S \ { 1 } ) ) = ( F |` ( S \ { 1 } ) ) )
106 cnvimass 
 |-  ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) C_ dom abs
107 92 fdmi 
 |-  dom abs = CC
108 106 107 sseqtri 
 |-  ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) C_ CC
109 108 sseli 
 |-  ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) -> x e. CC )
110 fveq2 
 |-  ( n = j -> ( A ` n ) = ( A ` j ) )
111 oveq2 
 |-  ( n = j -> ( x ^ n ) = ( x ^ j ) )
112 110 111 oveq12d 
 |-  ( n = j -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` j ) x. ( x ^ j ) ) )
113 112 cbvsumv 
 |-  sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ j e. NN0 ( ( A ` j ) x. ( x ^ j ) )
114 65 pserval2 
 |-  ( ( x e. CC /\ j e. NN0 ) -> ( ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` x ) ` j ) = ( ( A ` j ) x. ( x ^ j ) ) )
115 114 sumeq2dv 
 |-  ( x e. CC -> sum_ j e. NN0 ( ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` x ) ` j ) = sum_ j e. NN0 ( ( A ` j ) x. ( x ^ j ) ) )
116 113 115 eqtr4id 
 |-  ( x e. CC -> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ j e. NN0 ( ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` x ) ` j ) )
117 109 116 syl 
 |-  ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) -> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ j e. NN0 ( ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` x ) ` j ) )
118 117 mpteq2ia 
 |-  ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) = ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ j e. NN0 ( ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` x ) ` j ) )
119 eqid 
 |-  ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) = ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) )
120 eqid 
 |-  if ( sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` v ) + sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` v ) + 1 ) ) = if ( sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` v ) + sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` v ) + 1 ) )
121 65 118 1 66 119 120 psercn 
 |-  ( ph -> ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) e. ( ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) -cn-> CC ) )
122 rescncf 
 |-  ( ( S \ { 1 } ) C_ ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) -> ( ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) e. ( ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) -cn-> CC ) -> ( ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( S \ { 1 } ) ) e. ( ( S \ { 1 } ) -cn-> CC ) ) )
123 98 121 122 sylc 
 |-  ( ph -> ( ( x e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( t e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( t ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( S \ { 1 } ) ) e. ( ( S \ { 1 } ) -cn-> CC ) )
124 105 123 eqeltrrd 
 |-  ( ph -> ( F |` ( S \ { 1 } ) ) e. ( ( S \ { 1 } ) -cn-> CC ) )
125 124 adantr 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> ( F |` ( S \ { 1 } ) ) e. ( ( S \ { 1 } ) -cn-> CC ) )
126 101 15 sstri 
 |-  ( S \ { 1 } ) C_ CC
127 ssid 
 |-  CC C_ CC
128 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) = ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) )
129 38 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
130 129 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
131 38 128 130 cncfcn 
 |-  ( ( ( S \ { 1 } ) C_ CC /\ CC C_ CC ) -> ( ( S \ { 1 } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) Cn ( TopOpen ` CCfld ) ) )
132 126 127 131 mp2an 
 |-  ( ( S \ { 1 } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) Cn ( TopOpen ` CCfld ) )
133 125 132 eleqtrdi 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> ( F |` ( S \ { 1 } ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) Cn ( TopOpen ` CCfld ) ) )
134 simpr 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> y e. ( S \ { 1 } ) )
135 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( S \ { 1 } ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) e. ( TopOn ` ( S \ { 1 } ) ) )
136 129 126 135 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) e. ( TopOn ` ( S \ { 1 } ) )
137 136 toponunii 
 |-  ( S \ { 1 } ) = U. ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) )
138 137 cncnpi 
 |-  ( ( ( F |` ( S \ { 1 } ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) Cn ( TopOpen ` CCfld ) ) /\ y e. ( S \ { 1 } ) ) -> ( F |` ( S \ { 1 } ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
139 133 134 138 syl2anc 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> ( F |` ( S \ { 1 } ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
140 38 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
141 cnex 
 |-  CC e. _V
142 141 15 ssexi 
 |-  S e. _V
143 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( S \ { 1 } ) C_ S /\ S e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( S \ { 1 } ) ) = ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) )
144 140 101 142 143 mp3an 
 |-  ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( S \ { 1 } ) ) = ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) )
145 144 oveq1i 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) )
146 145 fveq1i 
 |-  ( ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) ) ` y ) = ( ( ( ( TopOpen ` CCfld ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) ) ` y )
147 139 146 eleqtrrdi 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> ( F |` ( S \ { 1 } ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
148 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S e. _V ) -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
149 140 142 148 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t S ) e. Top
150 149 a1i 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
151 101 a1i 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> ( S \ { 1 } ) C_ S )
152 10 snssd 
 |-  ( ph -> { 1 } C_ S )
153 38 cnfldhaus 
 |-  ( TopOpen ` CCfld ) e. Haus
154 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
155 154 sncld 
 |-  ( ( ( TopOpen ` CCfld ) e. Haus /\ 1 e. CC ) -> { 1 } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
156 153 14 155 mp2an 
 |-  { 1 } e. ( Clsd ` ( TopOpen ` CCfld ) )
157 154 restcldi 
 |-  ( ( S C_ CC /\ { 1 } e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ { 1 } C_ S ) -> { 1 } e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t S ) ) )
158 15 156 157 mp3an12 
 |-  ( { 1 } C_ S -> { 1 } e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t S ) ) )
159 154 restuni 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S C_ CC ) -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
160 140 15 159 mp2an 
 |-  S = U. ( ( TopOpen ` CCfld ) |`t S )
161 160 cldopn 
 |-  ( { 1 } e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t S ) ) -> ( S \ { 1 } ) e. ( ( TopOpen ` CCfld ) |`t S ) )
162 152 158 161 3syl 
 |-  ( ph -> ( S \ { 1 } ) e. ( ( TopOpen ` CCfld ) |`t S ) )
163 160 isopn3 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ ( S \ { 1 } ) C_ S ) -> ( ( S \ { 1 } ) e. ( ( TopOpen ` CCfld ) |`t S ) <-> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( S \ { 1 } ) ) = ( S \ { 1 } ) ) )
164 149 101 163 mp2an 
 |-  ( ( S \ { 1 } ) e. ( ( TopOpen ` CCfld ) |`t S ) <-> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( S \ { 1 } ) ) = ( S \ { 1 } ) )
165 162 164 sylib 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( S \ { 1 } ) ) = ( S \ { 1 } ) )
166 165 eleq2d 
 |-  ( ph -> ( y e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( S \ { 1 } ) ) <-> y e. ( S \ { 1 } ) ) )
167 166 biimpar 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> y e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( S \ { 1 } ) ) )
168 7 adantr 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> F : S --> CC )
169 160 154 cnprest 
 |-  ( ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ ( S \ { 1 } ) C_ S ) /\ ( y e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( S \ { 1 } ) ) /\ F : S --> CC ) ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( F |` ( S \ { 1 } ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
170 150 151 167 168 169 syl22anc 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( F |` ( S \ { 1 } ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( S \ { 1 } ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
171 147 170 mpbird 
 |-  ( ( ph /\ y e. ( S \ { 1 } ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) )
172 50 171 sylan2br 
 |-  ( ( ph /\ ( y e. S /\ y =/= 1 ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) )
173 172 anassrs 
 |-  ( ( ( ph /\ y e. S ) /\ y =/= 1 ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) )
174 49 173 pm2.61dane 
 |-  ( ( ph /\ y e. S ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) )
175 174 ralrimiva 
 |-  ( ph -> A. y e. S F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) )
176 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
177 129 15 176 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S )
178 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( F e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) <-> ( F : S --> CC /\ A. y e. S F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
179 177 129 178 mp2an 
 |-  ( F e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) <-> ( F : S --> CC /\ A. y e. S F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
180 7 175 179 sylanbrc 
 |-  ( ph -> F e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) )
181 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
182 38 181 130 cncfcn 
 |-  ( ( S C_ CC /\ CC C_ CC ) -> ( S -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) )
183 15 127 182 mp2an 
 |-  ( S -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) )
184 180 183 eleqtrrdi 
 |-  ( ph -> F e. ( S -cn-> CC ) )