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	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
	radcnv.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
	psergf.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
Assertion	psergf	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		pser.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2		radcnv.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
3		psergf.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4	1	pserval	⊢ ( 𝑋 ∈ ℂ → ( 𝐺 ‘ 𝑋 ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) )
5	4	adantl	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝐺 ‘ 𝑋 ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) )
6		ffvelrn	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
7	6	adantlr	⊢ ( ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑋 ∈ ℂ ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
8		expcl	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑚 ) ∈ ℂ )
9	8	adantll	⊢ ( ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑋 ∈ ℂ ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑚 ) ∈ ℂ )
10	7 9	mulcld	⊢ ( ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑋 ∈ ℂ ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ∈ ℂ )
11	5 10	fmpt3d	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ )
12	2 3 11	syl2anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ )