# Metamath Proof Explorer

## Theorem dvntaylp

Description: The M -th derivative of the Taylor polynomial is the Taylor polynomial of the M -th derivative of the function. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses dvntaylp.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
dvntaylp.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
dvntaylp.a ${⊢}{\phi }\to {A}\subseteq {S}$
dvntaylp.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
dvntaylp.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
dvntaylp.b ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+{M}\right)$
Assertion dvntaylp ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)={N}\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}$

### Proof

Step Hyp Ref Expression
1 dvntaylp.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 dvntaylp.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
3 dvntaylp.a ${⊢}{\phi }\to {A}\subseteq {S}$
4 dvntaylp.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
5 dvntaylp.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
6 dvntaylp.b ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+{M}\right)$
7 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
8 4 7 eleqtrdi ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
9 eluzfz2b ${⊢}{M}\in {ℤ}_{\ge 0}↔{M}\in \left(0\dots {M}\right)$
10 8 9 sylib ${⊢}{\phi }\to {M}\in \left(0\dots {M}\right)$
11 fveq2 ${⊢}{m}=0\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left(0\right)$
12 fveq2 ${⊢}{m}=0\to \left({S}{D}^{n}{F}\right)\left({m}\right)=\left({S}{D}^{n}{F}\right)\left(0\right)$
13 12 oveq2d ${⊢}{m}=0\to {S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)={S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left(0\right)$
14 oveq2 ${⊢}{m}=0\to {M}-{m}={M}-0$
15 14 oveq2d ${⊢}{m}=0\to {N}+{M}-{m}={N}+{M}-0$
16 eqidd ${⊢}{m}=0\to {B}={B}$
17 13 15 16 oveq123d ${⊢}{m}=0\to \left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}=\left({N}+{M}-0\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left(0\right)\right){B}$
18 11 17 eqeq12d ${⊢}{m}=0\to \left(\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}↔\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left(0\right)=\left({N}+{M}-0\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left(0\right)\right){B}\right)$
19 18 imbi2d ${⊢}{m}=0\to \left(\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}\right)↔\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left(0\right)=\left({N}+{M}-0\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left(0\right)\right){B}\right)\right)$
20 fveq2 ${⊢}{m}={n}\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)$
21 fveq2 ${⊢}{m}={n}\to \left({S}{D}^{n}{F}\right)\left({m}\right)=\left({S}{D}^{n}{F}\right)\left({n}\right)$
22 21 oveq2d ${⊢}{m}={n}\to {S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)={S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)$
23 oveq2 ${⊢}{m}={n}\to {M}-{m}={M}-{n}$
24 23 oveq2d ${⊢}{m}={n}\to {N}+{M}-{m}={N}+{M}-{n}$
25 eqidd ${⊢}{m}={n}\to {B}={B}$
26 22 24 25 oveq123d ${⊢}{m}={n}\to \left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}=\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}$
27 20 26 eqeq12d ${⊢}{m}={n}\to \left(\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}↔\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)=\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)$
28 27 imbi2d ${⊢}{m}={n}\to \left(\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}\right)↔\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)=\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)\right)$
29 fveq2 ${⊢}{m}={n}+1\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)$
30 fveq2 ${⊢}{m}={n}+1\to \left({S}{D}^{n}{F}\right)\left({m}\right)=\left({S}{D}^{n}{F}\right)\left({n}+1\right)$
31 30 oveq2d ${⊢}{m}={n}+1\to {S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)={S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)$
32 oveq2 ${⊢}{m}={n}+1\to {M}-{m}={M}-\left({n}+1\right)$
33 32 oveq2d ${⊢}{m}={n}+1\to {N}+{M}-{m}={N}+{M}-\left({n}+1\right)$
34 eqidd ${⊢}{m}={n}+1\to {B}={B}$
35 31 33 34 oveq123d ${⊢}{m}={n}+1\to \left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}$
36 29 35 eqeq12d ${⊢}{m}={n}+1\to \left(\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}↔\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}\right)$
37 36 imbi2d ${⊢}{m}={n}+1\to \left(\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}\right)↔\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}\right)\right)$
38 fveq2 ${⊢}{m}={M}\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)$
39 fveq2 ${⊢}{m}={M}\to \left({S}{D}^{n}{F}\right)\left({m}\right)=\left({S}{D}^{n}{F}\right)\left({M}\right)$
40 39 oveq2d ${⊢}{m}={M}\to {S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)={S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)$
41 oveq2 ${⊢}{m}={M}\to {M}-{m}={M}-{M}$
42 41 oveq2d ${⊢}{m}={M}\to {N}+{M}-{m}={N}+{M}-{M}$
43 eqidd ${⊢}{m}={M}\to {B}={B}$
44 40 42 43 oveq123d ${⊢}{m}={M}\to \left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}=\left({N}+{M}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}$
45 38 44 eqeq12d ${⊢}{m}={M}\to \left(\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}↔\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)=\left({N}+{M}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}\right)$
46 45 imbi2d ${⊢}{m}={M}\to \left(\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({m}\right)=\left({N}+{M}-{m}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({m}\right)\right){B}\right)↔\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)=\left({N}+{M}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}\right)\right)$
47 ssidd ${⊢}{\phi }\to ℂ\subseteq ℂ$
48 mapsspm ${⊢}{ℂ}^{ℂ}\subseteq ℂ{↑}_{𝑝𝑚}ℂ$
49 5 4 nn0addcld ${⊢}{\phi }\to {N}+{M}\in {ℕ}_{0}$
50 eqid ${⊢}\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}=\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}$
51 1 2 3 49 6 50 taylpf ${⊢}{\phi }\to \left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right):ℂ⟶ℂ$
52 cnex ${⊢}ℂ\in \mathrm{V}$
53 52 52 elmap ${⊢}\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\in \left({ℂ}^{ℂ}\right)↔\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right):ℂ⟶ℂ$
54 51 53 sylibr ${⊢}{\phi }\to \left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\in \left({ℂ}^{ℂ}\right)$
55 48 54 sseldi ${⊢}{\phi }\to \left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)$
56 dvn0 ${⊢}\left(ℂ\subseteq ℂ\wedge \left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\right)\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left(0\right)=\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}$
57 47 55 56 syl2anc ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left(0\right)=\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}$
58 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
59 1 58 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
60 52 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
61 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)$
62 60 1 2 3 61 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
63 dvn0 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}{F}\right)\left(0\right)={F}$
64 59 62 63 syl2anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left(0\right)={F}$
65 64 oveq2d ${⊢}{\phi }\to {S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left(0\right)={S}\mathrm{Tayl}{F}$
66 4 nn0cnd ${⊢}{\phi }\to {M}\in ℂ$
67 66 subid1d ${⊢}{\phi }\to {M}-0={M}$
68 67 oveq2d ${⊢}{\phi }\to {N}+{M}-0={N}+{M}$
69 eqidd ${⊢}{\phi }\to {B}={B}$
70 65 68 69 oveq123d ${⊢}{\phi }\to \left({N}+{M}-0\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left(0\right)\right){B}=\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}$
71 57 70 eqtr4d ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left(0\right)=\left({N}+{M}-0\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left(0\right)\right){B}$
72 71 a1i ${⊢}{M}\in {ℤ}_{\ge 0}\to \left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left(0\right)=\left({N}+{M}-0\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left(0\right)\right){B}\right)$
73 oveq2 ${⊢}\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)=\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\to ℂ\mathrm{D}\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)=ℂ\mathrm{D}\left(\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)$
74 ssidd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to ℂ\subseteq ℂ$
75 55 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)$
76 elfzouz ${⊢}{n}\in \left(0..^{M}\right)\to {n}\in {ℤ}_{\ge 0}$
77 76 adantl ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {n}\in {ℤ}_{\ge 0}$
78 77 7 eleqtrrdi ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {n}\in {ℕ}_{0}$
79 dvnp1 ${⊢}\left(ℂ\subseteq ℂ\wedge \left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge {n}\in {ℕ}_{0}\right)\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)=ℂ\mathrm{D}\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)$
80 74 75 78 79 syl3anc ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)=ℂ\mathrm{D}\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)$
81 1 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
82 62 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
83 dvnf ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({n}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({n}\right)⟶ℂ$
84 81 82 78 83 syl3anc ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({n}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({n}\right)⟶ℂ$
85 dvnbss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {n}\in {ℕ}_{0}\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({n}\right)\subseteq \mathrm{dom}{F}$
86 81 82 78 85 syl3anc ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({n}\right)\subseteq \mathrm{dom}{F}$
87 2 fdmd ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
88 87 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \mathrm{dom}{F}={A}$
89 86 88 sseqtrd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({n}\right)\subseteq {A}$
90 3 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {A}\subseteq {S}$
91 89 90 sstrd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({n}\right)\subseteq {S}$
92 5 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}\in {ℕ}_{0}$
93 fzofzp1 ${⊢}{n}\in \left(0..^{M}\right)\to {n}+1\in \left(0\dots {M}\right)$
94 93 adantl ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {n}+1\in \left(0\dots {M}\right)$
95 fznn0sub ${⊢}{n}+1\in \left(0\dots {M}\right)\to {M}-\left({n}+1\right)\in {ℕ}_{0}$
96 94 95 syl ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {M}-\left({n}+1\right)\in {ℕ}_{0}$
97 92 96 nn0addcld ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}+{M}-\left({n}+1\right)\in {ℕ}_{0}$
98 6 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+{M}\right)$
99 elfzofz ${⊢}{n}\in \left(0..^{M}\right)\to {n}\in \left(0\dots {M}\right)$
100 99 adantl ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {n}\in \left(0\dots {M}\right)$
101 fznn0sub ${⊢}{n}\in \left(0\dots {M}\right)\to {M}-{n}\in {ℕ}_{0}$
102 100 101 syl ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {M}-{n}\in {ℕ}_{0}$
103 92 102 nn0addcld ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}+{M}-{n}\in {ℕ}_{0}$
104 dvnadd ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge \left({n}\in {ℕ}_{0}\wedge {N}+{M}-{n}\in {ℕ}_{0}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({n}\right)\right)\left({N}+{M}-{n}\right)=\left({S}{D}^{n}{F}\right)\left({n}+{N}+\left({M}-{n}\right)\right)$
105 81 82 78 103 104 syl22anc ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({n}\right)\right)\left({N}+{M}-{n}\right)=\left({S}{D}^{n}{F}\right)\left({n}+{N}+\left({M}-{n}\right)\right)$
106 5 nn0cnd ${⊢}{\phi }\to {N}\in ℂ$
107 106 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}\in ℂ$
108 96 nn0cnd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {M}-\left({n}+1\right)\in ℂ$
109 1cnd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to 1\in ℂ$
110 107 108 109 addassd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}+\left({M}-\left({n}+1\right)\right)+1={N}+\left({M}-\left({n}+1\right)\right)+1$
111 66 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {M}\in ℂ$
112 78 nn0cnd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {n}\in ℂ$
113 111 112 109 nppcan2d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {M}-\left({n}+1\right)+1={M}-{n}$
114 113 oveq2d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}+\left({M}-\left({n}+1\right)\right)+1={N}+{M}-{n}$
115 110 114 eqtrd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}+\left({M}-\left({n}+1\right)\right)+1={N}+{M}-{n}$
116 115 fveq2d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({n}\right)\right)\left({N}+\left({M}-\left({n}+1\right)\right)+1\right)=\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({n}\right)\right)\left({N}+{M}-{n}\right)$
117 112 111 pncan3d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {n}+{M}-{n}={M}$
118 117 oveq2d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}+{n}+\left({M}-{n}\right)={N}+{M}$
119 111 112 subcld ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {M}-{n}\in ℂ$
120 107 112 119 add12d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}+{n}+\left({M}-{n}\right)={n}+{N}+\left({M}-{n}\right)$
121 118 120 eqtr3d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {N}+{M}={n}+{N}+\left({M}-{n}\right)$
122 121 fveq2d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({N}+{M}\right)=\left({S}{D}^{n}{F}\right)\left({n}+{N}+\left({M}-{n}\right)\right)$
123 105 116 122 3eqtr4d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({n}\right)\right)\left({N}+\left({M}-\left({n}+1\right)\right)+1\right)=\left({S}{D}^{n}{F}\right)\left({N}+{M}\right)$
124 123 dmeqd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({n}\right)\right)\left({N}+\left({M}-\left({n}+1\right)\right)+1\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+{M}\right)$
125 98 124 eleqtrrd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {B}\in \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({n}\right)\right)\left({N}+\left({M}-\left({n}+1\right)\right)+1\right)$
126 81 84 91 97 125 dvtaylp ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to ℂ\mathrm{D}\left(\left({N}+\left({M}-\left({n}+1\right)\right)+1\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}{\left({S}{D}^{n}{F}\right)\left({n}\right)}_{{S}}^{\prime }\right){B}$
127 115 oveq1d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({N}+\left({M}-\left({n}+1\right)\right)+1\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}=\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}$
128 127 oveq2d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to ℂ\mathrm{D}\left(\left({N}+\left({M}-\left({n}+1\right)\right)+1\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)=ℂ\mathrm{D}\left(\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)$
129 59 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {S}\subseteq ℂ$
130 dvnp1 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({n}+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({n}\right)$
131 129 82 78 130 syl3anc ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({n}+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({n}\right)$
132 131 oveq2d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)={S}\mathrm{Tayl}{\left({S}{D}^{n}{F}\right)\left({n}\right)}_{{S}}^{\prime }$
133 132 eqcomd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to {S}\mathrm{Tayl}{\left({S}{D}^{n}{F}\right)\left({n}\right)}_{{S}}^{\prime }={S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)$
134 133 oveqd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}{\left({S}{D}^{n}{F}\right)\left({n}\right)}_{{S}}^{\prime }\right){B}=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}$
135 126 128 134 3eqtr3rd ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}=ℂ\mathrm{D}\left(\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)$
136 80 135 eqeq12d ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left(\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}↔ℂ\mathrm{D}\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)=ℂ\mathrm{D}\left(\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)\right)$
137 73 136 syl5ibr ${⊢}\left({\phi }\wedge {n}\in \left(0..^{M}\right)\right)\to \left(\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)=\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}\right)$
138 137 expcom ${⊢}{n}\in \left(0..^{M}\right)\to \left({\phi }\to \left(\left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)=\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}\right)\right)$
139 138 a2d ${⊢}{n}\in \left(0..^{M}\right)\to \left(\left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}\right)=\left({N}+{M}-{n}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}\right)\right){B}\right)\to \left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({n}+1\right)=\left({N}+{M}-\left({n}+1\right)\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({n}+1\right)\right){B}\right)\right)$
140 19 28 37 46 72 139 fzind2 ${⊢}{M}\in \left(0\dots {M}\right)\to \left({\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)=\left({N}+{M}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}\right)$
141 10 140 mpcom ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)=\left({N}+{M}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}$
142 66 subidd ${⊢}{\phi }\to {M}-{M}=0$
143 142 oveq2d ${⊢}{\phi }\to {N}+{M}-{M}={N}+0$
144 106 addid1d ${⊢}{\phi }\to {N}+0={N}$
145 143 144 eqtrd ${⊢}{\phi }\to {N}+{M}-{M}={N}$
146 145 oveq1d ${⊢}{\phi }\to \left({N}+{M}-{M}\right)\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}={N}\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}$
147 141 146 eqtrd ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left({N}+{M}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({M}\right)={N}\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({M}\right)\right){B}$