taylth

Description: Taylor's theorem. The Taylor polynomial of a N -times differentiable function is such that the error term goes to zero faster than ( x - B ) ^ N . This is Metamath 100 proof #35. (Contributed by Mario Carneiro, 1-Jan-2017)

	Ref	Expression
Hypotheses	taylth.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
	taylth.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	taylth.d	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) = 𝐴 )
	taylth.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	taylth.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	taylth.t	⊢ 𝑇 = ( 𝑁 ( ℝ Tayl 𝐹 ) 𝐵 )
	taylth.r	⊢ 𝑅 = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝑇 ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑁 ) ) )
Assertion	taylth	⊢ ( 𝜑 → 0 ∈ ( 𝑅 lim_ℂ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		taylth.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2		taylth.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		taylth.d	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) = 𝐴 )
4		taylth.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		taylth.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
6		taylth.t	⊢ 𝑇 = ( 𝑁 ( ℝ Tayl 𝐹 ) 𝐵 )
7		taylth.r	⊢ 𝑅 = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝑇 ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑁 ) ) )
8		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
9	8	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
10		ax-resscn	⊢ ℝ ⊆ ℂ
11		fss	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
12	1 10 11	sylancl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
13	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → 𝐹 : 𝐴 ⟶ ℝ )
14	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → 𝐴 ⊆ ℝ )
15	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) = 𝐴 )
16	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → 𝑁 ∈ ℕ )
17	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → 𝐵 ∈ 𝐴 )
18		simprl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → 𝑚 ∈ ( 1 ..^ 𝑁 ) )
19		simprr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) )
20		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) = ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) )
21		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) = ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) )
22	20 21	oveq12d	⊢ ( 𝑦 = 𝑥 → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) ) )
23		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 − 𝐵 ) = ( 𝑥 − 𝐵 ) )
24	23	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) = ( ( 𝑥 − 𝐵 ) ↑ 𝑚 ) )
25	22 24	oveq12d	⊢ ( 𝑦 = 𝑥 → ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) = ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑚 ) ) )
26	25	cbvmptv	⊢ ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑚 ) ) )
27	26	oveq1i	⊢ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 )
28	19 27	eleqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) )
29	13 14 15 16 17 6 18 28	taylthlem2	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑚 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑚 ) ) ) lim_ℂ 𝐵 ) ) ) → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑚 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑚 + 1 ) ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ ( 𝑚 + 1 ) ) ) ) lim_ℂ 𝐵 ) )
30	9 12 2 3 4 5 6 7 29	taylthlem1	⊢ ( 𝜑 → 0 ∈ ( 𝑅 lim_ℂ 𝐵 ) )

Metamath Proof Explorer

Theorem taylth

Proof