Metamath Proof Explorer

Theorem taylpval

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

		Ref	Expression
	Hypotheses	taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
		taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
		taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
		taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
		taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
		taylpfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
		taylpval.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	Assertion	taylpval	⊢ ( 𝜑 → ( 𝑇 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) )

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
5		taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
6		taylpfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7		taylpval.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
8	1 2 3 4 5 6	taylpfval	⊢ ( 𝜑 → 𝑇 = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) )
9		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑥 = 𝑋 )
10	9	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 − 𝐵 ) = ( 𝑋 − 𝐵 ) )
11	10	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) = ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) )
12	11	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) = ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) )
13	12	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) )
14		sumex	⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ∈ V
15	14	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ∈ V )
16	8 13 7 15	fvmptd	⊢ ( 𝜑 → ( 𝑇 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) )