Metamath Proof Explorer

Theorem fourierdlem60

Description: Given a differentiable function F , with finite limit of the derivative at A the derived function H has a limit at 0 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem60.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem60.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem60.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem60.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
fourierdlem60.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐹 limℂ 𝐵 ) )
fourierdlem60.g ⊢ 𝐺 = ( ℝ D 𝐹 )
fourierdlem60.domg ⊢ ( 𝜑 → dom 𝐺 = ( 𝐴 (,) 𝐵 ) )
fourierdlem60.e ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐺 limℂ 𝐵 ) )
fourierdlem60.h ⊢ 𝐻 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) / 𝑠 ) )
fourierdlem60.n ⊢ 𝑁 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) )
fourierdlem60.d ⊢ 𝐷 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 )
Assertion fourierdlem60 ( 𝜑 → 𝐸 ∈ ( 𝐻 limℂ 0 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem60.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem60.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem60.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 fourierdlem60.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
5 fourierdlem60.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐹 limℂ 𝐵 ) )
6 fourierdlem60.g ⊢ 𝐺 = ( ℝ D 𝐹 )
7 fourierdlem60.domg ⊢ ( 𝜑 → dom 𝐺 = ( 𝐴 (,) 𝐵 ) )
8 fourierdlem60.e ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐺 limℂ 𝐵 ) )
9 fourierdlem60.h ⊢ 𝐻 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) / 𝑠 ) )
10 fourierdlem60.n ⊢ 𝑁 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) )
11 fourierdlem60.d ⊢ 𝐷 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 )
12 1 2 resubcld ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℝ )
13 12 rexrd ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℝ* )
14 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
15 1 2 sublt0d ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) < 0 ↔ 𝐴 < 𝐵 ) )
16 3 15 mpbird ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) < 0 )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
18 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐴 ∈ ℝ* )
20 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐵 ∈ ℝ* )
22 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐵 ∈ ℝ )
23 elioore ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) → 𝑠 ∈ ℝ )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑠 ∈ ℝ )
25 22 24 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) ∈ ℝ )
26 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
27 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28 26 27 pncan3d ⊢ ( 𝜑 → ( 𝐵 + ( 𝐴 − 𝐵 ) ) = 𝐴 )
29 28 eqcomd ⊢ ( 𝜑 → 𝐴 = ( 𝐵 + ( 𝐴 − 𝐵 ) ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐴 = ( 𝐵 + ( 𝐴 − 𝐵 ) ) )
31 12 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
32 13 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ* )
33 0xr ⊢ 0 ∈ ℝ*
34 33 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 0 ∈ ℝ* )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) )
36 32 34 35 ioogtlbd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐴 − 𝐵 ) < 𝑠 )
37 31 24 22 36 ltadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + ( 𝐴 − 𝐵 ) ) < ( 𝐵 + 𝑠 ) )
38 30 37 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐴 < ( 𝐵 + 𝑠 ) )
39 0red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 0 ∈ ℝ )
40 32 34 35 iooltubd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑠 < 0 )
41 24 39 22 40 ltadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) < ( 𝐵 + 0 ) )
42 26 addid1d ⊢ ( 𝜑 → ( 𝐵 + 0 ) = 𝐵 )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 0 ) = 𝐵 )
44 41 43 breqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) < 𝐵 )
45 19 21 25 38 44 eliood ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) ∈ ( 𝐴 (,) 𝐵 ) )
46 17 45 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ )
47 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
48 47 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
49 ax-resscn ⊢ ℝ ⊆ ℂ
50 48 49 sstrdi ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
51 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
52 51 18 2 3 lptioo2cn ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
53 4 50 52 5 limcrecl ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑌 ∈ ℝ )
55 46 54 resubcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ∈ ℝ )
56 55 10 fmptd ⊢ ( 𝜑 → 𝑁 : ( ( 𝐴 − 𝐵 ) (,) 0 ) ⟶ ℝ )
57 24 11 fmptd ⊢ ( 𝜑 → 𝐷 : ( ( 𝐴 − 𝐵 ) (,) 0 ) ⟶ ℝ )
58 10 oveq2i ⊢ ( ℝ D 𝑁 ) = ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) )
59 58 a1i ⊢ ( 𝜑 → ( ℝ D 𝑁 ) = ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) )
60 59 dmeqd ⊢ ( 𝜑 → dom ( ℝ D 𝑁 ) = dom ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) )
61 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
62 61 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
63 46 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℂ )
64 dvfre ⊢ ( ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
65 4 48 64 syl2anc ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
66 6 a1i ⊢ ( 𝜑 → 𝐺 = ( ℝ D 𝐹 ) )
67 66 feq1d ⊢ ( 𝜑 → ( 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ) )
68 65 67 mpbird ⊢ ( 𝜑 → 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ )
70 66 eqcomd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )
71 70 dmeqd ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = dom 𝐺 )
72 71 7 eqtr2d ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) = dom ( ℝ D 𝐹 ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐴 (,) 𝐵 ) = dom ( ℝ D 𝐹 ) )
74 45 73 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) ∈ dom ( ℝ D 𝐹 ) )
75 69 74 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ )
76 1red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 1 ∈ ℝ )
77 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
78 77 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
79 72 feq2d ⊢ ( 𝜑 → ( 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ↔ 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ) )
80 68 79 mpbird ⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
81 80 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
82 26 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐵 ∈ ℂ )
83 26 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 𝐵 ∈ ℂ )
84 0red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 0 ∈ ℝ )
85 62 26 dvmptc ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ 𝐵 ) ) = ( 𝑠 ∈ ℝ ↦ 0 ) )
86 ioossre ⊢ ( ( 𝐴 − 𝐵 ) (,) 0 ) ⊆ ℝ
87 86 a1i ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) ⊆ ℝ )
88 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
89 iooretop ⊢ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∈ ( topGen ‘ ran (,) )
90 89 a1i ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) ∈ ( topGen ‘ ran (,) ) )
91 62 83 84 85 87 88 51 90 dvmptres ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝐵 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 0 ) )
92 24 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑠 ∈ ℂ )
93 recn ⊢ ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ )
94 93 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 𝑠 ∈ ℂ )
95 1red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 1 ∈ ℝ )
96 62 dvmptid ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ 1 ) )
97 62 94 95 96 87 88 51 90 dvmptres ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) )
98 62 82 39 91 92 76 97 dvmptadd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 0 + 1 ) ) )
99 0p1e1 ⊢ ( 0 + 1 ) = 1
100 99 mpteq2i ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 0 + 1 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 )
101 98 100 eqtrdi ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) )
102 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
103 102 eqcomd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = 𝐹 )
104 103 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ℝ D 𝐹 ) )
105 80 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
106 104 70 105 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
107 fveq2 ⊢ ( 𝑥 = ( 𝐵 + 𝑠 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) )
108 fveq2 ⊢ ( 𝑥 = ( 𝐵 + 𝑠 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) )
109 62 62 45 76 78 81 101 106 107 108 dvmptco ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) · 1 ) ) )
110 75 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℂ )
111 110 mulid1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) · 1 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) )
112 111 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) · 1 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) )
113 109 112 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) )
114 limccl ⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ
115 114 5 sselid ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
116 115 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑌 ∈ ℂ )
117 115 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 𝑌 ∈ ℂ )
118 62 115 dvmptc ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ 𝑌 ) ) = ( 𝑠 ∈ ℝ ↦ 0 ) )
119 62 117 84 118 87 88 51 90 dvmptres ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑌 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 0 ) )
120 62 63 75 113 116 34 119 dvmptsub ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) − 0 ) ) )
121 110 subid1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) − 0 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) )
122 121 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) − 0 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) )
123 120 122 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) )
124 123 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) = dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) )
125 75 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ )
126 dmmptg ⊢ ( ∀ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ → dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) )
127 125 126 syl ⊢ ( 𝜑 → dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) )
128 60 124 127 3eqtrd ⊢ ( 𝜑 → dom ( ℝ D 𝑁 ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) )
129 11 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) )
130 129 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐷 ) = ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) ) )
131 130 97 eqtrd ⊢ ( 𝜑 → ( ℝ D 𝐷 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) )
132 131 dmeqd ⊢ ( 𝜑 → dom ( ℝ D 𝐷 ) = dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) )
133 76 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) 1 ∈ ℝ )
134 dmmptg ⊢ ( ∀ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) 1 ∈ ℝ → dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) )
135 133 134 syl ⊢ ( 𝜑 → dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) )
136 132 135 eqtrd ⊢ ( 𝜑 → dom ( ℝ D 𝐷 ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) )
137 eqid ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) )
138 eqid ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑌 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑌 )
139 eqid ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) )
140 45 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) ≠ 𝐵 ) ) → ( 𝐵 + 𝑠 ) ∈ ( 𝐴 (,) 𝐵 ) )
141 eqid ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝐵 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝐵 )
142 eqid ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 )
143 eqid ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) )
144 87 49 sstrdi ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) ⊆ ℂ )
145 14 recnd ⊢ ( 𝜑 → 0 ∈ ℂ )
146 141 144 26 145 constlimc ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝐵 ) limℂ 0 ) )
147 144 142 145 idlimc ⊢ ( 𝜑 → 0 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) limℂ 0 ) )
148 141 142 143 82 92 146 147 addlimc ⊢ ( 𝜑 → ( 𝐵 + 0 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) limℂ 0 ) )
149 42 148 eqeltrrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) limℂ 0 ) )
150 102 oveq1d ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) limℂ 𝐵 ) )
151 5 150 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) limℂ 𝐵 ) )
152 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) ∧ ¬ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) = 𝑌 ) → ( 𝐵 + 𝑠 ) = 𝐵 )
153 25 44 ltned ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) ≠ 𝐵 )
154 153 neneqd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ¬ ( 𝐵 + 𝑠 ) = 𝐵 )
155 154 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) → ¬ ( 𝐵 + 𝑠 ) = 𝐵 )
156 155 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) ∧ ¬ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) = 𝑌 ) → ¬ ( 𝐵 + 𝑠 ) = 𝐵 )
157 152 156 condan ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) → ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) = 𝑌 )
158 140 78 149 151 107 157 limcco ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) limℂ 0 ) )
159 138 144 115 145 constlimc ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑌 ) limℂ 0 ) )
160 137 138 139 63 116 158 159 sublimc ⊢ ( 𝜑 → ( 𝑌 − 𝑌 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) limℂ 0 ) )
161 115 subidd ⊢ ( 𝜑 → ( 𝑌 − 𝑌 ) = 0 )
162 10 eqcomi ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) = 𝑁
163 162 oveq1i ⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) limℂ 0 ) = ( 𝑁 limℂ 0 )
164 163 a1i ⊢ ( 𝜑 → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) limℂ 0 ) = ( 𝑁 limℂ 0 ) )
165 160 161 164 3eltr3d ⊢ ( 𝜑 → 0 ∈ ( 𝑁 limℂ 0 ) )
166 144 11 145 idlimc ⊢ ( 𝜑 → 0 ∈ ( 𝐷 limℂ 0 ) )
167 ubioo ⊢ ¬ 0 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 )
168 167 a1i ⊢ ( 𝜑 → ¬ 0 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) )
169 mptresid ⊢ ( I ↾ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 )
170 129 169 eqtr4di ⊢ ( 𝜑 → 𝐷 = ( I ↾ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) )
171 170 rneqd ⊢ ( 𝜑 → ran 𝐷 = ran ( I ↾ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) )
172 rnresi ⊢ ran ( I ↾ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) = ( ( 𝐴 − 𝐵 ) (,) 0 )
173 171 172 eqtr2di ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) = ran 𝐷 )
174 168 173 neleqtrd ⊢ ( 𝜑 → ¬ 0 ∈ ran 𝐷 )
175 0ne1 ⊢ 0 ≠ 1
176 175 neii ⊢ ¬ 0 = 1
177 elsng ⊢ ( 0 ∈ ℝ → ( 0 ∈ { 1 } ↔ 0 = 1 ) )
178 14 177 syl ⊢ ( 𝜑 → ( 0 ∈ { 1 } ↔ 0 = 1 ) )
179 176 178 mtbiri ⊢ ( 𝜑 → ¬ 0 ∈ { 1 } )
180 131 rneqd ⊢ ( 𝜑 → ran ( ℝ D 𝐷 ) = ran ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) )
181 eqid ⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 )
182 33 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
183 ioon0 ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( ( 𝐴 − 𝐵 ) (,) 0 ) ≠ ∅ ↔ ( 𝐴 − 𝐵 ) < 0 ) )
184 13 182 183 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) (,) 0 ) ≠ ∅ ↔ ( 𝐴 − 𝐵 ) < 0 ) )
185 16 184 mpbird ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) ≠ ∅ )
186 181 185 rnmptc ⊢ ( 𝜑 → ran ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) = { 1 } )
187 180 186 eqtr2d ⊢ ( 𝜑 → { 1 } = ran ( ℝ D 𝐷 ) )
188 179 187 neleqtrd ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐷 ) )
189 81 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
190 105 oveq1d ⊢ ( 𝜑 → ( 𝐺 limℂ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) limℂ 𝐵 ) )
191 8 190 eleqtrd ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) limℂ 𝐵 ) )
192 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) ∧ ¬ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = 𝐸 ) → ( 𝐵 + 𝑠 ) = 𝐵 )
193 155 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) ∧ ¬ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = 𝐸 ) → ¬ ( 𝐵 + 𝑠 ) = 𝐵 )
194 192 193 condan ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = 𝐸 )
195 140 189 149 191 108 194 limcco ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) limℂ 0 ) )
196 110 div1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) / 1 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) )
197 58 123 syl5eq ⊢ ( 𝜑 → ( ℝ D 𝑁 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) )
198 197 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ℝ D 𝑁 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) )
199 198 fveq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( ℝ D 𝑁 ) ‘ 𝑠 ) = ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ‘ 𝑠 ) )
200 fvmpt4 ⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ ) → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) )
201 35 75 200 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) )
202 199 201 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = ( ( ℝ D 𝑁 ) ‘ 𝑠 ) )
203 131 fveq1d ⊢ ( 𝜑 → ( ( ℝ D 𝐷 ) ‘ 𝑠 ) = ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ‘ 𝑠 ) )
204 203 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( ℝ D 𝐷 ) ‘ 𝑠 ) = ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ‘ 𝑠 ) )
205 fvmpt4 ⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ 1 ∈ ℝ ) → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ‘ 𝑠 ) = 1 )
206 35 76 205 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ‘ 𝑠 ) = 1 )
207 204 206 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 1 = ( ( ℝ D 𝐷 ) ‘ 𝑠 ) )
208 202 207 oveq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) / 1 ) = ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) )
209 196 208 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) )
210 209 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) ) )
211 210 oveq1d ⊢ ( 𝜑 → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) ) limℂ 0 ) )
212 195 211 eleqtrd ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) ) limℂ 0 ) )
213 13 14 16 56 57 128 136 165 166 174 188 212 lhop2 ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) ) limℂ 0 ) )
214 10 fvmpt2 ⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ∈ ℝ ) → ( 𝑁 ‘ 𝑠 ) = ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) )
215 35 55 214 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝑁 ‘ 𝑠 ) = ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) )
216 11 fvmpt2 ⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐷 ‘ 𝑠 ) = 𝑠 )
217 35 35 216 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐷 ‘ 𝑠 ) = 𝑠 )
218 215 217 oveq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) / 𝑠 ) )
219 218 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) / 𝑠 ) ) )
220 219 9 eqtr4di ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) ) = 𝐻 )
221 220 oveq1d ⊢ ( 𝜑 → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) ) limℂ 0 ) = ( 𝐻 limℂ 0 ) )
222 213 221 eleqtrd ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐻 limℂ 0 ) )