Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem45 Structured version   Unicode version

Theorem fourierdlem45 31775
 Description: If has bounded derivative on and is a convergent sequence, with values in , then the composition of and is a sequence converging to its . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem45.a
fourierdlem45.b
fourierdlem45.altb
fourierdlem45.f
fourierdlem45.dmdv
fourierdlem45.dvbd
fourierdlem45.m
fourierdlem45.r
fourierdlem45.s
fourierdlem45.rcnv
fourierdlem45.k
Assertion
Ref Expression
fourierdlem45
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,   ,,,   ,,   ,   ,,   ,   ,   ,,,   ,   ,,   ,   ,   ,,,   ,,,   ,   ,
Allowed substitution hints:   ()   ()   ()   (,)   (,,)   (,)   (,)

Proof of Theorem fourierdlem45
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2467 . 2
2 fourierdlem45.f . . . . . 6
3 cncff 21265 . . . . . 6
42, 3syl 16 . . . . 5
54adantr 465 . . . 4
6 fourierdlem45.r . . . . 5
76ffvelrnda 6032 . . . 4
85, 7ffvelrnd 6033 . . 3
9 fourierdlem45.s . . 3
108, 9fmptd 6056 . 2
11 ssrab2 3590 . . . . 5
12 fourierdlem45.k . . . . . 6
1311a1i 11 . . . . . . 7
14 rpre 11238 . . . . . . . . . . . . 13
1514adantl 466 . . . . . . . . . . . 12
16 fveq2 5872 . . . . . . . . . . . . . . . . . . 19
1716fveq2d 5876 . . . . . . . . . . . . . . . . . 18
1817cbvmptv 4544 . . . . . . . . . . . . . . . . 17
1918rneqi 5235 . . . . . . . . . . . . . . . 16
2019supeq1i 7919 . . . . . . . . . . . . . . 15
21 fourierdlem45.a . . . . . . . . . . . . . . . . . . 19
22 fourierdlem45.b . . . . . . . . . . . . . . . . . . 19
23 fourierdlem45.altb . . . . . . . . . . . . . . . . . . 19
24 ioomidp 31441 . . . . . . . . . . . . . . . . . . 19
2521, 22, 23, 24syl3anc 1228 . . . . . . . . . . . . . . . . . 18
26 ne0i 3796 . . . . . . . . . . . . . . . . . 18
2725, 26syl 16 . . . . . . . . . . . . . . . . 17
28 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . . 23
2928a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
30 dvfre 22222 . . . . . . . . . . . . . . . . . . . . . 22
314, 29, 30syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
32 fourierdlem45.dmdv . . . . . . . . . . . . . . . . . . . . . 22
3332feq2d 5724 . . . . . . . . . . . . . . . . . . . . 21
3431, 33mpbid 210 . . . . . . . . . . . . . . . . . . . 20
35 ax-resscn 9561 . . . . . . . . . . . . . . . . . . . . 21
3635a1i 11 . . . . . . . . . . . . . . . . . . . 20
3734, 36fssd 5746 . . . . . . . . . . . . . . . . . . 19
3837ffvelrnda 6032 . . . . . . . . . . . . . . . . . 18
3938abscld 13247 . . . . . . . . . . . . . . . . 17
40 fourierdlem45.dvbd . . . . . . . . . . . . . . . . 17
41 eqid 2467 . . . . . . . . . . . . . . . . 17
42 eqid 2467 . . . . . . . . . . . . . . . . 17
4327, 39, 40, 41, 42suprnmpt 31352 . . . . . . . . . . . . . . . 16
4443simpld 459 . . . . . . . . . . . . . . 15
4520, 44syl5eqel 2559 . . . . . . . . . . . . . 14
4645adantr 465 . . . . . . . . . . . . 13
47 peano2re 9764 . . . . . . . . . . . . 13
4846, 47syl 16 . . . . . . . . . . . 12
49 0red 9609 . . . . . . . . . . . . . 14
50 1red 9623 . . . . . . . . . . . . . . . 16
5149, 50readdcld 9635 . . . . . . . . . . . . . . 15
5245, 47syl 16 . . . . . . . . . . . . . . 15
5349ltp1d 10488 . . . . . . . . . . . . . . 15
5437, 25ffvelrnd 6033 . . . . . . . . . . . . . . . . . 18
5554abscld 13247 . . . . . . . . . . . . . . . . 17
5654absge0d 13255 . . . . . . . . . . . . . . . . 17
5743simprd 463 . . . . . . . . . . . . . . . . . . 19
58 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22
5958fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21
6020a1i 11 . . . . . . . . . . . . . . . . . . . . 21
6159, 60breq12d 4466 . . . . . . . . . . . . . . . . . . . 20
6261cbvralv 3093 . . . . . . . . . . . . . . . . . . 19
6357, 62sylibr 212 . . . . . . . . . . . . . . . . . 18
64 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21
6564fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20
6665breq1d 4463 . . . . . . . . . . . . . . . . . . 19
6766rspcva 3217 . . . . . . . . . . . . . . . . . 18
6825, 63, 67syl2anc 661 . . . . . . . . . . . . . . . . 17
6949, 55, 45, 56, 68letrd 9750 . . . . . . . . . . . . . . . 16
7049, 45, 50, 69leadd1dd 10178 . . . . . . . . . . . . . . 15
7149, 51, 52, 53, 70ltletrd 9753 . . . . . . . . . . . . . 14
7249, 71gtned 9731 . . . . . . . . . . . . 13
7372adantr 465 . . . . . . . . . . . 12
7415, 48, 73redivcld 10384 . . . . . . . . . . 11
75 rpgt0 11243 . . . . . . . . . . . . 13
7675adantl 466 . . . . . . . . . . . 12
7771adantr 465 . . . . . . . . . . . 12
7815, 48, 76, 77divgt0d 10493 . . . . . . . . . . 11
7974, 78elrpd 11266 . . . . . . . . . 10
80 fourierdlem45.m . . . . . . . . . . . 12
8180adantr 465 . . . . . . . . . . 11
82 fourierdlem45.rcnv . . . . . . . . . . . 12
8382adantr 465 . . . . . . . . . . 11
841climcau 13473 . . . . . . . . . . 11
8581, 83, 84syl2anc 661 . . . . . . . . . 10
86 breq2 4457 . . . . . . . . . . . . 13
8786ralbidv 2906 . . . . . . . . . . . 12
8887rexbidv 2978 . . . . . . . . . . 11
8988rspcva 3217 . . . . . . . . . 10
9079, 85, 89syl2anc 661 . . . . . . . . 9
91 nfv 1683 . . . . . . . . . 10
92 id 22 . . . . . . . . . . 11
9392a1ii 27 . . . . . . . . . 10
9491, 93reximdai 2936 . . . . . . . . 9
9590, 94mpd 15 . . . . . . . 8
96 rabn0 3810 . . . . . . . 8
9795, 96sylibr 212 . . . . . . 7
98 infmssuzcl 11177 . . . . . . 7
9913, 97, 98syl2anc 661 . . . . . 6
10012, 99syl5eqel 2559 . . . . 5
10111, 100sseldi 3507 . . . 4
1029a1i 11 . . . . . . . . 9
103 fveq2 5872 . . . . . . . . . . 11
104103fveq2d 5876 . . . . . . . . . 10
105104adantl 466 . . . . . . . . 9
106 uzss 11114 . . . . . . . . . . . 12
107101, 106syl 16 . . . . . . . . . . 11
108107adantr 465 . . . . . . . . . 10
109 simpr 461 . . . . . . . . . 10
110108, 109sseldd 3510 . . . . . . . . 9
1114ad2antrr 725 . . . . . . . . . 10
1126ad2antrr 725 . . . . . . . . . . 11
113112, 110ffvelrnd 6033 . . . . . . . . . 10
114111, 113ffvelrnd 6033 . . . . . . . . 9
115102, 105, 110, 114fvmptd 5962 . . . . . . . 8
116 fveq2 5872 . . . . . . . . . . 11
117116fveq2d 5876 . . . . . . . . . 10
118117adantl 466 . . . . . . . . 9
119101adantr 465 . . . . . . . . 9
120112, 119ffvelrnd 6033 . . . . . . . . . 10
121111, 120ffvelrnd 6033 . . . . . . . . 9
122102, 118, 119, 121fvmptd 5962 . . . . . . . 8
123115, 122oveq12d 6313 . . . . . . 7
124123fveq2d 5876 . . . . . 6
125114recnd 9634 . . . . . . . . . . 11
126121recnd 9634 . . . . . . . . . . 11
127125, 126subcld 9942 . . . . . . . . . 10
128127abscld 13247 . . . . . . . . 9
129128adantr 465 . . . . . . . 8
13045ad2antrr 725 . . . . . . . . . 10
131130adantr 465 . . . . . . . . 9
13228a1i 11 . . . . . . . . . . . 12
1336adantr 465 . . . . . . . . . . . . 13
134133, 101ffvelrnd 6033 . . . . . . . . . . . 12
135132, 134sseldd 3510 . . . . . . . . . . 11
136135ad2antrr 725 . . . . . . . . . 10
13728, 113sseldi 3507 . . . . . . . . . . 11
138137adantr 465 . . . . . . . . . 10
139136, 138resubcld 9999 . . . . . . . . 9
140131, 139remulcld 9636 . . . . . . . 8
14114ad2antlr 726 . . . . . . . . 9
142141adantr 465 . . . . . . . 8
14335, 114sseldi 3507 . . . . . . . . . . 11
144143adantr 465 . . . . . . . . . 10
145126adantr 465 . . . . . . . . . 10
146144, 145abssubd 13264 . . . . . . . . 9
14721ad3antrrr 729 . . . . . . . . . . 11
14822ad3antrrr 729 . . . . . . . . . . 11
149111adantr 465 . . . . . . . . . . 11
15032ad3antrrr 729 . . . . . . . . . . 11
15163ad3antrrr 729 . . . . . . . . . . 11
152113adantr 465 . . . . . . . . . . 11
153137rexrd 9655 . . . . . . . . . . . . 13
154153adantr 465 . . . . . . . . . . . 12
15522rexrd 9655 . . . . . . . . . . . . . . 15
156155adantr 465 . . . . . . . . . . . . . 14
157156adantlr 714 . . . . . . . . . . . . 13
158157adantr 465 . . . . . . . . . . . 12
159 simpr 461 . . . . . . . . . . . 12
16021rexrd 9655 . . . . . . . . . . . . . . 15
161160adantr 465 . . . . . . . . . . . . . 14
162155adantr 465 . . . . . . . . . . . . . 14
163 iooltub 31435 . . . . . . . . . . . . . 14
164161, 162, 134, 163syl3anc 1228 . . . . . . . . . . . . 13
165164ad2antrr 725 . . . . . . . . . . . 12
166154, 158, 136, 159, 165eliood 31418 . . . . . . . . . . 11
167147, 148, 149, 150, 131, 151, 152, 166dvbdfbdioolem1 31581 . . . . . . . . . 10
168167simpld 459 . . . . . . . . 9
169146, 168eqbrtrd 4473 . . . . . . . 8
170131, 47syl 16 . . . . . . . . . . 11
171170, 139jca 532 . . . . . . . . . 10
172 remulcl 9589 . . . . . . . . . 10
173171, 172syl 16 . . . . . . . . 9
174138, 136posdifd 10151 . . . . . . . . . . . 12
175159, 174mpbid 210 . . . . . . . . . . 11
176139, 175elrpd 11266 . . . . . . . . . 10
177 1rp 11236 . . . . . . . . . . . 12
178177a1i 11 . . . . . . . . . . 11
179131, 178ltaddrpd 11297 . . . . . . . . . 10
180131, 170, 176, 179ltmul1dd 11319 . . . . . . . . 9
18128a1i 11 . . . . . . . . . . . . . . . 16
182181, 113sseldd 3510 . . . . . . . . . . . . . . 15
18328, 120sseldi 3507 . . . . . . . . . . . . . . 15
184182, 183resubcld 9999 . . . . . . . . . . . . . 14
18535, 184sseldi 3507 . . . . . . . . . . . . 13
186185abscld 13247 . . . . . . . . . . . 12
187186adantr 465 . . . . . . . . . . 11
18874ad2antrr 725 . . . . . . . . . . 11
189139leabsd 13226 . . . . . . . . . . . 12
19035, 136sseldi 3507 . . . . . . . . . . . . 13
19135, 137sseldi 3507 . . . . . . . . . . . . . 14
192191adantr 465 . . . . . . . . . . . . 13
193190, 192abssubd 13264 . . . . . . . . . . . 12
194189, 193breqtrd 4477 . . . . . . . . . . 11
195 fveq2 5872 . . . . . . . . . . . . . . . . . 18
196 raleq 3063 . . . . . . . . . . . . . . . . . 18
197195, 196syl 16 . . . . . . . . . . . . . . . . 17
198 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21
199198oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20
200199fveq2d 5876 . . . . . . . . . . . . . . . . . . 19
201200breq1d 4463 . . . . . . . . . . . . . . . . . 18
202201ralbidv 2906 . . . . . . . . . . . . . . . . 17
203197, 202bitrd 253 . . . . . . . . . . . . . . . 16
204203elrab 3266 . . . . . . . . . . . . . . 15
205100, 204sylib 196 . . . . . . . . . . . . . 14
206205simprd 463 . . . . . . . . . . . . 13
207206r19.21bi 2836 . . . . . . . . . . . 12
208207adantr 465 . . . . . . . . . . 11
209139, 187, 188, 194, 208lelttrd 9751 . . . . . . . . . 10
21052, 71elrpd 11266 . . . . . . . . . . . 12
211210ad3antrrr 729 . . . . . . . . . . 11
212139, 142, 211ltmuldiv2d 11312 . . . . . . . . . 10
213209, 212mpbird 232 . . . . . . . . 9
214140, 173, 142, 180, 213lttrd 9754 . . . . . . . 8
215129, 140, 142, 169, 214lelttrd 9751 . . . . . . 7
216 fveq2 5872 . . . . . . . . . . . . . . 15
217216oveq1d 6310 . . . . . . . . . . . . . 14
218217adantl 466 . . . . . . . . . . . . 13
219126subidd 9930 . . . . . . . . . . . . . 14
220219adantr 465 . . . . . . . . . . . . 13
221218, 220eqtrd 2508 . . . . . . . . . . . 12
222221fveq2d 5876 . . . . . . . . . . 11
223 eqidd 2468 . . . . . . . . . . . 12
224223abs00bd 13104 . . . . . . . . . . 11
225222, 224eqtrd 2508 . . . . . . . . . 10
22676ad2antrr 725 . . . . . . . . . 10
227225, 226eqbrtrd 4473 . . . . . . . . 9
228227adantlr 714 . . . . . . . 8
229 simpll 753 . . . . . . . . 9
230229, 183syl 16 . . . . . . . . . 10
231229, 137syl 16 . . . . . . . . . 10
232 id 22 . . . . . . . . . . . . 13
233232eqcomd 2475 . . . . . . . . . . . 12
234233necon3bi 2696 . . . . . . . . . . 11
235234adantl 466 . . . . . . . . . 10
236 simplr 754 . . . . . . . . . 10
237230, 231, 235, 236lttri5d 31399 . . . . . . . . 9
238128adantr 465 . . . . . . . . . 10
239130, 184remulcld 9636 . . . . . . . . . . 11
240239adantr 465 . . . . . . . . . 10
241141adantr 465 . . . . . . . . . 10
24221ad3antrrr 729 . . . . . . . . . . . 12
24322ad3antrrr 729 . . . . . . . . . . . 12
244111adantr 465 . . . . . . . . . . . 12
24532ad3antrrr 729 . . . . . . . . . . . 12
24645ad3antrrr 729 . . . . . . . . . . . 12
24763ad3antrrr 729 . . . . . . . . . . . 12
248120adantr 465 . . . . . . . . . . . 12
249135rexrd 9655 . . . . . . . . . . . . . 14
250249ad2antrr 725 . . . . . . . . . . . . 13
251243rexrd 9655 . . . . . . . . . . . . 13
252137adantr 465 . . . . . . . . . . . . 13
253 simpr 461 . . . . . . . . . . . . 13
254160adantr 465 . . . . . . . . . . . . . . . 16
255254adantlr 714 . . . . . . . . . . . . . . 15
256 iooltub 31435 . . . . . . . . . . . . . . 15
257255, 157, 113, 256syl3anc 1228 . . . . . . . . . . . . . 14
258257adantr 465 . . . . . . . . . . . . 13
259250, 251, 252, 253, 258eliood 31418 . . . . . . . . . . . 12
260242, 243, 244, 245, 246, 247, 248, 259dvbdfbdioolem1 31581 . . . . . . . . . . 11
261260simpld 459 . . . . . . . . . 10
262 1red 9623 . . . . . . . . . . . . 13
263246, 262readdcld 9635 . . . . . . . . . . . 12
264183adantr 465 . . . . . . . . . . . . 13
265252, 264resubcld 9999 . . . . . . . . . . . 12
266263, 265remulcld 9636 . . . . . . . . . . 11
267246, 47syl 16 . . . . . . . . . . . 12
268264, 252posdifd 10151 . . . . . . . . . . . . . 14
269253, 268mpbid 210 . . . . . . . . . . . . 13
270265, 269elrpd 11266 . . . . . . . . . . . 12
271246ltp1d 10488 . . . . . . . . . . . 12
272246, 267, 270, 271ltmul1dd 11319 . . . . . . . . . . 11
273186adantr 465 . . . . . . . . . . . . 13
27474ad2antrr 725 . . . . . . . . . . . . 13
275265leabsd 13226 . . . . . . . . . . . . 13
276207adantr 465 . . . . . . . . . . . . 13
277265, 273, 274, 275, 276lelttrd 9751 . . . . . . . . . . . 12
278210ad3antrrr 729 . . . . . . . . . . . . 13
279265, 241, 278ltmuldiv2d 11312 . . . . . . . . . . . 12
280277, 279mpbird 232 . . . . . . . . . . 11
281240, 266, 241, 272, 280lttrd 9754 . . . . . . . . . 10
282238, 240, 241, 261, 281lelttrd 9751 . . . . . . . . 9
283229, 237, 282syl2anc 661 . . . . . . . 8
284228, 283pm2.61dan 789 . . . . . . 7
285215, 284pm2.61dan 789 . . . . . 6
286124, 285eqbrtrd 4473 . . . . 5
287286ralrimiva 2881 . . . 4
288 raleq 3063 . . . . . . 7
289195, 288syl 16 . . . . . 6
290 fveq2 5872 . . . . . . . . . 10
291290oveq2d 6311 . . . . . . . . 9
292291fveq2d 5876 . . . . . . . 8
293292breq1d 4463 . . . . . . 7
294293ralbidv 2906 . . . . . 6