Metamath Proof Explorer

Theorem radcnvcl

Description: The radius of convergence R of an infinite series is a nonnegative extended real number. (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* , < )
Assertion radcnvcl 
|- ( ph -> R e. ( 0 [,] +oo ) )

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 ssrab2 
 |-  { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR
5 ressxr 
 |-  RR C_ RR*
6 4 5 sstri 
 |-  { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR*
7 supxrcl 
 |-  ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR* -> sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
8 6 7 mp1i 
 |-  ( ph -> sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
9 3 8 eqeltrid 
 |-  ( ph -> R e. RR* )
10 1 2 radcnv0 
 |-  ( ph -> 0 e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
11 supxrub 
 |-  ( ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR* /\ 0 e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) -> 0 <_ sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) )
12 6 10 11 sylancr 
 |-  ( ph -> 0 <_ sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) )
13 12 3 breqtrrdi 
 |-  ( ph -> 0 <_ R )
14 pnfge 
 |-  ( R e. RR* -> R <_ +oo )
15 9 14 syl 
 |-  ( ph -> R <_ +oo )
16 0xr 
 |-  0 e. RR*
17 pnfxr 
 |-  +oo e. RR*
18 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) ) )
19 16 17 18 mp2an 
 |-  ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) )
20 9 13 15 19 syl3anbrc 
 |-  ( ph -> R e. ( 0 [,] +oo ) )