Metamath Proof Explorer

Theorem radcnvlt1

Description: If X is within the open disk of radius R centered at zero, then the infinite series converges absolutely at X , and also converges when the series is multiplied by n . (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 )
radcnvlt1.h 
|- H = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
Assertion radcnvlt1 
|- ( ph -> ( seq 0 ( + , H ) e. dom ~~> /\ 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 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 radcnvlt1.h 
 |-  H = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
7 ressxr 
 |-  RR C_ RR*
8 4 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
9 7 8 sseldi 
 |-  ( ph -> ( abs ` X ) e. RR* )
10 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
11 1 2 3 radcnvcl 
 |-  ( ph -> R e. ( 0 [,] +oo ) )
12 10 11 sseldi 
 |-  ( ph -> R e. RR* )
13 xrltnle 
 |-  ( ( ( abs ` X ) e. RR* /\ R e. RR* ) -> ( ( abs ` X ) < R <-> -. R <_ ( abs ` X ) ) )
14 9 12 13 syl2anc 
 |-  ( ph -> ( ( abs ` X ) < R <-> -. R <_ ( abs ` X ) ) )
15 5 14 mpbid 
 |-  ( ph -> -. R <_ ( abs ` X ) )
16 3 breq1i 
 |-  ( R <_ ( abs ` X ) <-> sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) <_ ( abs ` X ) )
17 ssrab2 
 |-  { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR
18 17 7 sstri 
 |-  { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR*
19 supxrleub 
 |-  ( ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR* /\ ( abs ` X ) e. RR* ) -> ( sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) <_ ( abs ` X ) <-> A. s e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } s <_ ( abs ` X ) ) )
20 18 9 19 sylancr 
 |-  ( ph -> ( sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) <_ ( abs ` X ) <-> A. s e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } s <_ ( abs ` X ) ) )
21 16 20 syl5bb 
 |-  ( ph -> ( R <_ ( abs ` X ) <-> A. s e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } s <_ ( abs ` X ) ) )
22 fveq2 
 |-  ( r = s -> ( G ` r ) = ( G ` s ) )
23 22 seqeq3d 
 |-  ( r = s -> seq 0 ( + , ( G ` r ) ) = seq 0 ( + , ( G ` s ) ) )
24 23 eleq1d 
 |-  ( r = s -> ( seq 0 ( + , ( G ` r ) ) e. dom ~~> <-> seq 0 ( + , ( G ` s ) ) e. dom ~~> ) )
25 24 ralrab 
 |-  ( A. s e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } s <_ ( abs ` X ) <-> A. s e. RR ( seq 0 ( + , ( G ` s ) ) e. dom ~~> -> s <_ ( abs ` X ) ) )
26 21 25 bitrdi 
 |-  ( ph -> ( R <_ ( abs ` X ) <-> A. s e. RR ( seq 0 ( + , ( G ` s ) ) e. dom ~~> -> s <_ ( abs ` X ) ) ) )
27 15 26 mtbid 
 |-  ( ph -> -. A. s e. RR ( seq 0 ( + , ( G ` s ) ) e. dom ~~> -> s <_ ( abs ` X ) ) )
28 rexanali 
 |-  ( E. s e. RR ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ -. s <_ ( abs ` X ) ) <-> -. A. s e. RR ( seq 0 ( + , ( G ` s ) ) e. dom ~~> -> s <_ ( abs ` X ) ) )
29 27 28 sylibr 
 |-  ( ph -> E. s e. RR ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ -. s <_ ( abs ` X ) ) )
30 ltnle 
 |-  ( ( ( abs ` X ) e. RR /\ s e. RR ) -> ( ( abs ` X ) < s <-> -. s <_ ( abs ` X ) ) )
31 8 30 sylan 
 |-  ( ( ph /\ s e. RR ) -> ( ( abs ` X ) < s <-> -. s <_ ( abs ` X ) ) )
32 31 adantr 
 |-  ( ( ( ph /\ s e. RR ) /\ seq 0 ( + , ( G ` s ) ) e. dom ~~> ) -> ( ( abs ` X ) < s <-> -. s <_ ( abs ` X ) ) )
33 2 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> A : NN0 --> CC )
34 4 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> X e. CC )
35 simplr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> s e. RR )
36 35 recnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> s e. CC )
37 simprr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> ( abs ` X ) < s )
38 0red 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> 0 e. RR )
39 34 abscld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> ( abs ` X ) e. RR )
40 34 absge0d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> 0 <_ ( abs ` X ) )
41 38 39 35 40 37 lelttrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> 0 < s )
42 38 35 41 ltled 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> 0 <_ s )
43 35 42 absidd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> ( abs ` s ) = s )
44 37 43 breqtrrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> ( abs ` X ) < ( abs ` s ) )
45 simprl 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> seq 0 ( + , ( G ` s ) ) e. dom ~~> )
46 1 33 34 36 44 45 6 radcnvlem1 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> seq 0 ( + , H ) e. dom ~~> )
47 1 33 34 36 44 45 radcnvlem2 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> )
48 46 47 jca 
 |-  ( ( ( ph /\ s e. RR ) /\ ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ ( abs ` X ) < s ) ) -> ( seq 0 ( + , H ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) )
49 48 expr 
 |-  ( ( ( ph /\ s e. RR ) /\ seq 0 ( + , ( G ` s ) ) e. dom ~~> ) -> ( ( abs ` X ) < s -> ( seq 0 ( + , H ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) ) )
50 32 49 sylbird 
 |-  ( ( ( ph /\ s e. RR ) /\ seq 0 ( + , ( G ` s ) ) e. dom ~~> ) -> ( -. s <_ ( abs ` X ) -> ( seq 0 ( + , H ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) ) )
51 50 expimpd 
 |-  ( ( ph /\ s e. RR ) -> ( ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ -. s <_ ( abs ` X ) ) -> ( seq 0 ( + , H ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) ) )
52 51 rexlimdva 
 |-  ( ph -> ( E. s e. RR ( seq 0 ( + , ( G ` s ) ) e. dom ~~> /\ -. s <_ ( abs ` X ) ) -> ( seq 0 ( + , H ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) ) )
53 29 52 mpd 
 |-  ( ph -> ( seq 0 ( + , H ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) )