Metamath Proof Explorer

Theorem taylpval

Description: Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016)

Ref Expression
Hypotheses taylpfval.s ⊢ φ → S ∈ ℝ ℂ
taylpfval.f ⊢ φ → F : A ⟶ ℂ
taylpfval.a ⊢ φ → A ⊆ S
taylpfval.n ⊢ φ → N ∈ ℕ 0
taylpfval.b ⊢ φ → B ∈ dom ⁡ S D n F ⁡ N
taylpfval.t ⊢ T = N S Tayl F B
taylpval.x ⊢ φ → X ∈ ℂ
Assertion taylpval ⊢ φ → T ⁡ X = ∑ k = 0 N S D n F ⁡ k ⁡ B k ! ⁢ X − B k

Proof

Step Hyp Ref Expression
1 taylpfval.s ⊢ φ → S ∈ ℝ ℂ
2 taylpfval.f ⊢ φ → F : A ⟶ ℂ
3 taylpfval.a ⊢ φ → A ⊆ S
4 taylpfval.n ⊢ φ → N ∈ ℕ 0
5 taylpfval.b ⊢ φ → B ∈ dom ⁡ S D n F ⁡ N
6 taylpfval.t ⊢ T = N S Tayl F B
7 taylpval.x ⊢ φ → X ∈ ℂ
8 1 2 3 4 5 6 taylpfval ⊢ φ → T = x ∈ ℂ ⟼ ∑ k = 0 N S D n F ⁡ k ⁡ B k ! ⁢ x − B k
9 simplr ⊢ φ ∧ x = X ∧ k ∈ 0 … N → x = X
10 9 oveq1d ⊢ φ ∧ x = X ∧ k ∈ 0 … N → x − B = X − B
11 10 oveq1d ⊢ φ ∧ x = X ∧ k ∈ 0 … N → x − B k = X − B k
12 11 oveq2d ⊢ φ ∧ x = X ∧ k ∈ 0 … N → S D n F ⁡ k ⁡ B k ! ⁢ x − B k = S D n F ⁡ k ⁡ B k ! ⁢ X − B k
13 12 sumeq2dv ⊢ φ ∧ x = X → ∑ k = 0 N S D n F ⁡ k ⁡ B k ! ⁢ x − B k = ∑ k = 0 N S D n F ⁡ k ⁡ B k ! ⁢ X − B k
14 sumex ⊢ ∑ k = 0 N S D n F ⁡ k ⁡ B k ! ⁢ X − B k ∈ V
15 14 a1i ⊢ φ → ∑ k = 0 N S D n F ⁡ k ⁡ B k ! ⁢ X − B k ∈ V
16 8 13 7 15 fvmptd ⊢ φ → T ⁡ X = ∑ k = 0 N S D n F ⁡ k ⁡ B k ! ⁢ X − B k