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

Theorem fourierdlem91 31821
 Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem91.p ..^
fourierdlem91.t
fourierdlem91.m
fourierdlem91.q
fourierdlem91.f
fourierdlem91.6
fourierdlem91.fcn ..^
fourierdlem91.l ..^ lim
fourierdlem91.c
fourierdlem91.d
fourierdlem91.o ..^
fourierdlem91.h
fourierdlem91.n
fourierdlem91.s
fourierdlem91.e
fourierdlem91.J
fourierdlem91.17 ..^
fourierdlem91.u
fourierdlem91.i ..^
fourierdlem91.w ..^
Assertion
Ref Expression
fourierdlem91 lim
Distinct variable groups:   ,,,   ,,,,   ,,,   ,,,   ,,   ,,   ,,   ,,,   ,   ,,   ,,,   ,   ,,,   ,,   ,,,   ,   ,   ,,,   ,,   ,,,   ,,   ,,   ,,,   ,,   ,,   ,,,   ,,   ,   ,,,   ,,   ,   ,,,   ,,   ,,   ,,   ,,,   ,,,   ,,
Allowed substitution hints:   (,)   ()   ()   (,,,,,,)   ()   ()   (,)   (,,,,)   (,)   (,,,)   (,,,,)   (,)   (,,,)   (,,,,,,)   (,,)   (,,,,,,)   (,,,,)   (,,,)

