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 ffvelrnda
 |-  ( ( 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 mulid2d
 |-  ( ( 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 mulid2d
 |-  ( ( 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 ~~> )