Metamath Proof Explorer

Theorem radcnvlem3

Description: Lemma for radcnvlt1 , radcnvle . If X is a point closer to zero than Y and the power series converges at Y , then it converges at X . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses pser.g 
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
radcnv.a 
|- ( ph -> A : NN0 --> CC )
psergf.x 
|- ( ph -> X e. CC )
radcnvlem2.y 
|- ( ph -> Y e. CC )
radcnvlem2.a 
|- ( ph -> ( abs ` X ) < ( abs ` Y ) )
radcnvlem2.c 
|- ( ph -> seq 0 ( + , ( G ` Y ) ) e. dom ~~> )
Assertion radcnvlem3 
|- ( 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 psergf.x 
 |-  ( ph -> X e. CC )
4 radcnvlem2.y 
 |-  ( ph -> Y e. CC )
5 radcnvlem2.a 
 |-  ( ph -> ( abs ` X ) < ( abs ` Y ) )
6 radcnvlem2.c 
 |-  ( ph -> seq 0 ( + , ( G ` Y ) ) e. dom ~~> )
7 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
8 0zd 
 |-  ( ph -> 0 e. ZZ )
9 1 2 3 psergf 
 |-  ( ph -> ( G ` X ) : NN0 --> CC )
10 fvco3 
 |-  ( ( ( G ` X ) : NN0 --> CC /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) = ( abs ` ( ( G ` X ) ` k ) ) )
11 9 10 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) = ( abs ` ( ( G ` X ) ` k ) ) )
12 9 ffvelcdmda 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` X ) ` k ) e. CC )
13 1 2 3 4 5 6 radcnvlem2 
 |-  ( ph -> seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> )
14 7 8 11 12 13 abscvgcvg 
 |-  ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )