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=\left(x\in ℂ⟼\left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)\right)$$
	radcnv.a	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
	psergf.x	$$⊢\phi \to X\in ℂ$$
Assertion	psergf	$$⊢\phi \to G\left(X\right):{\mathbb{N}}_0⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		pser.g	$$⊢G=\left(x\in ℂ⟼\left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)\right)$$
2		radcnv.a	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
3		psergf.x	$$⊢\phi \to X\in ℂ$$
4	1	pserval	$$⊢X\in ℂ\to G\left(X\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)X^m\right)$$
5	4	adantl	$$⊢\left(A:{\mathbb{N}}_0⟶ℂ\wedge X\in ℂ\right)\to G\left(X\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)X^m\right)$$
6		ffvelrn	$$⊢\left(A:{\mathbb{N}}_0⟶ℂ\wedge m\in {\mathbb{N}}_0\right)\to A\left(m\right)\in ℂ$$
7	6	adantlr	$$⊢\left(\left(A:{\mathbb{N}}_0⟶ℂ\wedge X\in ℂ\right)\wedge m\in {\mathbb{N}}_0\right)\to A\left(m\right)\in ℂ$$
8		expcl	$$⊢\left(X\in ℂ\wedge m\in {\mathbb{N}}_0\right)\to X^m\in ℂ$$
9	8	adantll	$$⊢\left(\left(A:{\mathbb{N}}_0⟶ℂ\wedge X\in ℂ\right)\wedge m\in {\mathbb{N}}_0\right)\to X^m\in ℂ$$
10	7 9	mulcld	$$⊢\left(\left(A:{\mathbb{N}}_0⟶ℂ\wedge X\in ℂ\right)\wedge m\in {\mathbb{N}}_0\right)\to A\left(m\right)X^m\in ℂ$$
11	5 10	fmpt3d	$$⊢\left(A:{\mathbb{N}}_0⟶ℂ\wedge X\in ℂ\right)\to G\left(X\right):{\mathbb{N}}_0⟶ℂ$$
12	2 3 11	syl2anc	$$⊢\phi \to G\left(X\right):{\mathbb{N}}_0⟶ℂ$$