Proof of Theorem fourierdlem91
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fourierdlem91.f . . . . . 6
2 fdm 5741 . . . . . . . 8
31, 2syl 16 . . . . . . 7
43feq2d 5724 . . . . . 6
51, 4mpbird 232 . . . . 5
6 ioosscn 31414 . . . . . 6
76a1i 11 . . . . 5
8 ioossre 11598 . . . . . . 7
98a1i 11 . . . . . 6
103sseq2d 3537 . . . . . 6
119, 10mpbird 232 . . . . 5
12 ax-resscn 9561 . . . . . 6
13 fourierdlem91.u . . . . . . 7
14 fourierdlem91.t . . . . . . . . . . . . . . 15
15 fourierdlem91.p . . . . . . . . . . . . . . 15 ..^
16 fourierdlem91.m . . . . . . . . . . . . . . 15
17 fourierdlem91.q . . . . . . . . . . . . . . 15
18 fourierdlem91.c . . . . . . . . . . . . . . 15
19 fourierdlem91.d . . . . . . . . . . . . . . . 16
20 elioore 11571 . . . . . . . . . . . . . . . 16
2119, 20syl 16 . . . . . . . . . . . . . . 15
22 elioo4g 11597 . . . . . . . . . . . . . . . . . 18
2319, 22sylib 196 . . . . . . . . . . . . . . . . 17
2423simprd 463 . . . . . . . . . . . . . . . 16
2524simpld 459 . . . . . . . . . . . . . . 15
26 fourierdlem91.o . . . . . . . . . . . . . . 15 ..^
27 oveq1 6302 . . . . . . . . . . . . . . . . . . 19
2827eleq1d 2536 . . . . . . . . . . . . . . . . . 18
2928rexbidv 2978 . . . . . . . . . . . . . . . . 17
3029cbvrabv 3117 . . . . . . . . . . . . . . . 16
3130uneq2i 3660 . . . . . . . . . . . . . . 15
32 fourierdlem91.n . . . . . . . . . . . . . . . 16
33 fourierdlem91.h . . . . . . . . . . . . . . . . . 18
3433fveq2i 5875 . . . . . . . . . . . . . . . . 17
3534oveq1i 6305 . . . . . . . . . . . . . . . 16
3632, 35eqtri 2496 . . . . . . . . . . . . . . 15
37 fourierdlem91.s . . . . . . . . . . . . . . . 16
38 isoeq5 6218 . . . . . . . . . . . . . . . . . . 19
3933, 38ax-mp 5 . . . . . . . . . . . . . . . . . 18
4039ax-gen 1601 . . . . . . . . . . . . . . . . 17
41 iotabi 5566 . . . . . . . . . . . . . . . . 17
4240, 41ax-mp 5 . . . . . . . . . . . . . . . 16
4337, 42eqtri 2496 . . . . . . . . . . . . . . 15
4414, 15, 16, 17, 18, 21, 25, 26, 31, 36, 43fourierdlem54 31784 . . . . . . . . . . . . . 14
4544simpld 459 . . . . . . . . . . . . 13
4645simprd 463 . . . . . . . . . . . 12
4745simpld 459 . . . . . . . . . . . . 13
4826fourierdlem2 31732 . . . . . . . . . . . . 13 ..^
4947, 48syl 16 . . . . . . . . . . . 12 ..^
5046, 49mpbid 210 . . . . . . . . . . 11 ..^
5150simpld 459 . . . . . . . . . 10
52 elmapi 7452 . . . . . . . . . 10
5351, 52syl 16 . . . . . . . . 9
54 fourierdlem91.17 . . . . . . . . . 10 ..^
55 fzofzp1 11889 . . . . . . . . . 10 ..^
5654, 55syl 16 . . . . . . . . 9
5753, 56ffvelrnd 6033 . . . . . . . 8
5815, 16, 17fourierdlem11 31741 . . . . . . . . . . . 12
5958simp1d 1008 . . . . . . . . . . 11
6059rexrd 9655 . . . . . . . . . 10
6158simp2d 1009 . . . . . . . . . 10
62 iocssre 11616 . . . . . . . . . 10
6360, 61, 62syl2anc 661 . . . . . . . . 9
6458simp3d 1010 . . . . . . . . . . 11
65 fourierdlem91.e . . . . . . . . . . 11
6659, 61, 64, 14, 65fourierdlem4 31734 . . . . . . . . . 10
6766, 57ffvelrnd 6033 . . . . . . . . 9
6863, 67sseldd 3510 . . . . . . . 8
6957, 68resubcld 9999 . . . . . . 7
7013, 69syl5eqel 2559 . . . . . 6
7112, 70sseldi 3507 . . . . 5
72 eqid 2467 . . . . 5
73 ioossre 11598 . . . . . . . 8
7473a1i 11 . . . . . . 7
753sseq2d 3537 . . . . . . 7
7674, 75mpbird 232 . . . . . 6
7759, 61iccssred 31426 . . . . . . . . 9
78 fourierdlem91.J . . . . . . . . . . 11
7959, 61, 64, 78fourierdlem17 31747 . . . . . . . . . 10
80 ssid 3528 . . . . . . . . . . . . 13
8180a1i 11 . . . . . . . . . . . 12
82 elfzofz 11823 . . . . . . . . . . . . . 14 ..^
8354, 82syl 16 . . . . . . . . . . . . 13
8453, 83ffvelrnd 6033 . . . . . . . . . . . 12
8581, 84sseldd 3510 . . . . . . . . . . 11
8666, 85ffvelrnd 6033 . . . . . . . . . 10
8779, 86ffvelrnd 6033 . . . . . . . . 9
8877, 87sseldd 3510 . . . . . . . 8
8988, 68, 70iooshift 31449 . . . . . . 7
9089sseq1d 3536 . . . . . 6
9176, 90mpbid 210 . . . . 5
92 simpl 457 . . . . . 6
938sseli 3505 . . . . . . 7
9493adantl 466 . . . . . 6
95 id 22 . . . . . . . . . . . . 13
9661, 59resubcld 9999 . . . . . . . . . . . . . . . 16
9714, 96syl5eqel 2559 . . . . . . . . . . . . . . 15
9859, 61posdifd 10151 . . . . . . . . . . . . . . . . 17
9964, 98mpbid 210 . . . . . . . . . . . . . . . 16
10014a1i 11 . . . . . . . . . . . . . . . . 17
101100eqcomd 2475 . . . . . . . . . . . . . . . 16
10299, 101breqtrd 4477 . . . . . . . . . . . . . . 15
10397, 102elrpd 11266 . . . . . . . . . . . . . 14
104103rpcnd 11270 . . . . . . . . . . . . 13
10595, 104syl 16 . . . . . . . . . . . 12
106102gt0ne0d 10129 . . . . . . . . . . . . 13
10795, 106syl 16 . . . . . . . . . . . 12
10871, 105, 107divcan1d 10333 . . . . . . . . . . 11
109108eqcomd 2475 . . . . . . . . . 10
110109oveq2d 6311 . . . . . . . . 9
111110adantr 465 . . . . . . . 8
112111fveq2d 5876 . . . . . . 7
113 eqidd 2468 . . . . . . 7
1141adantr 465 . . . . . . . 8
11595, 97syl 16 . . . . . . . . 9
116115adantr 465 . . . . . . . 8
11713oveq1i 6305 . . . . . . . . . . . 12
118117a1i 11 . . . . . . . . . . 11
11968recnd 9634 . . . . . . . . . . . . . 14
12057recnd 9634 . . . . . . . . . . . . . 14
121119, 120negsubdi2d 9958 . . . . . . . . . . . . 13
122121eqcomd 2475 . . . . . . . . . . . 12
123122oveq1d 6310 . . . . . . . . . . 11
12465a1i 11 . . . . . . . . . . . . . . . . 17
125 id 22 . . . . . . . . . . . . . . . . . . 19
126 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . 22
127126oveq1d 6310 . . . . . . . . . . . . . . . . . . . . 21
128127fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20
129128oveq1d 6310 . . . . . . . . . . . . . . . . . . 19
130125, 129oveq12d 6313 . . . . . . . . . . . . . . . . . 18
131130adantl 466 . . . . . . . . . . . . . . . . 17
13261, 57resubcld 9999 . . . . . . . . . . . . . . . . . . . . . 22
133132, 115, 107redivcld 10384 . . . . . . . . . . . . . . . . . . . . 21
134133flcld 11915 . . . . . . . . . . . . . . . . . . . 20
135134zred 10978 . . . . . . . . . . . . . . . . . . 19
136135, 115remulcld 9636 . . . . . . . . . . . . . . . . . 18
13757, 136readdcld 9635 . . . . . . . . . . . . . . . . 17
138124, 131, 57, 137fvmptd 5962 . . . . . . . . . . . . . . . 16
139138oveq1d 6310 . . . . . . . . . . . . . . 15
14012, 135sseldi 3507 . . . . . . . . . . . . . . . . 17
141140, 105mulcld 9628 . . . . . . . . . . . . . . . 16
142120, 141pncan2d 9944 . . . . . . . . . . . . . . 15
143139, 142eqtrd 2508 . . . . . . . . . . . . . 14
144143, 141eqeltrd 2555 . . . . . . . . . . . . 13
145144, 105, 107divnegd 10345 . . . . . . . . . . . 12
146145eqcomd 2475 . . . . . . . . . . 11
147118, 123, 1463eqtrd 2512 . . . . . . . . . 10
148143oveq1d 6310 . . . . . . . . . . . . 13
149140, 105, 107divcan4d 10338 . . . . . . . . . . . . 13
150 eqidd 2468 . . . . . . . . . . . . 13
151148, 149, 1503eqtrd 2512 . . . . . . . . . . . 12
152151, 134eqeltrd 2555 . . . . . . . . . . 11
153152znegcld 10980 . . . . . . . . . 10
154147, 153eqeltrd 2555 . . . . . . . . 9
155154adantr 465 . . . . . . . 8
156 simpr 461 . . . . . . . 8
157 fourierdlem91.6 . . . . . . . . . 10
158157idi 2 . . . . . . . . 9
159158adantlr 714 . . . . . . . 8
160114, 116, 155, 156, 159fperiodmul 31404 . . . . . . 7
161112, 113, 1603eqtrd 2512 . . . . . 6
16292, 94, 161syl2anc 661 . . . . 5
16315fourierdlem2 31732 . . . . . . . . . . . . 13 ..^
16416, 163syl 16 . . . . . . . . . . . 12 ..^
16517, 164mpbid 210 . . . . . . . . . . 11 ..^
166165simpld 459 . . . . . . . . . 10
167 elmapi 7452 . . . . . . . . . 10
168166, 167syl 16 . . . . . . . . 9
16995, 168syl 16 . . . . . . . 8
170 elfzofz 11823 . . . . . . . . . . 11 ..^
171170ssriv 3513 . . . . . . . . . 10 ..^
172171a1i 11 . . . . . . . . 9 ..^
17395, 16syl 16 . . . . . . . . . . . 12
17495, 17syl 16 . . . . . . . . . . . 12
175 fourierdlem91.i . . . . . . . . . . . 12 ..^
17615, 173, 174, 14, 65, 78, 175fourierdlem37 31767 . . . . . . . . . . 11 ..^ ..^ ..^
177176simpld 459 . . . . . . . . . 10 ..^
178177, 84ffvelrnd 6033 . . . . . . . . 9 ..^
179172, 178sseldd 3510 . . . . . . . 8
180169, 179ffvelrnd 6033 . . . . . . 7
181 fzofzp1 11889 . . . . . . . . 9 ..^
182178, 181syl 16 . . . . . . . 8
183169, 182ffvelrnd 6033 . . . . . . 7
184165simprd 463 . . . . . . . . 9 ..^
185184simprd 463 . . . . . . . 8 ..^
18615, 16, 17, 14, 65, 78, 175fourierdlem37 31767 . . . . . . . . . 10 ..^ ..^ ..^
187186simpld 459 . . . . . . . . 9 ..^
188187, 84ffvelrnd 6033 . . . . . . . 8 ..^
189 fveq2 5872 . . . . . . . . . 10
190 oveq1 6302 . . . . . . . . . . 11
191190fveq2d 5876 . . . . . . . . . 10
192189, 191breq12d 4466 . . . . . . . . 9
193192rspccva 3218 . . . . . . . 8 ..^ ..^
194185, 188, 193syl2anc 661 . . . . . . 7
19595, 188jca 532 . . . . . . . 8 ..^
196 eleq1 2539 . . . . . . . . . . 11 ..^ ..^
197196anbi2d 703 . . . . . . . . . 10 ..^ ..^
198189, 191oveq12d 6313 . . . . . . . . . . . 12
199198reseq2d 5279 . . . . . . . . . . 11
200198oveq1d 6310 . . . . . . . . . . 11
201199, 200eleq12d 2549 . . . . . . . . . 10
202197, 201imbi12d 320 . . . . . . . . 9 ..^ ..^
203 fourierdlem91.fcn . . . . . . . . 9 ..^
204202, 203vtoclg 3176 . . . . . . . 8 ..^ ..^
205188, 195, 204sylc 60 . . . . . . 7
206 nfcv 2629 . . . . . . . . 9
207 nfv 1683 . . . . . . . . . 10 ..^
208 fourierdlem91.w . . . . . . . . . . . . 13 ..^
209 nfmpt1 4542 . . . . . . . . . . . . 13 ..^
210208, 209nfcxfr 2627 . . . . . . . . . . . 12
211210, 206nffv 5879 . . . . . . . . . . 11
212 nfcv 2629 . . . . . . . . . . 11 lim
213211, 212nfel 2642 . . . . . . . . . 10 lim
214207, 213nfim 1867 . . . . . . . . 9 ..^ lim
215197biimpar 485 . . . . . . . . . . . . . 14 ..^ ..^
2162153adant2 1015 . . . . . . . . . . . . 13 ..^ lim ..^ ..^
217 simp2 997 . . . . . . . . . . . . 13 ..^ lim ..^ ..^ lim
218216, 217mpd 15 . . . . . . . . . . . 12 ..^ lim ..^ lim
219 fveq2 5872 . . . . . . . . . . . . . . . . 17
220219eqcomd 2475 . . . . . . . . . . . . . . . 16
221220adantr 465 . . . . . . . . . . . . . . 15 ..^
222215simprd 463 . . . . . . . . . . . . . . . 16 ..^ ..^
223 fourierdlem91.l . . . . . . . . . . . . . . . . 17 ..^ lim
224 elex 3127 . . . . . . . . . . . . . . . . 17 lim
225215, 223, 2243syl 20 . . . . . . . . . . . . . . . 16 ..^
226208fvmpt2 5964 . . . . . . . . . . . . . . . 16 ..^
227222, 225, 226syl2anc 661 . . . . . . . . . . . . . . 15 ..^
228221, 227eqtrd 2508 . . . . . . . . . . . . . 14 ..^
2292283adant2 1015 . . . . . . . . . . . . 13 ..^ lim ..^
230199, 191oveq12d 6313 . . . . . . . . . . . . . . 15 lim lim
231230eqcomd 2475 . . . . . . . . . . . . . 14 lim lim
2322313ad2ant1 1017 . . . . . . . . . . . . 13 ..^ lim ..^ lim lim
233229, 232eleq12d 2549 . . . . . . . . . . . 12 ..^ lim ..^ lim lim
234218, 233mpbird 232 . . . . . . . . . . 11 ..^ lim ..^ lim
2352343exp 1195 . . . . . . . . . 10 ..^ lim ..^ lim
236223a1ii 27 . . . . . . . . . 10 ..^ lim ..^ lim
237235, 236impbid 191 . . . . . . . . 9 ..^ lim ..^ lim
238206, 214, 237, 223vtoclgf 3174 . . . . . . . 8 ..^ ..^ lim
239188, 195, 238sylc 60 . . . . . . 7 lim
24050simprd 463 . . . . . . . . . . . 12 ..^
241240simprd 463 . . . . . . . . . . 11 ..^
242 fveq2 5872 . . . . . . . . . . . . 13
243 oveq1 6302 . . . . . . . . . . . . . 14
244243fveq2d 5876 . . . . . . . . . . . . 13
245242, 244breq12d 4466 . . . . . . . . . . . 12
246245rspccva 3218 . . . . . . . . . . 11 ..^ ..^
247241, 54, 246syl2anc 661 . . . . . . . . . 10
248 posdif 10057 . . . . . . . . . . 11
24984, 57, 248syl2anc 661 . . . . . . . . . 10
250247, 249mpbid 210 . . . . . . . . 9
251 simpr 461 . . . . . . . . . . . 12 ..^ ..^
252 eleq1 2539 . . . . . . . . . . . . . . 15 ..^ ..^
253252anbi2d 703 . . . . . . . . . . . . . 14 ..^ ..^
254 oveq1 6302 . . . . . . . . . . . . . . . . . 18
255254fveq2d 5876 . . . . . . . . . . . . . . . . 17
256255fveq2d 5876 . . . . . . . . . . . . . . . 16
257 fveq2 5872 . . . . . . . . . . . . . . . . . 18
258257fveq2d 5876 . . . . . . . . . . . . . . . . 17
259258fveq2d 5876 . . . . . . . . . . . . . . . 16
260256, 259oveq12d 6313 . . . . . . . . . . . . . . 15
261255, 257oveq12d 6313 . . . . . . . . . . . . . . 15
262260, 261eqeq12d 2489 . . . . . . . . . . . . . 14
263253, 262imbi12d 320 . . . . . . . . . . . . 13 ..^ ..^
26414oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . 23
265264oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . 22
266265eleq1i 2544 . . . . . . . . . . . . . . . . . . . . 21
267266rexbii 2969 . . . . . . . . . . . . . . . . . . . 20
268267rgenw 2828 . . . . . . . . . . . . . . . . . . 19
269 rabbi 3045 . . . . . . . . . . . . . . . . . . 19
270268, 269mpbi 208 . . . . . . . . . . . . . . . . . 18
271270uneq2i 3660 . . . . . . . . . . . . . . . . 17
272271fveq2i 5875 . . . . . . . . . . . . . . . 16
273272oveq1i 6305 . . . . . . . . . . . . . . 15
27436, 273eqtri 2496 . . . . . . . . . . . . . 14
275 isoeq5 6218 . . . . . . . . . . . . . . . . . 18
276271, 275ax-mp 5 . . . . . . . . . . . . . . . . 17
277276ax-gen 1601 . . . . . . . . . . . . . . . 16
278 iotabi 5566 . . . . . . . . . . . . . . . 16
279277, 278ax-mp 5 . . . . . . . . . . . . . . 15
28043, 279eqtri 2496 . . . . . . . . . . . . . 14
281 eqid 2467 . . . . . . . . . . . . . 14
28215, 14, 16, 17, 18, 19, 26, 274, 280, 65, 78, 281fourierdlem65 31795 . . . . . . . . . . . . 13 ..^
283263, 282vtoclg 3176 . . . . . . . . . . . 12 ..^ ..^
284251, 283mpcom 36 . . . . . . . . . . 11 ..^
28595, 54, 284syl2anc 661 . . . . . . . . . 10
286285eqcomd 2475 . . . . . . . . 9
287250, 286breqtrd 4477 . . . . . . . 8
28888, 68posdifd 10151 . . . . . . . 8
289287, 288mpbird 232 . . . . . . 7
290259, 256oveq12d 6313 . . . . . . . . . . . 12
291257fveq2d 5876 . . . . . . . . . . . . . 14
292291fveq2d 5876 . . . . . . . . . . . . 13
293291oveq1d 6310 . . . . . . . . . . . . . 14
294293fveq2d 5876 . . . . . . . . . . . . 13
295292, 294oveq12d 6313 . . . . . . . . . . . 12
296290, 295sseq12d 3538 . . . . . . . . . . 11
297253, 296imbi12d 320 . . . . . . . . . 10 ..^ ..^
29833, 31eqtri 2496 . . . . . . . . . . 11
299 eqid 2467 . . . . . . . . . . 11
30014, 15, 16, 17, 18, 21, 25, 26, 298, 32, 37, 65, 78, 299, 175fourierdlem79 31809 . . . . . . . . . 10 ..^
301297, 300vtoclg 3176 . . . . . . . . 9 ..^ ..^
302251, 301mpcom 36 . . . . . . . 8 ..^
30395, 54, 302syl2anc 661 . . . . . . 7
304 eqid 2467 . . . . . . 7
305 eqid 2467 . . . . . . 7 fldt fldt
306180, 183, 194, 205, 239, 88, 68, 289, 303, 304, 305fourierdlem33 31763 . . . . . 6 lim
307 resabs1 5308 . . . . . . . 8
308303, 307syl 16 . . . . . . 7
309308oveq1d 6310 . . . . . 6 lim lim
310306, 309eleqtrd 2557 . . . . 5 lim
3115, 7, 11, 71, 72, 91, 162, 310limcperiod 31493 . . . 4 lim
31213oveq2i 6306 . . . . . . 7
313312a1i 11 . . . . . 6
314119, 120pncan3d 9945 . . . . . 6
315313, 314eqtrd 2508 . . . . 5
316315oveq2d 6311 . . . 4 lim lim
317311, 316eleqtrd 2557 . . 3