Metamath Proof Explorer

Theorem radcnvlt2

Description: If X is within the open disk of radius R centered at zero, then the infinite series converges at X . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses pser.g 
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
radcnv.a 
|- ( ph -> A : NN0 --> CC )
radcnv.r 
|- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
radcnvlt.x 
|- ( ph -> X e. CC )
radcnvlt.a 
|- ( ph -> ( abs ` X ) < R )
Assertion radcnvlt2 
|- ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 pser.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 radcnv.a 
 |-  ( ph -> A : NN0 --> CC )
3 radcnv.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
4 radcnvlt.x 
 |-  ( ph -> X e. CC )
5 radcnvlt.a 
 |-  ( ph -> ( abs ` X ) < R )
6 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
7 0zd 
 |-  ( ph -> 0 e. ZZ )
8 1 2 4 psergf 
 |-  ( ph -> ( G ` X ) : NN0 --> CC )
9 fvco3 
 |-  ( ( ( G ` X ) : NN0 --> CC /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) = ( abs ` ( ( G ` X ) ` k ) ) )
10 8 9 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) = ( abs ` ( ( G ` X ) ` k ) ) )
11 8 ffvelrnda 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` X ) ` k ) e. CC )
12 id 
 |-  ( m = k -> m = k )
13 2fveq3 
 |-  ( m = k -> ( abs ` ( ( G ` X ) ` m ) ) = ( abs ` ( ( G ` X ) ` k ) ) )
14 12 13 oveq12d 
 |-  ( m = k -> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
15 14 cbvmptv 
 |-  ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) = ( k e. NN0 |-> ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
16 1 2 3 4 5 15 radcnvlt1 
 |-  ( ph -> ( seq 0 ( + , ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) )
17 16 simprd 
 |-  ( ph -> seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> )
18 6 7 10 11 17 abscvgcvg 
 |-  ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )