Metamath Proof Explorer

Theorem radcnvle

Description: If X is a convergent point of the infinite series, then X is within the closed disk of radius R centered at zero. Or, by contraposition, the series diverges at any point strictly more than R from the origin. (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* , < )
radcnvle.x 
|- ( ph -> X e. CC )
radcnvle.a 
|- ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )
Assertion radcnvle 
|- ( ph -> ( abs ` X ) <_ R )

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 radcnvle.x 
 |-  ( ph -> X e. CC )
5 radcnvle.a 
 |-  ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )
6 ressxr 
 |-  RR C_ RR*
7 4 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
8 6 7 sselid 
 |-  ( ph -> ( abs ` X ) e. RR* )
9 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
10 1 2 3 radcnvcl 
 |-  ( ph -> R e. ( 0 [,] +oo ) )
11 9 10 sselid 
 |-  ( ph -> R e. RR* )
12 simpr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> R < ( abs ` X ) )
13 11 adantr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> R e. RR* )
14 7 adantr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( abs ` X ) e. RR )
15 0xr 
 |-  0 e. RR*
16 pnfxr 
 |-  +oo e. RR*
17 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) ) )
18 15 16 17 mp2an 
 |-  ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) )
19 10 18 sylib 
 |-  ( ph -> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) )
20 19 simp2d 
 |-  ( ph -> 0 <_ R )
21 ge0gtmnf 
 |-  ( ( R e. RR* /\ 0 <_ R ) -> -oo < R )
22 11 20 21 syl2anc 
 |-  ( ph -> -oo < R )
23 22 adantr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> -oo < R )
24 8 adantr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( abs ` X ) e. RR* )
25 13 24 12 xrltled 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> R <_ ( abs ` X ) )
26 xrre 
 |-  ( ( ( R e. RR* /\ ( abs ` X ) e. RR ) /\ ( -oo < R /\ R <_ ( abs ` X ) ) ) -> R e. RR )
27 13 14 23 25 26 syl22anc 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> R e. RR )
28 avglt1 
 |-  ( ( R e. RR /\ ( abs ` X ) e. RR ) -> ( R < ( abs ` X ) <-> R < ( ( R + ( abs ` X ) ) / 2 ) ) )
29 27 14 28 syl2anc 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( R < ( abs ` X ) <-> R < ( ( R + ( abs ` X ) ) / 2 ) ) )
30 12 29 mpbid 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> R < ( ( R + ( abs ` X ) ) / 2 ) )
31 27 14 readdcld 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( R + ( abs ` X ) ) e. RR )
32 31 rehalfcld 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) e. RR )
33 ssrab2 
 |-  { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR
34 33 6 sstri 
 |-  { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR*
35 2 adantr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> A : NN0 --> CC )
36 32 recnd 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) e. CC )
37 4 adantr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> X e. CC )
38 0red 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> 0 e. RR )
39 20 adantr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> 0 <_ R )
40 38 27 32 39 30 lelttrd 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> 0 < ( ( R + ( abs ` X ) ) / 2 ) )
41 38 32 40 ltled 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> 0 <_ ( ( R + ( abs ` X ) ) / 2 ) )
42 32 41 absidd 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( abs ` ( ( R + ( abs ` X ) ) / 2 ) ) = ( ( R + ( abs ` X ) ) / 2 ) )
43 avglt2 
 |-  ( ( R e. RR /\ ( abs ` X ) e. RR ) -> ( R < ( abs ` X ) <-> ( ( R + ( abs ` X ) ) / 2 ) < ( abs ` X ) ) )
44 27 14 43 syl2anc 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( R < ( abs ` X ) <-> ( ( R + ( abs ` X ) ) / 2 ) < ( abs ` X ) ) )
45 12 44 mpbid 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) < ( abs ` X ) )
46 42 45 eqbrtrd 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( abs ` ( ( R + ( abs ` X ) ) / 2 ) ) < ( abs ` X ) )
47 5 adantr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )
48 1 35 36 37 46 47 radcnvlem3 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> seq 0 ( + , ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) ) e. dom ~~> )
49 fveq2 
 |-  ( y = ( ( R + ( abs ` X ) ) / 2 ) -> ( G ` y ) = ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) )
50 49 seqeq3d 
 |-  ( y = ( ( R + ( abs ` X ) ) / 2 ) -> seq 0 ( + , ( G ` y ) ) = seq 0 ( + , ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) ) )
51 50 eleq1d 
 |-  ( y = ( ( R + ( abs ` X ) ) / 2 ) -> ( seq 0 ( + , ( G ` y ) ) e. dom ~~> <-> seq 0 ( + , ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) ) e. dom ~~> ) )
52 fveq2 
 |-  ( r = y -> ( G ` r ) = ( G ` y ) )
53 52 seqeq3d 
 |-  ( r = y -> seq 0 ( + , ( G ` r ) ) = seq 0 ( + , ( G ` y ) ) )
54 53 eleq1d 
 |-  ( r = y -> ( seq 0 ( + , ( G ` r ) ) e. dom ~~> <-> seq 0 ( + , ( G ` y ) ) e. dom ~~> ) )
55 54 cbvrabv 
 |-  { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } = { y e. RR | seq 0 ( + , ( G ` y ) ) e. dom ~~> }
56 51 55 elrab2 
 |-  ( ( ( R + ( abs ` X ) ) / 2 ) e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } <-> ( ( ( R + ( abs ` X ) ) / 2 ) e. RR /\ seq 0 ( + , ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) ) e. dom ~~> ) )
57 32 48 56 sylanbrc 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
58 supxrub 
 |-  ( ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR* /\ ( ( R + ( abs ` X ) ) / 2 ) e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) -> ( ( R + ( abs ` X ) ) / 2 ) <_ sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) )
59 34 57 58 sylancr 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) <_ sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) )
60 59 3 breqtrrdi 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) <_ R )
61 32 27 60 lensymd 
 |-  ( ( ph /\ R < ( abs ` X ) ) -> -. R < ( ( R + ( abs ` X ) ) / 2 ) )
62 30 61 pm2.65da 
 |-  ( ph -> -. R < ( abs ` X ) )
63 8 11 62 xrnltled 
 |-  ( ph -> ( abs ` X ) <_ R )