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 
|- ( ph -> A e. RR )
fourierdlem60.b 
|- ( ph -> B e. RR )
fourierdlem60.altb 
|- ( ph -> A < B )
fourierdlem60.f 
|- ( ph -> F : ( A (,) B ) --> RR )
fourierdlem60.y 
|- ( ph -> Y e. ( F limCC B ) )
fourierdlem60.g 
|- G = ( RR _D F )
fourierdlem60.domg 
|- ( ph -> dom G = ( A (,) B ) )
fourierdlem60.e 
|- ( ph -> E e. ( G limCC B ) )
fourierdlem60.h 
|- H = ( s e. ( ( A - B ) (,) 0 ) |-> ( ( ( F ` ( B + s ) ) - Y ) / s ) )
fourierdlem60.n 
|- N = ( s e. ( ( A - B ) (,) 0 ) |-> ( ( F ` ( B + s ) ) - Y ) )
fourierdlem60.d 
|- D = ( s e. ( ( A - B ) (,) 0 ) |-> s )
Assertion fourierdlem60 
|- ( ph -> E e. ( H limCC 0 ) )

Proof

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