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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	taylthlem1.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	taylthlem1.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	taylthlem1.d	⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = 𝐴 )
	taylthlem1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	taylthlem1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	taylthlem1.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
	taylthlem1.r	⊢ 𝑅 = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝑇 ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑁 ) ) )
	taylthlem1.i	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ..^ 𝑁 ) ∧ 0 ∈ ( ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 − 𝑛 ) ) ‘ 𝑦 ) − ( ( ( ℂ D𝑛 𝑇 ) ‘ ( 𝑁 − 𝑛 ) ) ‘ 𝑦 ) ) / ( ( 𝑦 − 𝐵 ) ↑ 𝑛 ) ) ) limℂ 𝐵 ) ) ) → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑛 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑛 + 1 ) ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ ( 𝑛 + 1 ) ) ) ) limℂ 𝐵 ) )
Assertion	taylthlem1	⊢ ( 𝜑 → 0 ∈ ( 𝑅 limℂ 𝐵 ) )

Proof

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