# 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 ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
dvntaylp0.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
dvntaylp0.a ${⊢}{\phi }\to {A}\subseteq {S}$
dvntaylp0.m ${⊢}{\phi }\to {M}\in \left(0\dots {N}\right)$
dvntaylp0.b ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
dvntaylp0.t ${⊢}{T}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
Assertion dvntaylp0 ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({M}\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({M}\right)\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 dvntaylp0.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 dvntaylp0.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
3 dvntaylp0.a ${⊢}{\phi }\to {A}\subseteq {S}$
4 dvntaylp0.m ${⊢}{\phi }\to {M}\in \left(0\dots {N}\right)$
5 dvntaylp0.b ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
6 dvntaylp0.t ${⊢}{T}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
7 elfz3nn0 ${⊢}{M}\in \left(0\dots {N}\right)\to {N}\in {ℕ}_{0}$
8 4 7 syl ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
9 8 nn0cnd ${⊢}{\phi }\to {N}\in ℂ$
10 elfznn0 ${⊢}{M}\in \left(0\dots {N}\right)\to {M}\in {ℕ}_{0}$
11 4 10 syl ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
12 11 nn0cnd ${⊢}{\phi }\to {M}\in ℂ$
13 9 12 npcand ${⊢}{\phi }\to {N}-{M}+{M}={N}$
14 13 oveq1d ${⊢}{\phi }\to \left({N}-{M}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
15 14 6 syl6eqr ${⊢}{\phi }\to \left({N}-{M}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}={T}$
16 15 oveq2d ${⊢}{\phi }\to ℂ{D}^{n}\left(\left({N}-{M}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)=ℂ{D}^{n}{T}$
17 16 fveq1d ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left({N}-{M}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)=\left(ℂ{D}^{n}{T}\right)\left({M}\right)$
18 fznn0sub ${⊢}{M}\in \left(0\dots {N}\right)\to {N}-{M}\in {ℕ}_{0}$
19 4 18 syl ${⊢}{\phi }\to {N}-{M}\in {ℕ}_{0}$
20 13 fveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-{M}+{M}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
21 20 dmeqd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-{M}+{M}\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
22 5 21 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-{M}+{M}\right)$
23 1 2 3 11 19 22 dvntaylp ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left({N}-{M}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)=\left({N}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}$
24 17 23 eqtr3d ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({M}\right)=\left({N}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}$
25 24 fveq1d ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({M}\right)\left({B}\right)=\left(\left({N}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}\right)\left({B}\right)$
26 cnex ${⊢}ℂ\in \mathrm{V}$
27 26 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
28 elpm2r ${⊢}\left(\left(ℂ\in \mathrm{V}\wedge {S}\in \left\{ℝ,ℂ\right\}\right)\wedge \left({F}:{A}⟶ℂ\wedge {A}\subseteq {S}\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
29 27 1 2 3 28 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
30 dvnf ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({M}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)⟶ℂ$
31 1 29 11 30 syl3anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({M}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)⟶ℂ$
32 dvnbss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {M}\in {ℕ}_{0}\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)\subseteq \mathrm{dom}{F}$
33 1 29 11 32 syl3anc ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)\subseteq \mathrm{dom}{F}$
34 2 33 fssdmd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)\subseteq {A}$
35 34 3 sstrd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({M}\right)\subseteq {S}$
36 19 orcd ${⊢}{\phi }\to \left({N}-{M}\in {ℕ}_{0}\vee {N}-{M}=\mathrm{+\infty }\right)$
37 dvnadd ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge \left({M}\in {ℕ}_{0}\wedge {N}-{M}\in {ℕ}_{0}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}-{M}\right)$
38 1 29 11 19 37 syl22anc ${⊢}{\phi }\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)=\left({S}{D}^{n}{F}\right)\left({M}+{N}-{M}\right)$
39 12 9 pncan3d ${⊢}{\phi }\to {M}+{N}-{M}={N}$
40 39 fveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({M}+{N}-{M}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
41 38 40 eqtrd ${⊢}{\phi }\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
42 41 dmeqd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
43 5 42 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({N}-{M}\right)$
44 1 31 35 19 43 taylplem1 ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}-{M}\right]\cap ℤ\right)\right)\to {B}\in \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({M}\right)\right)\left({k}\right)$
45 eqid ${⊢}\left({N}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}=\left({N}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}$
46 1 31 35 36 44 45 tayl0 ${⊢}{\phi }\to \left({B}\in \mathrm{dom}\left(\left({N}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}\right)\wedge \left(\left({N}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({M}\right)\left({B}\right)\right)$
47 46 simprd ${⊢}{\phi }\to \left(\left({N}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({M}\right)\left({B}\right)$
48 25 47 eqtrd ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({M}\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({M}\right)\left({B}\right)$