Metamath Proof Explorer


Theorem 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 𝐵 ) )