Metamath Proof Explorer


Theorem fourierdlem61

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 fourierdlem61.a φ A
fourierdlem61.b φ B
fourierdlem61.altb φ A < B
fourierdlem61.f φ F : A B
fourierdlem61.y φ Y F lim A
fourierdlem61.g G = D F
fourierdlem61.domg φ dom G = A B
fourierdlem61.e φ E G lim A
fourierdlem61.h H = s 0 B A F A + s Y s
fourierdlem61.n N = s 0 B A F A + s Y
fourierdlem61.d D = s 0 B A s
Assertion fourierdlem61 φ E H lim 0

Proof

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