# 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 ( 𝜑𝑆 ∈ { ℝ , ℂ } )
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 ffvelrnd ( 𝜑 → ( ( ( 𝑆 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 ffvelrnda ( ( 𝜑𝑦𝐴 ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 − 1 ) ) ‘ 𝑦 ) ∈ ℂ )
116 4 feq2d ( 𝜑 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⟶ ℂ ↔ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) : 𝐴 ⟶ ℂ ) )
117 88 116 mpbid ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) : 𝐴 ⟶ ℂ )
118 117 ffvelrnda ( ( 𝜑𝑦𝐴 ) → ( ( ( 𝑆 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 ffvelrnda ( ( 𝜑𝑦 ∈ ℂ ) → ( ( ( ℂ 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 addid2d ( 𝜑 → ( 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 ffvelrnda ( ( 𝜑𝑦 ∈ ℂ ) → ( ( ( ℂ 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 sseldi ( 𝜑𝑇 ∈ ( ℂ ↑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 ffvelrnd ( 𝜑 → ( ( ( 𝑆 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 ffvelrnda ( ( 𝜑𝑥𝐴 ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 − 1 ) ) ‘ 𝑥 ) ∈ ℂ )
255 132 sselda ( ( 𝜑𝑥𝐴 ) → 𝑥 ∈ ℂ )
256 157 ffvelrnda ( ( 𝜑𝑥 ∈ ℂ ) → ( ( ( ℂ 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 𝐵 ) )