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 ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ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 ffvelcdm ⊢ ( ( 𝐴 : ℕ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 ⟶ ℂ )