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		ffvelrn	|- ( ( 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 )