Metamath Proof Explorer

Theorem radcnv0

Description: Zero is always a convergent point for any power series. (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 )
Assertion radcnv0 
|- ( ph -> 0 e. { r e. RR | seq 0 ( + , ( G ` r ) ) 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 fveq2 
 |-  ( r = 0 -> ( G ` r ) = ( G ` 0 ) )
4 3 seqeq3d 
 |-  ( r = 0 -> seq 0 ( + , ( G ` r ) ) = seq 0 ( + , ( G ` 0 ) ) )
5 4 eleq1d 
 |-  ( r = 0 -> ( seq 0 ( + , ( G ` r ) ) e. dom ~~> <-> seq 0 ( + , ( G ` 0 ) ) e. dom ~~> ) )
6 0red 
 |-  ( ph -> 0 e. RR )
7 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
8 0zd 
 |-  ( ph -> 0 e. ZZ )
9 snfi 
 |-  { 0 } e. Fin
10 9 a1i 
 |-  ( ph -> { 0 } e. Fin )
11 0nn0 
 |-  0 e. NN0
12 11 a1i 
 |-  ( ph -> 0 e. NN0 )
13 12 snssd 
 |-  ( ph -> { 0 } C_ NN0 )
14 ifid 
 |-  if ( k e. { 0 } , ( ( G ` 0 ) ` k ) , ( ( G ` 0 ) ` k ) ) = ( ( G ` 0 ) ` k )
15 0cnd 
 |-  ( ph -> 0 e. CC )
16 1 pserval2 
 |-  ( ( 0 e. CC /\ k e. NN0 ) -> ( ( G ` 0 ) ` k ) = ( ( A ` k ) x. ( 0 ^ k ) ) )
17 15 16 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` 0 ) ` k ) = ( ( A ` k ) x. ( 0 ^ k ) ) )
18 17 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k e. { 0 } ) -> ( ( G ` 0 ) ` k ) = ( ( A ` k ) x. ( 0 ^ k ) ) )
19 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
20 elnn0 
 |-  ( k e. NN0 <-> ( k e. NN \/ k = 0 ) )
21 19 20 sylib 
 |-  ( ( ph /\ k e. NN0 ) -> ( k e. NN \/ k = 0 ) )
22 21 ord 
 |-  ( ( ph /\ k e. NN0 ) -> ( -. k e. NN -> k = 0 ) )
23 velsn 
 |-  ( k e. { 0 } <-> k = 0 )
24 22 23 imbitrrdi 
 |-  ( ( ph /\ k e. NN0 ) -> ( -. k e. NN -> k e. { 0 } ) )
25 24 con1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( -. k e. { 0 } -> k e. NN ) )
26 25 imp 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k e. { 0 } ) -> k e. NN )
27 26 0expd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k e. { 0 } ) -> ( 0 ^ k ) = 0 )
28 27 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k e. { 0 } ) -> ( ( A ` k ) x. ( 0 ^ k ) ) = ( ( A ` k ) x. 0 ) )
29 2 ffvelcdmda 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. CC )
30 29 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k e. { 0 } ) -> ( A ` k ) e. CC )
31 30 mul01d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k e. { 0 } ) -> ( ( A ` k ) x. 0 ) = 0 )
32 18 28 31 3eqtrd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k e. { 0 } ) -> ( ( G ` 0 ) ` k ) = 0 )
33 32 ifeq2da 
 |-  ( ( ph /\ k e. NN0 ) -> if ( k e. { 0 } , ( ( G ` 0 ) ` k ) , ( ( G ` 0 ) ` k ) ) = if ( k e. { 0 } , ( ( G ` 0 ) ` k ) , 0 ) )
34 14 33 eqtr3id 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` 0 ) ` k ) = if ( k e. { 0 } , ( ( G ` 0 ) ` k ) , 0 ) )
35 13 sselda 
 |-  ( ( ph /\ k e. { 0 } ) -> k e. NN0 )
36 1 2 15 psergf 
 |-  ( ph -> ( G ` 0 ) : NN0 --> CC )
37 36 ffvelcdmda 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` 0 ) ` k ) e. CC )
38 35 37 syldan 
 |-  ( ( ph /\ k e. { 0 } ) -> ( ( G ` 0 ) ` k ) e. CC )
39 7 8 10 13 34 38 fsumcvg3 
 |-  ( ph -> seq 0 ( + , ( G ` 0 ) ) e. dom ~~> )
40 5 6 39 elrabd 
 |-  ( ph -> 0 e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )