Metamath Proof Explorer


Theorem dvntaylp0

Description: The first N derivatives of the Taylor polynomial at B match the derivatives of the function from which it is derived. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses dvntaylp0.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
dvntaylp0.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
dvntaylp0.a ( 𝜑𝐴𝑆 )
dvntaylp0.m ( 𝜑𝑀 ∈ ( 0 ... 𝑁 ) )
dvntaylp0.b ( 𝜑𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
dvntaylp0.t 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
Assertion dvntaylp0 ( 𝜑 → ( ( ( ℂ D𝑛 𝑇 ) ‘ 𝑀 ) ‘ 𝐵 ) = ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dvntaylp0.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 dvntaylp0.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
3 dvntaylp0.a ( 𝜑𝐴𝑆 )
4 dvntaylp0.m ( 𝜑𝑀 ∈ ( 0 ... 𝑁 ) )
5 dvntaylp0.b ( 𝜑𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
6 dvntaylp0.t 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7 elfz3nn0 ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
8 4 7 syl ( 𝜑𝑁 ∈ ℕ0 )
9 8 nn0cnd ( 𝜑𝑁 ∈ ℂ )
10 elfznn0 ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ0 )
11 4 10 syl ( 𝜑𝑀 ∈ ℕ0 )
12 11 nn0cnd ( 𝜑𝑀 ∈ ℂ )
13 9 12 npcand ( 𝜑 → ( ( 𝑁𝑀 ) + 𝑀 ) = 𝑁 )
14 13 oveq1d ( 𝜑 → ( ( ( 𝑁𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 ) )
15 14 6 syl6eqr ( 𝜑 → ( ( ( 𝑁𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) = 𝑇 )
16 15 oveq2d ( 𝜑 → ( ℂ D𝑛 ( ( ( 𝑁𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) = ( ℂ D𝑛 𝑇 ) )
17 16 fveq1d ( 𝜑 → ( ( ℂ D𝑛 ( ( ( 𝑁𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( ( ℂ D𝑛 𝑇 ) ‘ 𝑀 ) )
18 fznn0sub ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑁𝑀 ) ∈ ℕ0 )
19 4 18 syl ( 𝜑 → ( 𝑁𝑀 ) ∈ ℕ0 )
20 13 fveq2d ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( ( 𝑁𝑀 ) + 𝑀 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
21 20 dmeqd ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( ( 𝑁𝑀 ) + 𝑀 ) ) = dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
22 5 21 eleqtrrd ( 𝜑𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( ( 𝑁𝑀 ) + 𝑀 ) ) )
23 1 2 3 11 19 22 dvntaylp ( 𝜑 → ( ( ℂ D𝑛 ( ( ( 𝑁𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( ( 𝑁𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )
24 17 23 eqtr3d ( 𝜑 → ( ( ℂ D𝑛 𝑇 ) ‘ 𝑀 ) = ( ( 𝑁𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )
25 24 fveq1d ( 𝜑 → ( ( ( ℂ D𝑛 𝑇 ) ‘ 𝑀 ) ‘ 𝐵 ) = ( ( ( 𝑁𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ‘ 𝐵 ) )
26 cnex ℂ ∈ V
27 26 a1i ( 𝜑 → ℂ ∈ V )
28 elpm2r ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
29 27 1 2 3 28 syl22anc ( 𝜑𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
30 dvnf ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ⟶ ℂ )
31 1 29 11 30 syl3anc ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ⟶ ℂ )
32 dvnbss ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ⊆ dom 𝐹 )
33 1 29 11 32 syl3anc ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ⊆ dom 𝐹 )
34 2 33 fssdmd ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ⊆ 𝐴 )
35 34 3 sstrd ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ⊆ 𝑆 )
36 19 orcd ( 𝜑 → ( ( 𝑁𝑀 ) ∈ ℕ0 ∨ ( 𝑁𝑀 ) = +∞ ) )
37 dvnadd ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ ( 𝑁𝑀 ) ∈ ℕ0 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁𝑀 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁𝑀 ) ) ) )
38 1 29 11 19 37 syl22anc ( 𝜑 → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁𝑀 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁𝑀 ) ) ) )
39 12 9 pncan3d ( 𝜑 → ( 𝑀 + ( 𝑁𝑀 ) ) = 𝑁 )
40 39 fveq2d ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁𝑀 ) ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
41 38 40 eqtrd ( 𝜑 → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁𝑀 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
42 41 dmeqd ( 𝜑 → dom ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁𝑀 ) ) = dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
43 5 42 eleqtrrd ( 𝜑𝐵 ∈ dom ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁𝑀 ) ) )
44 1 31 35 19 43 taylplem1 ( ( 𝜑𝑘 ∈ ( ( 0 [,] ( 𝑁𝑀 ) ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) )
45 eqid ( ( 𝑁𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) = ( ( 𝑁𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 )
46 1 31 35 36 44 45 tayl0 ( 𝜑 → ( 𝐵 ∈ dom ( ( 𝑁𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ∧ ( ( ( 𝑁𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ‘ 𝐵 ) = ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ‘ 𝐵 ) ) )
47 46 simprd ( 𝜑 → ( ( ( 𝑁𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ‘ 𝐵 ) = ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ‘ 𝐵 ) )
48 25 47 eqtrd ( 𝜑 → ( ( ( ℂ D𝑛 𝑇 ) ‘ 𝑀 ) ‘ 𝐵 ) = ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ‘ 𝐵 ) )