# Metamath Proof Explorer

## Theorem taylthlem1

Description: Lemma for taylth . This is the main part of Taylor's theorem, except for the induction step, which is supposed to be proven using L'Hôpital's rule. However, since our proof of L'Hôpital assumes that S = RR , we can only do this part generically, and for taylth itself we must restrict to RR . (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses taylthlem1.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
taylthlem1.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
taylthlem1.a ${⊢}{\phi }\to {A}\subseteq {S}$
taylthlem1.d ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)={A}$
taylthlem1.n ${⊢}{\phi }\to {N}\in ℕ$
taylthlem1.b ${⊢}{\phi }\to {B}\in {A}$
taylthlem1.t ${⊢}{T}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
taylthlem1.r ${⊢}{R}=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{{F}\left({x}\right)-{T}\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right)$
taylthlem1.i ${⊢}\left({\phi }\wedge \left({n}\in \left(1..^{N}\right)\wedge 0\in \left(\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right){lim}_{ℂ}{B}\right)\right)\right)\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right){lim}_{ℂ}{B}\right)$
Assertion taylthlem1 ${⊢}{\phi }\to 0\in \left({R}{lim}_{ℂ}{B}\right)$

### Proof

Step Hyp Ref Expression
1 taylthlem1.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 taylthlem1.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
3 taylthlem1.a ${⊢}{\phi }\to {A}\subseteq {S}$
4 taylthlem1.d ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)={A}$
5 taylthlem1.n ${⊢}{\phi }\to {N}\in ℕ$
6 taylthlem1.b ${⊢}{\phi }\to {B}\in {A}$
7 taylthlem1.t ${⊢}{T}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
8 taylthlem1.r ${⊢}{R}=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{{F}\left({x}\right)-{T}\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right)$
9 taylthlem1.i ${⊢}\left({\phi }\wedge \left({n}\in \left(1..^{N}\right)\wedge 0\in \left(\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right){lim}_{ℂ}{B}\right)\right)\right)\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right){lim}_{ℂ}{B}\right)$
10 elfz1end ${⊢}{N}\in ℕ↔{N}\in \left(1\dots {N}\right)$
11 5 10 sylib ${⊢}{\phi }\to {N}\in \left(1\dots {N}\right)$
12 oveq2 ${⊢}{m}=1\to {N}-{m}={N}-1$
13 12 fveq2d ${⊢}{m}=1\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
14 13 fveq1d ${⊢}{m}=1\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)$
15 12 fveq2d ${⊢}{m}=1\to \left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)$
16 15 fveq1d ${⊢}{m}=1\to \left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)$
17 14 16 oveq12d ${⊢}{m}=1\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)$
18 oveq2 ${⊢}{m}=1\to {\left({x}-{B}\right)}^{{m}}={\left({x}-{B}\right)}^{1}$
19 17 18 oveq12d ${⊢}{m}=1\to \frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}=\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}$
20 19 mpteq2dv ${⊢}{m}=1\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right)=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}\right)$
21 20 oveq1d ${⊢}{m}=1\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}\right){lim}_{ℂ}{B}$
22 21 eleq2d ${⊢}{m}=1\to \left(0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}\right)↔0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}\right){lim}_{ℂ}{B}\right)\right)$
23 22 imbi2d ${⊢}{m}=1\to \left(\left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}\right)\right)↔\left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}\right){lim}_{ℂ}{B}\right)\right)\right)$
24 oveq2 ${⊢}{m}={n}\to {N}-{m}={N}-{n}$
25 24 fveq2d ${⊢}{m}={n}\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)=\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)$
26 25 fveq1d ${⊢}{m}={n}\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({x}\right)$
27 24 fveq2d ${⊢}{m}={n}\to \left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)$
28 27 fveq1d ${⊢}{m}={n}\to \left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({x}\right)$
29 26 28 oveq12d ${⊢}{m}={n}\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({x}\right)$
30 oveq2 ${⊢}{m}={n}\to {\left({x}-{B}\right)}^{{m}}={\left({x}-{B}\right)}^{{n}}$
31 29 30 oveq12d ${⊢}{m}={n}\to \frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}=\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}}}$
32 31 mpteq2dv ${⊢}{m}={n}\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right)=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}}}\right)$
33 fveq2 ${⊢}{x}={y}\to \left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)$
34 fveq2 ${⊢}{x}={y}\to \left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({x}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)$
35 33 34 oveq12d ${⊢}{x}={y}\to \left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)$
36 oveq1 ${⊢}{x}={y}\to {x}-{B}={y}-{B}$
37 36 oveq1d ${⊢}{x}={y}\to {\left({x}-{B}\right)}^{{n}}={\left({y}-{B}\right)}^{{n}}$
38 35 37 oveq12d ${⊢}{x}={y}\to \frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}}}=\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}$
39 38 cbvmptv ${⊢}\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}}}\right)=\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right)$
40 32 39 syl6eq ${⊢}{m}={n}\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right)=\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right)$
41 40 oveq1d ${⊢}{m}={n}\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}=\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right){lim}_{ℂ}{B}$
42 41 eleq2d ${⊢}{m}={n}\to \left(0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}\right)↔0\in \left(\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right){lim}_{ℂ}{B}\right)\right)$
43 42 imbi2d ${⊢}{m}={n}\to \left(\left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}\right)\right)↔\left({\phi }\to 0\in \left(\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right){lim}_{ℂ}{B}\right)\right)\right)$
44 oveq2 ${⊢}{m}={n}+1\to {N}-{m}={N}-\left({n}+1\right)$
45 44 fveq2d ${⊢}{m}={n}+1\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)=\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)$
46 45 fveq1d ${⊢}{m}={n}+1\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)$
47 44 fveq2d ${⊢}{m}={n}+1\to \left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)$
48 47 fveq1d ${⊢}{m}={n}+1\to \left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)$
49 46 48 oveq12d ${⊢}{m}={n}+1\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)$
50 oveq2 ${⊢}{m}={n}+1\to {\left({x}-{B}\right)}^{{m}}={\left({x}-{B}\right)}^{{n}+1}$
51 49 50 oveq12d ${⊢}{m}={n}+1\to \frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}=\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}$
52 51 mpteq2dv ${⊢}{m}={n}+1\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right)=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right)$
53 52 oveq1d ${⊢}{m}={n}+1\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right){lim}_{ℂ}{B}$
54 53 eleq2d ${⊢}{m}={n}+1\to \left(0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}\right)↔0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right){lim}_{ℂ}{B}\right)\right)$
55 54 imbi2d ${⊢}{m}={n}+1\to \left(\left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}\right)\right)↔\left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right){lim}_{ℂ}{B}\right)\right)\right)$
56 oveq2 ${⊢}{m}={N}\to {N}-{m}={N}-{N}$
57 56 fveq2d ${⊢}{m}={N}\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)=\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)$
58 57 fveq1d ${⊢}{m}={N}\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)$
59 56 fveq2d ${⊢}{m}={N}\to \left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)$
60 59 fveq1d ${⊢}{m}={N}\to \left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)$
61 58 60 oveq12d ${⊢}{m}={N}\to \left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)$
62 oveq2 ${⊢}{m}={N}\to {\left({x}-{B}\right)}^{{m}}={\left({x}-{B}\right)}^{{N}}$
63 61 62 oveq12d ${⊢}{m}={N}\to \frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}=\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}$
64 63 mpteq2dv ${⊢}{m}={N}\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right)=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right)$
65 64 oveq1d ${⊢}{m}={N}\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right){lim}_{ℂ}{B}$
66 65 eleq2d ${⊢}{m}={N}\to \left(0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}\right)↔0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right){lim}_{ℂ}{B}\right)\right)$
67 66 imbi2d ${⊢}{m}={N}\to \left(\left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{m}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{m}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{m}}}\right){lim}_{ℂ}{B}\right)\right)↔\left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right){lim}_{ℂ}{B}\right)\right)\right)$
68 fveq2 ${⊢}{y}={B}\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)$
69 fveq2 ${⊢}{y}={B}\to \left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({B}\right)$
70 68 69 oveq12d ${⊢}{y}={B}\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({B}\right)$
71 eqid ${⊢}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)=\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)$
72 ovex ${⊢}\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({B}\right)\in \mathrm{V}$
73 70 71 72 fvmpt ${⊢}{B}\in {A}\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({B}\right)$
74 6 73 syl ${⊢}{\phi }\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({B}\right)$
75 5 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
76 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
77 75 76 eleqtrdi ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 0}$
78 eluzfz2b ${⊢}{N}\in {ℤ}_{\ge 0}↔{N}\in \left(0\dots {N}\right)$
79 77 78 sylib ${⊢}{\phi }\to {N}\in \left(0\dots {N}\right)$
80 6 4 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
81 1 2 3 79 80 7 dvntaylp0 ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)$
82 81 oveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)-\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)$
83 cnex ${⊢}ℂ\in \mathrm{V}$
84 83 a1i ${⊢}{\phi }\to ℂ\in \mathrm{V}$
85 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)$
86 84 1 2 3 85 syl22anc ${⊢}{\phi }\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
87 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)⟶ℂ$
88 1 86 75 87 syl3anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)⟶ℂ$
89 88 80 ffvelrnd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)\in ℂ$
90 89 subidd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)-\left({S}{D}^{n}{F}\right)\left({N}\right)\left({B}\right)=0$
91 74 82 90 3eqtrd ${⊢}{\phi }\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)\left({B}\right)=0$
92 funmpt ${⊢}\mathrm{Fun}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)$
93 ovex ${⊢}\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\in \mathrm{V}$
94 93 71 dmmpti ${⊢}\mathrm{dom}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)={A}$
95 6 94 eleqtrrdi ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)$
96 funbrfvb ${⊢}\left(\mathrm{Fun}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)\wedge {B}\in \mathrm{dom}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)\right)\to \left(\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)\left({B}\right)=0↔{B}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)0\right)$
97 92 95 96 sylancr ${⊢}{\phi }\to \left(\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)\left({B}\right)=0↔{B}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)0\right)$
98 91 97 mpbid ${⊢}{\phi }\to {B}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)0$
99 nnm1nn0 ${⊢}{N}\in ℕ\to {N}-1\in {ℕ}_{0}$
100 5 99 syl ${⊢}{\phi }\to {N}-1\in {ℕ}_{0}$
101 dvnf ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}-1\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)⟶ℂ$
102 1 86 100 101 syl3anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)⟶ℂ$
103 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}$
104 1 86 100 103 syl3anc ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\subseteq \mathrm{dom}{F}$
105 2 104 fssdmd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\subseteq {A}$
106 fzo0end ${⊢}{N}\in ℕ\to {N}-1\in \left(0..^{N}\right)$
107 elfzofz ${⊢}{N}-1\in \left(0..^{N}\right)\to {N}-1\in \left(0\dots {N}\right)$
108 5 106 107 3syl ${⊢}{\phi }\to {N}-1\in \left(0\dots {N}\right)$
109 dvn2bss ${⊢}\left({S}\in \left\{ℝ,ℂ\right\}\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}-1\in \left(0\dots {N}\right)\right)\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
110 1 86 108 109 syl3anc ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)\subseteq \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
111 4 110 eqsstrrd ${⊢}{\phi }\to {A}\subseteq \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
112 105 111 eqssd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)={A}$
113 112 feq2d ${⊢}{\phi }\to \left(\left({S}{D}^{n}{F}\right)\left({N}-1\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}-1\right)⟶ℂ↔\left({S}{D}^{n}{F}\right)\left({N}-1\right):{A}⟶ℂ\right)$
114 102 113 mpbid ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1\right):{A}⟶ℂ$
115 114 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)\in ℂ$
116 4 feq2d ${⊢}{\phi }\to \left(\left({S}{D}^{n}{F}\right)\left({N}\right):\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)⟶ℂ↔\left({S}{D}^{n}{F}\right)\left({N}\right):{A}⟶ℂ\right)$
117 88 116 mpbid ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right):{A}⟶ℂ$
118 117 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)\in ℂ$
119 5 nncnd ${⊢}{\phi }\to {N}\in ℂ$
120 1cnd ${⊢}{\phi }\to 1\in ℂ$
121 119 120 npcand ${⊢}{\phi }\to {N}-1+1={N}$
122 121 fveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1+1\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
123 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
124 1 123 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
125 dvnp1 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\wedge {N}-1\in {ℕ}_{0}\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
126 124 86 100 125 syl3anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1+1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
127 122 126 eqtr3d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
128 117 feqmptd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)=\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)\right)$
129 114 feqmptd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)=\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)\right)$
130 129 oveq2d ${⊢}{\phi }\to {S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}-1\right)=\frac{d\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{{S}}{y}}$
131 127 128 130 3eqtr3rd ${⊢}{\phi }\to \frac{d\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{{S}}{y}}=\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)\right)$
132 3 124 sstrd ${⊢}{\phi }\to {A}\subseteq ℂ$
133 132 sselda ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {y}\in ℂ$
134 1nn0 ${⊢}1\in {ℕ}_{0}$
135 134 a1i ${⊢}{\phi }\to 1\in {ℕ}_{0}$
136 elpm2r ${⊢}\left(\left(ℂ\in \mathrm{V}\wedge {S}\in \left\{ℝ,ℂ\right\}\right)\wedge \left(\left({S}{D}^{n}{F}\right)\left({N}-1\right):{A}⟶ℂ\wedge {A}\subseteq {S}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
137 84 1 114 3 136 syl22anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
138 dvn1 ${⊢}\left({S}\subseteq ℂ\wedge \left({S}{D}^{n}{F}\right)\left({N}-1\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right)\left(1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
139 124 137 138 syl2anc ${⊢}{\phi }\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right)\left(1\right)={S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}-1\right)$
140 126 122 eqtr3d ${⊢}{\phi }\to {S}\mathrm{D}\left({S}{D}^{n}{F}\right)\left({N}-1\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
141 139 140 eqtrd ${⊢}{\phi }\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right)\left(1\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
142 141 dmeqd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right)\left(1\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
143 80 142 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right)\left(1\right)$
144 eqid ${⊢}1\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right){B}=1\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right){B}$
145 1 114 3 135 143 144 taylpf ${⊢}{\phi }\to \left(1\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right){B}\right):ℂ⟶ℂ$
146 120 119 pncan3d ${⊢}{\phi }\to 1+{N}-1={N}$
147 146 oveq1d ${⊢}{\phi }\to \left(1+{N}-1\right)\left({S}\mathrm{Tayl}{F}\right){B}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
148 147 7 syl6reqr ${⊢}{\phi }\to {T}=\left(1+{N}-1\right)\left({S}\mathrm{Tayl}{F}\right){B}$
149 148 oveq2d ${⊢}{\phi }\to ℂ{D}^{n}{T}=ℂ{D}^{n}\left(\left(1+{N}-1\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)$
150 149 fveq1d ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)=\left(ℂ{D}^{n}\left(\left(1+{N}-1\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({N}-1\right)$
151 146 fveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left(1+{N}-1\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
152 151 dmeqd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left(1+{N}-1\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
153 80 152 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left(1+{N}-1\right)$
154 1 2 3 100 135 153 dvntaylp ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left(1+{N}-1\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({N}-1\right)=1\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right){B}$
155 150 154 eqtrd ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)=1\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right){B}$
156 155 feq1d ${⊢}{\phi }\to \left(\left(ℂ{D}^{n}{T}\right)\left({N}-1\right):ℂ⟶ℂ↔\left(1\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\right){B}\right):ℂ⟶ℂ\right)$
157 145 156 mpbird ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right):ℂ⟶ℂ$
158 157 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in ℂ\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\in ℂ$
159 133 158 syldan ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\in ℂ$
160 0nn0 ${⊢}0\in {ℕ}_{0}$
161 160 a1i ${⊢}{\phi }\to 0\in {ℕ}_{0}$
162 elpm2r ${⊢}\left(\left(ℂ\in \mathrm{V}\wedge {S}\in \left\{ℝ,ℂ\right\}\right)\wedge \left(\left({S}{D}^{n}{F}\right)\left({N}\right):{A}⟶ℂ\wedge {A}\subseteq {S}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({N}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
163 84 1 117 3 162 syl22anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
164 dvn0 ${⊢}\left({S}\subseteq ℂ\wedge \left({S}{D}^{n}{F}\right)\left({N}\right)\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}\right)\right)\left(0\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
165 124 163 164 syl2anc ${⊢}{\phi }\to \left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}\right)\right)\left(0\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
166 165 dmeqd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}\right)\right)\left(0\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
167 80 166 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}\left({S}{D}^{n}{F}\right)\left({N}\right)\right)\left(0\right)$
168 eqid ${⊢}0\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}\right)\right){B}=0\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}\right)\right){B}$
169 1 117 3 161 167 168 taylpf ${⊢}{\phi }\to \left(0\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}\right)\right){B}\right):ℂ⟶ℂ$
170 119 addid2d ${⊢}{\phi }\to 0+{N}={N}$
171 170 oveq1d ${⊢}{\phi }\to \left(0+{N}\right)\left({S}\mathrm{Tayl}{F}\right){B}={N}\left({S}\mathrm{Tayl}{F}\right){B}$
172 171 7 syl6eqr ${⊢}{\phi }\to \left(0+{N}\right)\left({S}\mathrm{Tayl}{F}\right){B}={T}$
173 172 oveq2d ${⊢}{\phi }\to ℂ{D}^{n}\left(\left(0+{N}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)=ℂ{D}^{n}{T}$
174 173 fveq1d ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left(0+{N}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({N}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}\right)$
175 170 fveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left(0+{N}\right)=\left({S}{D}^{n}{F}\right)\left({N}\right)$
176 175 dmeqd ${⊢}{\phi }\to \mathrm{dom}\left({S}{D}^{n}{F}\right)\left(0+{N}\right)=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
177 80 176 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{dom}\left({S}{D}^{n}{F}\right)\left(0+{N}\right)$
178 1 2 3 75 161 177 dvntaylp ${⊢}{\phi }\to \left(ℂ{D}^{n}\left(\left(0+{N}\right)\left({S}\mathrm{Tayl}{F}\right){B}\right)\right)\left({N}\right)=0\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}\right)\right){B}$
179 174 178 eqtr3d ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}\right)=0\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}\right)\right){B}$
180 179 feq1d ${⊢}{\phi }\to \left(\left(ℂ{D}^{n}{T}\right)\left({N}\right):ℂ⟶ℂ↔\left(0\left({S}\mathrm{Tayl}\left({S}{D}^{n}{F}\right)\left({N}\right)\right){B}\right):ℂ⟶ℂ\right)$
181 169 180 mpbird ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}\right):ℂ⟶ℂ$
182 181 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in ℂ\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\in ℂ$
183 133 182 syldan ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\in ℂ$
184 124 sselda ${⊢}\left({\phi }\wedge {y}\in {S}\right)\to {y}\in ℂ$
185 184 158 syldan ${⊢}\left({\phi }\wedge {y}\in {S}\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\in ℂ$
186 184 182 syldan ${⊢}\left({\phi }\wedge {y}\in {S}\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\in ℂ$
187 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
188 187 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
189 toponmax ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
190 188 189 mp1i ${⊢}{\phi }\to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
191 df-ss ${⊢}{S}\subseteq ℂ↔{S}\cap ℂ={S}$
192 124 191 sylib ${⊢}{\phi }\to {S}\cap ℂ={S}$
193 ssid ${⊢}ℂ\subseteq ℂ$
194 193 a1i ${⊢}{\phi }\to ℂ\subseteq ℂ$
195 mapsspm ${⊢}{ℂ}^{ℂ}\subseteq ℂ{↑}_{𝑝𝑚}ℂ$
196 1 2 3 75 80 7 taylpf ${⊢}{\phi }\to {T}:ℂ⟶ℂ$
197 83 83 elmap ${⊢}{T}\in \left({ℂ}^{ℂ}\right)↔{T}:ℂ⟶ℂ$
198 196 197 sylibr ${⊢}{\phi }\to {T}\in \left({ℂ}^{ℂ}\right)$
199 195 198 sseldi ${⊢}{\phi }\to {T}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)$
200 dvnp1 ${⊢}\left(ℂ\subseteq ℂ\wedge {T}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\wedge {N}-1\in {ℕ}_{0}\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}-1+1\right)=ℂ\mathrm{D}\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)$
201 194 199 100 200 syl3anc ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-1+1\right)=ℂ\mathrm{D}\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)$
202 121 fveq2d ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-1+1\right)=\left(ℂ{D}^{n}{T}\right)\left({N}\right)$
203 201 202 eqtr3d ${⊢}{\phi }\to ℂ\mathrm{D}\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)=\left(ℂ{D}^{n}{T}\right)\left({N}\right)$
204 157 feqmptd ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)=\left({y}\in ℂ⟼\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)$
205 204 oveq2d ${⊢}{\phi }\to ℂ\mathrm{D}\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)=\frac{d\left({y}\in ℂ⟼\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{ℂ}{y}}$
206 181 feqmptd ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}\right)=\left({y}\in ℂ⟼\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)$
207 203 205 206 3eqtr3d ${⊢}{\phi }\to \frac{d\left({y}\in ℂ⟼\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{ℂ}{y}}=\left({y}\in ℂ⟼\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)$
208 187 1 190 192 158 182 207 dvmptres3 ${⊢}{\phi }\to \frac{d\left({y}\in {S}⟼\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{{S}}{y}}=\left({y}\in {S}⟼\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)$
209 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}$
210 resttopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge {S}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
211 188 124 210 sylancr ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
212 topontop ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}$
213 211 212 syl ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}$
214 toponuni ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)\to {S}=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
215 211 214 syl ${⊢}{\phi }\to {S}=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
216 3 215 sseqtrd ${⊢}{\phi }\to {A}\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
217 eqid ${⊢}\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
218 217 ntrss2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}\wedge {A}\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\right)\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)\subseteq {A}$
219 213 216 218 syl2anc ${⊢}{\phi }\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)\subseteq {A}$
220 140 dmeqd ${⊢}{\phi }\to \mathrm{dom}{\left({S}{D}^{n}{F}\right)\left({N}-1\right)}_{{S}}^{\prime }=\mathrm{dom}\left({S}{D}^{n}{F}\right)\left({N}\right)$
221 220 4 eqtrd ${⊢}{\phi }\to \mathrm{dom}{\left({S}{D}^{n}{F}\right)\left({N}-1\right)}_{{S}}^{\prime }={A}$
222 124 114 3 209 187 dvbssntr ${⊢}{\phi }\to \mathrm{dom}{\left({S}{D}^{n}{F}\right)\left({N}-1\right)}_{{S}}^{\prime }\subseteq \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)$
223 221 222 eqsstrrd ${⊢}{\phi }\to {A}\subseteq \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)$
224 219 223 eqssd ${⊢}{\phi }\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)={A}$
225 1 185 186 208 3 209 187 224 dvmptres2 ${⊢}{\phi }\to \frac{d\left({y}\in {A}⟼\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{{S}}{y}}=\left({y}\in {A}⟼\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)$
226 1 115 118 131 159 183 225 dvmptsub ${⊢}{\phi }\to \frac{d\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{{S}}{y}}=\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)$
227 226 breqd ${⊢}{\phi }\to \left({B}\frac{d\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{{S}}{y}}0↔{B}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}\right)\left({y}\right)\right)0\right)$
228 98 227 mpbird ${⊢}{\phi }\to {B}\frac{d\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{{S}}{y}}0$
229 eqid ${⊢}\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)}{{x}-{B}}\right)=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)}{{x}-{B}}\right)$
230 115 159 subcld ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\in ℂ$
231 230 fmpttd ${⊢}{\phi }\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right):{A}⟶ℂ$
232 209 187 229 124 231 3 eldv ${⊢}{\phi }\to \left({B}\frac{d\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)}{{d}_{{S}}{y}}0↔\left({B}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)\wedge 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)}{{x}-{B}}\right){lim}_{ℂ}{B}\right)\right)\right)$
233 228 232 mpbid ${⊢}{\phi }\to \left({B}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)\wedge 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)}{{x}-{B}}\right){lim}_{ℂ}{B}\right)\right)$
234 233 simprd ${⊢}{\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)}{{x}-{B}}\right){lim}_{ℂ}{B}\right)$
235 eldifi ${⊢}{x}\in \left({A}\setminus \left\{{B}\right\}\right)\to {x}\in {A}$
236 fveq2 ${⊢}{y}={x}\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)$
237 fveq2 ${⊢}{y}={x}\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)$
238 236 237 oveq12d ${⊢}{y}={x}\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)$
239 eqid ${⊢}\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)=\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)$
240 ovex ${⊢}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)\in \mathrm{V}$
241 238 239 240 fvmpt ${⊢}{x}\in {A}\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)$
242 fveq2 ${⊢}{y}={B}\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)$
243 fveq2 ${⊢}{y}={B}\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)=\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({B}\right)$
244 242 243 oveq12d ${⊢}{y}={B}\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({B}\right)$
245 ovex ${⊢}\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({B}\right)\in \mathrm{V}$
246 244 239 245 fvmpt ${⊢}{B}\in {A}\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({B}\right)$
247 6 246 syl ${⊢}{\phi }\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({B}\right)$
248 1 2 3 108 80 7 dvntaylp0 ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)$
249 248 oveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)-\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)$
250 114 6 ffvelrnd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)\in ℂ$
251 250 subidd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)-\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({B}\right)=0$
252 247 249 251 3eqtrd ${⊢}{\phi }\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)=0$
253 241 252 oveqan12rd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)-0$
254 114 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)\in ℂ$
255 132 sselda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in ℂ$
256 157 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)\in ℂ$
257 255 256 syldan ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)\in ℂ$
258 254 257 subcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)\in ℂ$
259 258 subid1d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)-0=\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)$
260 253 259 eqtr2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)=\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)$
261 235 260 sylan2 ${⊢}\left({\phi }\wedge {x}\in \left({A}\setminus \left\{{B}\right\}\right)\right)\to \left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)=\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)$
262 132 ssdifssd ${⊢}{\phi }\to {A}\setminus \left\{{B}\right\}\subseteq ℂ$
263 262 sselda ${⊢}\left({\phi }\wedge {x}\in \left({A}\setminus \left\{{B}\right\}\right)\right)\to {x}\in ℂ$
264 132 6 sseldd ${⊢}{\phi }\to {B}\in ℂ$
265 264 adantr ${⊢}\left({\phi }\wedge {x}\in \left({A}\setminus \left\{{B}\right\}\right)\right)\to {B}\in ℂ$
266 263 265 subcld ${⊢}\left({\phi }\wedge {x}\in \left({A}\setminus \left\{{B}\right\}\right)\right)\to {x}-{B}\in ℂ$
267 266 exp1d ${⊢}\left({\phi }\wedge {x}\in \left({A}\setminus \left\{{B}\right\}\right)\right)\to {\left({x}-{B}\right)}^{1}={x}-{B}$
268 261 267 oveq12d ${⊢}\left({\phi }\wedge {x}\in \left({A}\setminus \left\{{B}\right\}\right)\right)\to \frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}=\frac{\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)}{{x}-{B}}$
269 268 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}\right)=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)}{{x}-{B}}\right)$
270 269 oveq1d ${⊢}{\phi }\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}\right){lim}_{ℂ}{B}=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({x}\right)-\left({y}\in {A}⟼\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({y}\right)\right)\left({B}\right)}{{x}-{B}}\right){lim}_{ℂ}{B}$
271 234 270 eleqtrrd ${⊢}{\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}\right){lim}_{ℂ}{B}\right)$
272 271 a1i ${⊢}{N}\in {ℤ}_{\ge 1}\to \left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-1\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-1\right)\left({x}\right)}{{\left({x}-{B}\right)}^{1}}\right){lim}_{ℂ}{B}\right)\right)$
273 9 expr ${⊢}\left({\phi }\wedge {n}\in \left(1..^{N}\right)\right)\to \left(0\in \left(\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right){lim}_{ℂ}{B}\right)\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right){lim}_{ℂ}{B}\right)\right)$
274 273 expcom ${⊢}{n}\in \left(1..^{N}\right)\to \left({\phi }\to \left(0\in \left(\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right){lim}_{ℂ}{B}\right)\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right){lim}_{ℂ}{B}\right)\right)\right)$
275 274 a2d ${⊢}{n}\in \left(1..^{N}\right)\to \left(\left({\phi }\to 0\in \left(\left({y}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{n}\right)\left({y}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{n}\right)\left({y}\right)}{{\left({y}-{B}\right)}^{{n}}}\right){lim}_{ℂ}{B}\right)\right)\to \left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-\left({n}+1\right)\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{n}+1}}\right){lim}_{ℂ}{B}\right)\right)\right)$
276 23 43 55 67 272 275 fzind2 ${⊢}{N}\in \left(1\dots {N}\right)\to \left({\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right){lim}_{ℂ}{B}\right)\right)$
277 11 276 mpcom ${⊢}{\phi }\to 0\in \left(\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right){lim}_{ℂ}{B}\right)$
278 119 subidd ${⊢}{\phi }\to {N}-{N}=0$
279 278 fveq2d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-{N}\right)=\left({S}{D}^{n}{F}\right)\left(0\right)$
280 dvn0 ${⊢}\left({S}\subseteq ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\to \left({S}{D}^{n}{F}\right)\left(0\right)={F}$
281 124 86 280 syl2anc ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left(0\right)={F}$
282 279 281 eqtrd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-{N}\right)={F}$
283 282 fveq1d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)={F}\left({x}\right)$
284 278 fveq2d ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)=\left(ℂ{D}^{n}{T}\right)\left(0\right)$
285 dvn0 ${⊢}\left(ℂ\subseteq ℂ\wedge {T}\in \left(ℂ{↑}_{𝑝𝑚}ℂ\right)\right)\to \left(ℂ{D}^{n}{T}\right)\left(0\right)={T}$
286 193 199 285 sylancr ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left(0\right)={T}$
287 284 286 eqtrd ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)={T}$
288 287 fveq1d ${⊢}{\phi }\to \left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)={T}\left({x}\right)$
289 283 288 oveq12d ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)={F}\left({x}\right)-{T}\left({x}\right)$
290 289 oveq1d ${⊢}{\phi }\to \frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}=\frac{{F}\left({x}\right)-{T}\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}$
291 290 mpteq2dv ${⊢}{\phi }\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right)=\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{{F}\left({x}\right)-{T}\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right)$
292 291 8 syl6eqr ${⊢}{\phi }\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right)={R}$
293 292 oveq1d ${⊢}{\phi }\to \left({x}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{\left({S}{D}^{n}{F}\right)\left({N}-{N}\right)\left({x}\right)-\left(ℂ{D}^{n}{T}\right)\left({N}-{N}\right)\left({x}\right)}{{\left({x}-{B}\right)}^{{N}}}\right){lim}_{ℂ}{B}={R}{lim}_{ℂ}{B}$
294 277 293 eleqtrd ${⊢}{\phi }\to 0\in \left({R}{lim}_{ℂ}{B}\right)$