This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psergf

Description: The sequence of terms in the infinite sequence defining a power series for fixed 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 )
Assertion psergf 
|- ( ph -> ( G ` X ) : NN0 --> CC )

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 1 pserval 
 |-  ( X e. CC -> ( G ` X ) = ( m e. NN0 |-> ( ( A ` m ) x. ( X ^ m ) ) ) )
5 4 adantl 
 |-  ( ( A : NN0 --> CC /\ X e. CC ) -> ( G ` X ) = ( m e. NN0 |-> ( ( A ` m ) x. ( X ^ m ) ) ) )
6 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ m e. NN0 ) -> ( A ` m ) e. CC )
7 6 adantlr 
 |-  ( ( ( A : NN0 --> CC /\ X e. CC ) /\ m e. NN0 ) -> ( A ` m ) e. CC )
8 expcl 
 |-  ( ( X e. CC /\ m e. NN0 ) -> ( X ^ m ) e. CC )
9 8 adantll 
 |-  ( ( ( A : NN0 --> CC /\ X e. CC ) /\ m e. NN0 ) -> ( X ^ m ) e. CC )
10 7 9 mulcld 
 |-  ( ( ( A : NN0 --> CC /\ X e. CC ) /\ m e. NN0 ) -> ( ( A ` m ) x. ( X ^ m ) ) e. CC )
11 5 10 fmpt3d 
 |-  ( ( A : NN0 --> CC /\ X e. CC ) -> ( G ` X ) : NN0 --> CC )
12 2 3 11 syl2anc 
 |-  ( ph -> ( G ` X ) : NN0 --> CC )