Metamath Proof Explorer

Theorem radcnvlem2

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 absolutely 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 )
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 radcnvlem2 
|- ( ph -> seq 0 ( + , ( abs o. ( 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 1nn0 
 |-  1 e. NN0
9 8 a1i 
 |-  ( ph -> 1 e. NN0 )
10 id 
 |-  ( m = k -> m = k )
11 2fveq3 
 |-  ( m = k -> ( abs ` ( ( G ` X ) ` m ) ) = ( abs ` ( ( G ` X ) ` k ) ) )
12 10 11 oveq12d 
 |-  ( m = k -> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
13 eqid 
 |-  ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
14 ovex 
 |-  ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) e. _V
15 12 13 14 fvmpt 
 |-  ( k e. NN0 -> ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
16 15 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
17 nn0re 
 |-  ( k e. NN0 -> k e. RR )
18 17 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> k e. RR )
19 1 2 3 psergf 
 |-  ( ph -> ( G ` X ) : NN0 --> CC )
20 19 ffvelcdmda 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` X ) ` k ) e. CC )
21 20 abscld 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( G ` X ) ` k ) ) e. RR )
22 18 21 remulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) e. RR )
23 16 22 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) e. RR )
24 fvco3 
 |-  ( ( ( G ` X ) : NN0 --> CC /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) = ( abs ` ( ( G ` X ) ` k ) ) )
25 19 24 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) = ( abs ` ( ( G ` X ) ` k ) ) )
26 21 recnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( G ` X ) ` k ) ) e. CC )
27 25 26 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) e. CC )
28 12 cbvmptv 
 |-  ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) = ( k e. NN0 |-> ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
29 1 2 3 4 5 6 28 radcnvlem1 
 |-  ( ph -> seq 0 ( + , ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ) e. dom ~~> )
30 1red 
 |-  ( ph -> 1 e. RR )
31 1red 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> 1 e. RR )
32 elnnuz 
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
33 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
34 32 33 sylbir 
 |-  ( k e. ( ZZ>= ` 1 ) -> k e. NN0 )
35 34 18 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> k e. RR )
36 34 21 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( G ` X ) ` k ) ) e. RR )
37 20 absge0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ ( abs ` ( ( G ` X ) ` k ) ) )
38 34 37 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> 0 <_ ( abs ` ( ( G ` X ) ` k ) ) )
39 eluzle 
 |-  ( k e. ( ZZ>= ` 1 ) -> 1 <_ k )
40 39 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> 1 <_ k )
41 31 35 36 38 40 lemul1ad 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( 1 x. ( abs ` ( ( G ` X ) ` k ) ) ) <_ ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
42 absidm 
 |-  ( ( ( G ` X ) ` k ) e. CC -> ( abs ` ( abs ` ( ( G ` X ) ` k ) ) ) = ( abs ` ( ( G ` X ) ` k ) ) )
43 20 42 syl 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( abs ` ( ( G ` X ) ` k ) ) ) = ( abs ` ( ( G ` X ) ` k ) ) )
44 25 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( abs o. ( G ` X ) ) ` k ) ) = ( abs ` ( abs ` ( ( G ` X ) ` k ) ) ) )
45 26 mullidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 x. ( abs ` ( ( G ` X ) ` k ) ) ) = ( abs ` ( ( G ` X ) ` k ) ) )
46 43 44 45 3eqtr4d 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( abs o. ( G ` X ) ) ` k ) ) = ( 1 x. ( abs ` ( ( G ` X ) ` k ) ) ) )
47 34 46 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( abs o. ( G ` X ) ) ` k ) ) = ( 1 x. ( abs ` ( ( G ` X ) ` k ) ) ) )
48 16 oveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 x. ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) ) = ( 1 x. ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) )
49 22 recnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) e. CC )
50 49 mullidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 x. ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
51 48 50 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 x. ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
52 34 51 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( 1 x. ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
53 41 47 52 3brtr4d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( abs o. ( G ` X ) ) ` k ) ) <_ ( 1 x. ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) ) )
54 7 9 23 27 29 30 53 cvgcmpce 
 |-  ( ph -> seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> )