# Metamath Proof Explorer

## Theorem dvtaylp

Description: The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016)

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

### Proof

Step Hyp Ref Expression
1 dvtaylp.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 dvtaylp.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
3 dvtaylp.a ${⊢}{\phi }\to {A}\subseteq {S}$
4 dvtaylp.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
5 dvtaylp.b ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+1\right)$
6 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
7 6 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
8 7 toponrestid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ$
9 cnelprrecn ${⊢}ℂ\in \left\{ℝ,ℂ\right\}$
10 9 a1i ${⊢}{\phi }\to ℂ\in \left\{ℝ,ℂ\right\}$
11 toponmax ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
12 7 11 mp1i ${⊢}{\phi }\to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
13 fzfid ${⊢}{\phi }\to \left(0\dots {N}+1\right)\in \mathrm{Fin}$
14 cnex ${⊢}ℂ\in \mathrm{V}$
15 14 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
16 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)$
17 15 1 2 3 16 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
18 elfznn0 ${⊢}{k}\in \left(0\dots {N}+1\right)\to {k}\in {ℕ}_{0}$
19 dvnf ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟶ℂ$
20 1 17 18 19 syl2an3an ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)⟶ℂ$
21 0z ${⊢}0\in ℤ$
22 peano2nn0 ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in {ℕ}_{0}$
23 4 22 syl ${⊢}{\phi }\to {N}+1\in {ℕ}_{0}$
24 23 nn0zd ${⊢}{\phi }\to {N}+1\in ℤ$
25 fzval2 ${⊢}\left(0\in ℤ\wedge {N}+1\in ℤ\right)\to \left(0\dots {N}+1\right)=\left[0,{N}+1\right]\cap ℤ$
26 21 24 25 sylancr ${⊢}{\phi }\to \left(0\dots {N}+1\right)=\left[0,{N}+1\right]\cap ℤ$
27 26 eleq2d ${⊢}{\phi }\to \left({k}\in \left(0\dots {N}+1\right)↔{k}\in \left(\left[0,{N}+1\right]\cap ℤ\right)\right)$
28 27 biimpa ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {k}\in \left(\left[0,{N}+1\right]\cap ℤ\right)$
29 1 2 3 23 5 taylplem1 ${⊢}\left({\phi }\wedge {k}\in \left(\left[0,{N}+1\right]\cap ℤ\right)\right)\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
30 28 29 syldan ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({k}\right)$
31 20 30 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)\in ℂ$
32 18 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {k}\in {ℕ}_{0}$
33 32 faccld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {k}!\in ℕ$
34 33 nncnd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {k}!\in ℂ$
35 33 nnne0d ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {k}!\ne 0$
36 31 34 35 divcld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in ℂ$
37 36 3adant3 ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in ℂ$
38 simp3 ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to {x}\in ℂ$
39 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
40 1 39 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
41 3 40 sstrd ${⊢}{\phi }\to {A}\subseteq ℂ$
42 dvnbss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}+1\in {ℕ}_{0}\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+1\right)\subseteq \mathrm{dom}{F}$
43 1 17 23 42 syl3anc ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+1\right)\subseteq \mathrm{dom}{F}$
44 2 43 fssdmd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+1\right)\subseteq {A}$
45 44 5 sseldd ${⊢}{\phi }\to {B}\in {A}$
46 41 45 sseldd ${⊢}{\phi }\to {B}\in ℂ$
47 46 3ad2ant1 ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to {B}\in ℂ$
48 38 47 subcld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to {x}-{B}\in ℂ$
49 18 3ad2ant2 ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to {k}\in {ℕ}_{0}$
50 48 49 expcld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to {\left({x}-{B}\right)}^{{k}}\in ℂ$
51 37 50 mulcld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\in ℂ$
52 0cnd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge {k}=0\right)\to 0\in ℂ$
53 49 nn0cnd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to {k}\in ℂ$
54 53 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to {k}\in ℂ$
55 48 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to {x}-{B}\in ℂ$
56 49 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to {k}\in {ℕ}_{0}$
57 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to ¬{k}=0$
58 57 neqned ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to {k}\ne 0$
59 elnnne0 ${⊢}{k}\in ℕ↔\left({k}\in {ℕ}_{0}\wedge {k}\ne 0\right)$
60 56 58 59 sylanbrc ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to {k}\in ℕ$
61 nnm1nn0 ${⊢}{k}\in ℕ\to {k}-1\in {ℕ}_{0}$
62 60 61 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to {k}-1\in {ℕ}_{0}$
63 55 62 expcld ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to {\left({x}-{B}\right)}^{{k}-1}\in ℂ$
64 54 63 mulcld ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\wedge ¬{k}=0\right)\to {k}{\left({x}-{B}\right)}^{{k}-1}\in ℂ$
65 52 64 ifclda ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\in ℂ$
66 37 65 mulcld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\wedge {x}\in ℂ\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\in ℂ$
67 9 a1i ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to ℂ\in \left\{ℝ,ℂ\right\}$
68 50 3expa ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {x}\in ℂ\right)\to {\left({x}-{B}\right)}^{{k}}\in ℂ$
69 65 3expa ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {x}\in ℂ\right)\to if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\in ℂ$
70 48 3expa ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {x}\in ℂ\right)\to {x}-{B}\in ℂ$
71 1cnd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {x}\in ℂ\right)\to 1\in ℂ$
72 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {y}\in ℂ\right)\to {y}\in ℂ$
73 32 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {y}\in ℂ\right)\to {k}\in {ℕ}_{0}$
74 72 73 expcld ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {y}\in ℂ\right)\to {{y}}^{{k}}\in ℂ$
75 c0ex ${⊢}0\in \mathrm{V}$
76 ovex ${⊢}{k}{{y}}^{{k}-1}\in \mathrm{V}$
77 75 76 ifex ${⊢}if\left({k}=0,0,{k}{{y}}^{{k}-1}\right)\in \mathrm{V}$
78 77 a1i ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {y}\in ℂ\right)\to if\left({k}=0,0,{k}{{y}}^{{k}-1}\right)\in \mathrm{V}$
79 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {x}\in ℂ\right)\to {x}\in ℂ$
80 67 dvmptid ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{d\left({x}\in ℂ⟼{x}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼1\right)$
81 46 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {x}\in ℂ\right)\to {B}\in ℂ$
82 0cnd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {x}\in ℂ\right)\to 0\in ℂ$
83 46 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {B}\in ℂ$
84 67 83 dvmptc ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{d\left({x}\in ℂ⟼{B}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼0\right)$
85 67 79 71 80 81 82 84 dvmptsub ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{d\left({x}\in ℂ⟼{x}-{B}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼1-0\right)$
86 1m0e1 ${⊢}1-0=1$
87 86 mpteq2i ${⊢}\left({x}\in ℂ⟼1-0\right)=\left({x}\in ℂ⟼1\right)$
88 85 87 eqtrdi ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{d\left({x}\in ℂ⟼{x}-{B}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼1\right)$
89 dvexp2 ${⊢}{k}\in {ℕ}_{0}\to \frac{d\left({y}\in ℂ⟼{{y}}^{{k}}\right)}{{d}_{ℂ}{y}}=\left({y}\in ℂ⟼if\left({k}=0,0,{k}{{y}}^{{k}-1}\right)\right)$
90 32 89 syl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{d\left({y}\in ℂ⟼{{y}}^{{k}}\right)}{{d}_{ℂ}{y}}=\left({y}\in ℂ⟼if\left({k}=0,0,{k}{{y}}^{{k}-1}\right)\right)$
91 oveq1 ${⊢}{y}={x}-{B}\to {{y}}^{{k}}={\left({x}-{B}\right)}^{{k}}$
92 oveq1 ${⊢}{y}={x}-{B}\to {{y}}^{{k}-1}={\left({x}-{B}\right)}^{{k}-1}$
93 92 oveq2d ${⊢}{y}={x}-{B}\to {k}{{y}}^{{k}-1}={k}{\left({x}-{B}\right)}^{{k}-1}$
94 93 ifeq2d ${⊢}{y}={x}-{B}\to if\left({k}=0,0,{k}{{y}}^{{k}-1}\right)=if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)$
95 67 67 70 71 74 78 88 90 91 94 dvmptco ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{d\left({x}\in ℂ⟼{\left({x}-{B}\right)}^{{k}}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\cdot 1\right)$
96 69 mulid1d ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\wedge {x}\in ℂ\right)\to if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\cdot 1=if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)$
97 96 mpteq2dva ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \left({x}\in ℂ⟼if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\cdot 1\right)=\left({x}\in ℂ⟼if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\right)$
98 95 97 eqtrd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{d\left({x}\in ℂ⟼{\left({x}-{B}\right)}^{{k}}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\right)$
99 67 68 69 98 36 dvmptcmul ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{d\left({x}\in ℂ⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\right)$
100 8 6 10 12 13 51 66 99 dvmptfsum ${⊢}{\phi }\to \frac{d\left({x}\in ℂ⟼\sum _{{k}=0}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼\sum _{{k}=0}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\right)$
101 1zzd ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to 1\in ℤ$
102 0zd ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to 0\in ℤ$
103 4 nn0zd ${⊢}{\phi }\to {N}\in ℤ$
104 103 adantr ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {N}\in ℤ$
105 dvfg ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
106 1 105 syl ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
107 40 2 3 dvbss ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {A}$
108 107 3 sstrd ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {S}$
109 1nn0 ${⊢}1\in {ℕ}_{0}$
110 109 a1i ${⊢}{\phi }\to 1\in {ℕ}_{0}$
111 dvnadd ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge \left(1\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left(1\right)\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left(1+{N}\right)$
112 1 17 110 4 111 syl22anc ${⊢}{\phi }\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left(1\right)\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left(1+{N}\right)$
113 dvn1 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}{F}\right)\left(1\right)={S}\mathrm{D}{F}$
114 40 17 113 syl2anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left(1\right)={S}\mathrm{D}{F}$
115 114 oveq2d ${⊢}{\phi }\to {S}{D}^{n}\left({S}{D}^{n}{F}\right)\left(1\right)={S}{D}^{n}{{F}}_{{S}}^{\prime }$
116 115 fveq1d ${⊢}{\phi }\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left(1\right)\right)\left({N}\right)=\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({N}\right)$
117 1cnd ${⊢}{\phi }\to 1\in ℂ$
118 4 nn0cnd ${⊢}{\phi }\to {N}\in ℂ$
119 117 118 addcomd ${⊢}{\phi }\to 1+{N}={N}+1$
120 119 fveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left(1+{N}\right)=\left({S}{D}^{n}{F}\right)\left({N}+1\right)$
121 112 116 120 3eqtr3d ${⊢}{\phi }\to \left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({N}\right)=\left({S}{D}^{n}{F}\right)\left({N}+1\right)$
122 121 dmeqd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({N}\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}+1\right)$
123 5 122 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({N}\right)$
124 1 106 108 4 123 taylplem2 ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {j}\in \left(0\dots {N}\right)\right)\to \left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)}{{j}!}\right){\left({x}-{B}\right)}^{{j}}\in ℂ$
125 fveq2 ${⊢}{j}={k}-1\to \left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)=\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)$
126 125 fveq1d ${⊢}{j}={k}-1\to \left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)=\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)$
127 fveq2 ${⊢}{j}={k}-1\to {j}!=\left({k}-1\right)!$
128 126 127 oveq12d ${⊢}{j}={k}-1\to \frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)}{{j}!}=\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}$
129 oveq2 ${⊢}{j}={k}-1\to {\left({x}-{B}\right)}^{{j}}={\left({x}-{B}\right)}^{{k}-1}$
130 128 129 oveq12d ${⊢}{j}={k}-1\to \left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)}{{j}!}\right){\left({x}-{B}\right)}^{{j}}=\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}\right){\left({x}-{B}\right)}^{{k}-1}$
131 101 102 104 124 130 fsumshft ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \sum _{{j}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)}{{j}!}\right){\left({x}-{B}\right)}^{{j}}=\sum _{{k}=0+1}^{{N}+1}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}\right){\left({x}-{B}\right)}^{{k}-1}$
132 elfznn ${⊢}{k}\in \left(1\dots {N}+1\right)\to {k}\in ℕ$
133 132 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {k}\in ℕ$
134 133 nnne0d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {k}\ne 0$
135 ifnefalse ${⊢}{k}\ne 0\to if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)={k}{\left({x}-{B}\right)}^{{k}-1}$
136 134 135 syl ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)={k}{\left({x}-{B}\right)}^{{k}-1}$
137 136 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){k}{\left({x}-{B}\right)}^{{k}-1}$
138 simpll ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {\phi }$
139 fz1ssfz0 ${⊢}\left(1\dots {N}+1\right)\subseteq \left(0\dots {N}+1\right)$
140 139 sseli ${⊢}{k}\in \left(1\dots {N}+1\right)\to {k}\in \left(0\dots {N}+1\right)$
141 140 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {k}\in \left(0\dots {N}+1\right)$
142 138 141 36 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in ℂ$
143 133 nncnd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {k}\in ℂ$
144 simplr ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {x}\in ℂ$
145 46 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {B}\in ℂ$
146 144 145 subcld ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {x}-{B}\in ℂ$
147 133 61 syl ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {k}-1\in {ℕ}_{0}$
148 146 147 expcld ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {\left({x}-{B}\right)}^{{k}-1}\in ℂ$
149 142 143 148 mulassd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){k}{\left({x}-{B}\right)}^{{k}-1}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){k}{\left({x}-{B}\right)}^{{k}-1}$
150 facp1 ${⊢}{k}-1\in {ℕ}_{0}\to \left({k}-1+1\right)!=\left({k}-1\right)!\left({k}-1+1\right)$
151 147 150 syl ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({k}-1+1\right)!=\left({k}-1\right)!\left({k}-1+1\right)$
152 1cnd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to 1\in ℂ$
153 143 152 npcand ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {k}-1+1={k}$
154 153 fveq2d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({k}-1+1\right)!={k}!$
155 153 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({k}-1\right)!\left({k}-1+1\right)=\left({k}-1\right)!{k}$
156 151 154 155 3eqtr3d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {k}!=\left({k}-1\right)!{k}$
157 156 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right){k}}{{k}!}=\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right){k}}{\left({k}-1\right)!{k}}$
158 32 nn0cnd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to {k}\in ℂ$
159 31 158 34 35 div23d ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right){k}}{{k}!}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){k}$
160 138 141 159 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right){k}}{{k}!}=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){k}$
161 138 141 31 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)\in ℂ$
162 147 faccld ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({k}-1\right)!\in ℕ$
163 162 nncnd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({k}-1\right)!\in ℂ$
164 162 nnne0d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({k}-1\right)!\ne 0$
165 161 163 143 164 134 divcan5rd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right){k}}{\left({k}-1\right)!{k}}=\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{\left({k}-1\right)!}$
166 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
167 17 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
168 109 a1i ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to 1\in {ℕ}_{0}$
169 dvnadd ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\wedge \left(1\in {ℕ}_{0}\wedge {k}-1\in {ℕ}_{0}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left(1\right)\right)\left({k}-1\right)=\left({S}{D}^{n}{F}\right)\left(1+{k}-1\right)$
170 166 167 168 147 169 syl22anc ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left(1\right)\right)\left({k}-1\right)=\left({S}{D}^{n}{F}\right)\left(1+{k}-1\right)$
171 114 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({S}{D}^{n}{F}\right)\left(1\right)={S}\mathrm{D}{F}$
172 171 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to {S}{D}^{n}\left({S}{D}^{n}{F}\right)\left(1\right)={S}{D}^{n}{{F}}_{{S}}^{\prime }$
173 172 fveq1d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left(1\right)\right)\left({k}-1\right)=\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)$
174 152 143 pncan3d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to 1+{k}-1={k}$
175 174 fveq2d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({S}{D}^{n}{F}\right)\left(1+{k}-1\right)=\left({S}{D}^{n}{F}\right)\left({k}\right)$
176 170 173 175 3eqtr3rd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right)=\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)$
177 176 fveq1d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)=\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)$
178 177 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{\left({k}-1\right)!}=\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}$
179 165 178 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right){k}}{\left({k}-1\right)!{k}}=\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}$
180 157 160 179 3eqtr3d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){k}=\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}$
181 180 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){k}{\left({x}-{B}\right)}^{{k}-1}=\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}\right){\left({x}-{B}\right)}^{{k}-1}$
182 137 149 181 3eqtr2d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}\right){\left({x}-{B}\right)}^{{k}-1}$
183 182 sumeq2dv ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \sum _{{k}=1}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=\sum _{{k}=1}^{{N}+1}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}\right){\left({x}-{B}\right)}^{{k}-1}$
184 0p1e1 ${⊢}0+1=1$
185 184 oveq1i ${⊢}\left(0+1\dots {N}+1\right)=\left(1\dots {N}+1\right)$
186 185 sumeq1i ${⊢}\sum _{{k}=0+1}^{{N}+1}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}\right){\left({x}-{B}\right)}^{{k}-1}=\sum _{{k}=1}^{{N}+1}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}\right){\left({x}-{B}\right)}^{{k}-1}$
187 183 186 eqtr4di ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \sum _{{k}=1}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=\sum _{{k}=0+1}^{{N}+1}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({k}-1\right)\left({B}\right)}{\left({k}-1\right)!}\right){\left({x}-{B}\right)}^{{k}-1}$
188 139 a1i ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left(1\dots {N}+1\right)\subseteq \left(0\dots {N}+1\right)$
189 69 an32s ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(0\dots {N}+1\right)\right)\to if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\in ℂ$
190 140 189 sylan2 ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\in ℂ$
191 142 190 mulcld ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(1\dots {N}+1\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\in ℂ$
192 eldif ${⊢}{k}\in \left(\left(0\dots {N}+1\right)\setminus \left(1\dots {N}+1\right)\right)↔\left({k}\in \left(0\dots {N}+1\right)\wedge ¬{k}\in \left(1\dots {N}+1\right)\right)$
193 59 biimpri ${⊢}\left({k}\in {ℕ}_{0}\wedge {k}\ne 0\right)\to {k}\in ℕ$
194 18 193 sylan ${⊢}\left({k}\in \left(0\dots {N}+1\right)\wedge {k}\ne 0\right)\to {k}\in ℕ$
195 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
196 194 195 eleqtrdi ${⊢}\left({k}\in \left(0\dots {N}+1\right)\wedge {k}\ne 0\right)\to {k}\in {ℤ}_{\ge 1}$
197 elfzuz3 ${⊢}{k}\in \left(0\dots {N}+1\right)\to {N}+1\in {ℤ}_{\ge {k}}$
198 197 adantr ${⊢}\left({k}\in \left(0\dots {N}+1\right)\wedge {k}\ne 0\right)\to {N}+1\in {ℤ}_{\ge {k}}$
199 elfzuzb ${⊢}{k}\in \left(1\dots {N}+1\right)↔\left({k}\in {ℤ}_{\ge 1}\wedge {N}+1\in {ℤ}_{\ge {k}}\right)$
200 196 198 199 sylanbrc ${⊢}\left({k}\in \left(0\dots {N}+1\right)\wedge {k}\ne 0\right)\to {k}\in \left(1\dots {N}+1\right)$
201 200 ex ${⊢}{k}\in \left(0\dots {N}+1\right)\to \left({k}\ne 0\to {k}\in \left(1\dots {N}+1\right)\right)$
202 201 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \left({k}\ne 0\to {k}\in \left(1\dots {N}+1\right)\right)$
203 202 necon1bd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \left(¬{k}\in \left(1\dots {N}+1\right)\to {k}=0\right)$
204 203 impr ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge \left({k}\in \left(0\dots {N}+1\right)\wedge ¬{k}\in \left(1\dots {N}+1\right)\right)\right)\to {k}=0$
205 192 204 sylan2b ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(\left(0\dots {N}+1\right)\setminus \left(1\dots {N}+1\right)\right)\right)\to {k}=0$
206 205 iftrued ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(\left(0\dots {N}+1\right)\setminus \left(1\dots {N}+1\right)\right)\right)\to if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=0$
207 206 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(\left(0\dots {N}+1\right)\setminus \left(1\dots {N}+1\right)\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)\cdot 0$
208 eldifi ${⊢}{k}\in \left(\left(0\dots {N}+1\right)\setminus \left(1\dots {N}+1\right)\right)\to {k}\in \left(0\dots {N}+1\right)$
209 36 adantlr ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(0\dots {N}+1\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in ℂ$
210 208 209 sylan2 ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(\left(0\dots {N}+1\right)\setminus \left(1\dots {N}+1\right)\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\in ℂ$
211 210 mul01d ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(\left(0\dots {N}+1\right)\setminus \left(1\dots {N}+1\right)\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)\cdot 0=0$
212 207 211 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in ℂ\right)\wedge {k}\in \left(\left(0\dots {N}+1\right)\setminus \left(1\dots {N}+1\right)\right)\right)\to \left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=0$
213 fzfid ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left(0\dots {N}+1\right)\in \mathrm{Fin}$
214 188 191 212 213 fsumss ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \sum _{{k}=1}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=\sum _{{k}=0}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)$
215 131 187 214 3eqtr2rd ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \sum _{{k}=0}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)=\sum _{{j}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)}{{j}!}\right){\left({x}-{B}\right)}^{{j}}$
216 215 mpteq2dva ${⊢}{\phi }\to \left({x}\in ℂ⟼\sum _{{k}=0}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right)if\left({k}=0,0,{k}{\left({x}-{B}\right)}^{{k}-1}\right)\right)=\left({x}\in ℂ⟼\sum _{{j}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)}{{j}!}\right){\left({x}-{B}\right)}^{{j}}\right)$
217 100 216 eqtrd ${⊢}{\phi }\to \frac{d\left({x}\in ℂ⟼\sum _{{k}=0}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼\sum _{{j}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)}{{j}!}\right){\left({x}-{B}\right)}^{{j}}\right)$
218 eqid ${⊢}\left({N}+1\right)\left({S}\mathrm{Tayl}{F}\right){B}=\left({N}+1\right)\left({S}\mathrm{Tayl}{F}\right){B}$
219 1 2 3 23 5 218 taylpfval ${⊢}{\phi }\to \left({N}+1\right)\left({S}\mathrm{Tayl}{F}\right){B}=\left({x}\in ℂ⟼\sum _{{k}=0}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)$
220 219 oveq2d ${⊢}{\phi }\to ℂ\mathrm{D}\left(\left({N}+1\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)=\frac{d\left({x}\in ℂ⟼\sum _{{k}=0}^{{N}+1}\left(\frac{\left({S}{D}^{n}{F}\right)\left({k}\right)\left({B}\right)}{{k}!}\right){\left({x}-{B}\right)}^{{k}}\right)}{{d}_{ℂ}{x}}$
221 eqid ${⊢}{N}\left({S}\mathrm{Tayl}{{F}}_{{S}}^{\prime }\right){B}={N}\left({S}\mathrm{Tayl}{{F}}_{{S}}^{\prime }\right){B}$
222 1 106 108 4 123 221 taylpfval ${⊢}{\phi }\to {N}\left({S}\mathrm{Tayl}{{F}}_{{S}}^{\prime }\right){B}=\left({x}\in ℂ⟼\sum _{{j}=0}^{{N}}\left(\frac{\left({S}{D}^{n}{{F}}_{{S}}^{\prime }\right)\left({j}\right)\left({B}\right)}{{j}!}\right){\left({x}-{B}\right)}^{{j}}\right)$
223 217 220 222 3eqtr4d ${⊢}{\phi }\to ℂ\mathrm{D}\left(\left({N}+1\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)={N}\left({S}\mathrm{Tayl}{{F}}_{{S}}^{\prime }\right){B}$