psergf

Description: The sequence of terms in the infinite sequence defining a power series for fixed X . (Contributed by Mario Carneiro, 26-Feb-2015)

Step	Hyp	Ref	Expression
1		pser.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		radcnv.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
3		psergf.x	$⊢ φ \to X \in ℂ$
4	1	pserval	$⊢ X \in ℂ \to G (X) = (m \in ℕ_{0} ⟼ A (m) X^{m})$
5	4	adantl	$⊢ (A : ℕ_{0} ⟶ ℂ \land X \in ℂ) \to G (X) = (m \in ℕ_{0} ⟼ A (m) X^{m})$
6		ffvelcdm	$⊢ (A : ℕ_{0} ⟶ ℂ \land m \in ℕ_{0}) \to A (m) \in ℂ$
7	6	adantlr	$⊢ ((A : ℕ_{0} ⟶ ℂ \land X \in ℂ) \land m \in ℕ_{0}) \to A (m) \in ℂ$
8		expcl	$⊢ (X \in ℂ \land m \in ℕ_{0}) \to X^{m} \in ℂ$
9	8	adantll	$⊢ ((A : ℕ_{0} ⟶ ℂ \land X \in ℂ) \land m \in ℕ_{0}) \to X^{m} \in ℂ$
10	7 9	mulcld	$⊢ ((A : ℕ_{0} ⟶ ℂ \land X \in ℂ) \land m \in ℕ_{0}) \to A (m) X^{m} \in ℂ$
11	5 10	fmpt3d	$⊢ (A : ℕ_{0} ⟶ ℂ \land X \in ℂ) \to G (X) : ℕ_{0} ⟶ ℂ$
12	2 3 11	syl2anc	$⊢ φ \to G (X) : ℕ_{0} ⟶ ℂ$

Metamath Proof Explorer