This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pserval2

Description: Value of the function G that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypothesis pser.g ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
Assertion pserval2 ⊢ X ∈ ℂ ∧ N ∈ ℕ 0 → G ⁡ X ⁡ N = A ⁡ N ⁢ X N

Proof

Step Hyp Ref Expression
1 pser.g ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
2 1 pserval ⊢ X ∈ ℂ → G ⁡ X = y ∈ ℕ 0 ⟼ A ⁡ y ⁢ X y
3 2 fveq1d ⊢ X ∈ ℂ → G ⁡ X ⁡ N = y ∈ ℕ 0 ⟼ A ⁡ y ⁢ X y ⁡ N
4 fveq2 ⊢ y = N → A ⁡ y = A ⁡ N
5 oveq2 ⊢ y = N → X y = X N
6 4 5 oveq12d ⊢ y = N → A ⁡ y ⁢ X y = A ⁡ N ⁢ X N
7 eqid ⊢ y ∈ ℕ 0 ⟼ A ⁡ y ⁢ X y = y ∈ ℕ 0 ⟼ A ⁡ y ⁢ X y
8 ovex ⊢ A ⁡ N ⁢ X N ∈ V
9 6 7 8 fvmpt ⊢ N ∈ ℕ 0 → y ∈ ℕ 0 ⟼ A ⁡ y ⁢ X y ⁡ N = A ⁡ N ⁢ X N
10 3 9 sylan9eq ⊢ X ∈ ℂ ∧ N ∈ ℕ 0 → G ⁡ X ⁡ N = A ⁡ N ⁢ X N