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

Theorem fourierdlem93 31823
 Description: Integral by substitution (the domain is shifted by ) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem93.1 ..^
fourierdlem93.2
fourierdlem93.3
fourierdlem93.4
fourierdlem93.5
fourierdlem93.6
fourierdlem93.7 ..^
fourierdlem93.8 ..^ lim
fourierdlem93.9 ..^ lim
Assertion
Ref Expression
fourierdlem93
Distinct variable groups:   ,,,   ,,,   ,   ,,,   ,,   ,,   ,,   ,   ,,,   ,,,
Allowed substitution hints:   (,)   (,,,,)   ()   (,,,)   (,)   (,)   (,,,)   (,)

Proof of Theorem fourierdlem93
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem93.4 . . . . . . . . . . 11
2 fourierdlem93.3 . . . . . . . . . . . 12
3 fourierdlem93.1 . . . . . . . . . . . . 13 ..^
43fourierdlem2 31732 . . . . . . . . . . . 12 ..^
52, 4syl 16 . . . . . . . . . . 11 ..^
61, 5mpbid 210 . . . . . . . . . 10 ..^
76simprd 463 . . . . . . . . 9 ..^
87simpld 459 . . . . . . . 8
98simpld 459 . . . . . . 7
108simprd 463 . . . . . . 7
117simprd 463 . . . . . . 7 ..^
129, 10, 113jca 1176 . . . . . 6 ..^
1312simp1d 1008 . . . . 5
1413eqcomd 2475 . . . 4
1512simp2d 1009 . . . . 5
1615eqcomd 2475 . . . 4
1714, 16oveq12d 6313 . . 3
18 itgeq1 22047 . . 3
1917, 18syl 16 . 2
20 0z 10887 . . . 4
2120a1i 11 . . 3
22 nnuz 11129 . . . . 5
232, 22syl6eleq 2565 . . . 4
24 1e0p1 11016 . . . . . 6
2524a1i 11 . . . . 5
2625fveq2d 5876 . . . 4
2723, 26eleqtrd 2557 . . 3
283, 2, 1fourierdlem15 31745 . . . . 5
29 pire 22718 . . . . . . . . 9
3029renegcli 9892 . . . . . . . 8
3130, 29pm3.2i 455 . . . . . . 7
32 iccssre 11618 . . . . . . 7
3331, 32ax-mp 5 . . . . . 6
3433a1i 11 . . . . 5
3528, 34jca 532 . . . 4
36 fss 5745 . . . 4
3735, 36syl 16 . . 3
3811r19.21bi 2836 . . 3 ..^
39 fourierdlem93.6 . . . . . 6
4039adantr 465 . . . . 5
41 simpr 461 . . . . . 6
4217eqcomd 2475 . . . . . . 7
4342adantr 465 . . . . . 6
4441, 43eleqtrd 2557 . . . . 5
4540, 44jca 532 . . . 4
46 ffvelrn 6030 . . . 4
4745, 46syl 16 . . 3
48 iooinlbub 31421 . . . . . . 7
4948a1i 11 . . . . . 6 ..^
5049fveq2d 5876 . . . . 5 ..^
51 ovol0 21772 . . . . . 6
5251a1i 11 . . . . 5 ..^
5350, 52eqtrd 2508 . . . 4 ..^
5437adantr 465 . . . . . . . . . 10 ..^
55 elfzofz 11823 . . . . . . . . . . 11 ..^
5655adantl 466 . . . . . . . . . 10 ..^
5754, 56jca 532 . . . . . . . . 9 ..^
58 ffvelrn 6030 . . . . . . . . 9
5957, 58syl 16 . . . . . . . 8 ..^
6059rexrd 9655 . . . . . . 7 ..^
61 fzofzp1 11889 . . . . . . . . . . 11 ..^
6261adantl 466 . . . . . . . . . 10 ..^
6354, 62jca 532 . . . . . . . . 9 ..^
64 ffvelrn 6030 . . . . . . . . 9
6563, 64syl 16 . . . . . . . 8 ..^
6665rexrd 9655 . . . . . . 7 ..^
6759, 65, 38ltled 9744 . . . . . . 7 ..^
6860, 66, 673jca 1176 . . . . . 6 ..^
69 prunioo 11661 . . . . . 6
7068, 69syl 16 . . . . 5 ..^
7170eqcomd 2475 . . . 4 ..^
7239ad2antrr 725 . . . . . 6 ..^
7330rexri 9658 . . . . . . . 8
7473a1i 11 . . . . . . 7 ..^
7529rexri 9658 . . . . . . . 8
7675a1i 11 . . . . . . 7 ..^
7728ad2antrr 725 . . . . . . 7 ..^
78 simplr 754 . . . . . . 7 ..^ ..^
79 simpr 461 . . . . . . 7 ..^
8074, 76, 77, 78, 79fourierdlem1 31731 . . . . . 6 ..^
8172, 80jca 532 . . . . 5 ..^
8281, 46syl 16 . . . 4 ..^
8339feqmptd 5927 . . . . . . . . . 10
8483adantr 465 . . . . . . . . 9 ..^
8584reseq1d 5278 . . . . . . . 8 ..^
86 ioossicc 11622 . . . . . . . . . . 11
8786a1i 11 . . . . . . . . . 10 ..^
8880ralrimiva 2881 . . . . . . . . . . 11 ..^
89 dfss3 3499 . . . . . . . . . . 11
9088, 89sylibr 212 . . . . . . . . . 10 ..^
9187, 90sstrd 3519 . . . . . . . . 9 ..^
92 resmpt 5329 . . . . . . . . 9
9391, 92syl 16 . . . . . . . 8 ..^
94 eqidd 2468 . . . . . . . 8 ..^
9585, 93, 943eqtrd 2512 . . . . . . 7 ..^
9695eqcomd 2475 . . . . . 6 ..^
97 fourierdlem93.7 . . . . . 6 ..^
9896, 97eqeltrd 2555 . . . . 5 ..^
99 fourierdlem93.9 . . . . . 6 ..^ lim
10095oveq1d 6310 . . . . . 6 ..^ lim lim
10199, 100eleqtrd 2557 . . . . 5 ..^ lim
102 fourierdlem93.8 . . . . . 6 ..^ lim
10395oveq1d 6310 . . . . . 6 ..^ lim lim
104102, 103eleqtrd 2557 . . . . 5 ..^ lim
10559, 65, 98, 101, 104iblcncfioo 31619 . . . 4 ..^
10659, 65jca 532 . . . . . . 7 ..^
107 prssg 4188 . . . . . . . 8
108106, 107syl 16 . . . . . . 7 ..^
109106, 108mpbid 210 . . . . . 6 ..^
110 prfi 7807 . . . . . . . . 9
111110a1i 11 . . . . . . . 8 ..^
112111, 109jca 532 . . . . . . 7 ..^
113 ovolfi 21773 . . . . . . 7
114112, 113syl 16 . . . . . 6 ..^
11539ad2antrr 725 . . . . . . . 8 ..^
116 simpl 457 . . . . . . . . . 10 ..^ ..^
117 lbicc2 11648 . . . . . . . . . . . . . . 15
11868, 117syl 16 . . . . . . . . . . . . . 14 ..^
119 ubicc2 11649 . . . . . . . . . . . . . . 15
12068, 119syl 16 . . . . . . . . . . . . . 14 ..^
121118, 120jca 532 . . . . . . . . . . . . 13 ..^
122 prssi 4189 . . . . . . . . . . . . 13
123121, 122syl 16 . . . . . . . . . . . 12 ..^
124123sseld 3508 . . . . . . . . . . 11 ..^
125124imp 429 . . . . . . . . . 10 ..^
126116, 125jca 532 . . . . . . . . 9 ..^ ..^
127126, 80syl 16 . . . . . . . 8 ..^
128115, 127jca 532 . . . . . . 7 ..^
129128, 46syl 16 . . . . . 6 ..^
130109, 114, 129itgvol0 31609 . . . . 5 ..^
131130simpld 459 . . . 4 ..^
13253, 71, 82, 105, 131iblsplit 31607 . . 3 ..^
13321, 27, 37, 38, 47, 132itgspltprt 31620 . 2 ..^
134 fvres 5886 . . . . . . . 8
135134eqcomd 2475 . . . . . . 7
136135adantl 466 . . . . . 6 ..^
137136itgeq2dv 22056 . . . . 5 ..^
138 eqid 2467 . . . . . 6
13939adantr 465 . . . . . . 7 ..^
140 fssres 5757 . . . . . . 7
141139, 90, 140syl2anc 661 . . . . . 6 ..^
142 resabs1 5308 . . . . . . . 8
14387, 142syl 16 . . . . . . 7 ..^
144143, 97eqeltrd 2555 . . . . . 6 ..^
145143oveq1d 6310 . . . . . . . . 9 ..^ lim lim
146145eqcomd 2475 . . . . . . . 8 ..^ lim lim
14759, 65, 38, 141limcicciooub 31502 . . . . . . . 8 ..^ lim lim
148146, 147eqtrd 2508 . . . . . . 7 ..^ lim lim
14999, 148eleqtrd 2557 . . . . . 6 ..^ lim
150143eqcomd 2475 . . . . . . . . 9 ..^
151150oveq1d 6310 . . . . . . . 8 ..^ lim lim
15259, 65, 38, 141limciccioolb 31486 . . . . . . . 8 ..^ lim lim
153 eqidd 2468 . . . . . . . 8 ..^ lim lim
154151, 152, 1533eqtrd 2512 . . . . . . 7 ..^ lim lim
155102, 154eleqtrd 2557 . . . . . 6 ..^ lim
156 fourierdlem93.5 . . . . . . 7
157156adantr 465 . . . . . 6 ..^
158138, 59, 65, 38, 141, 144, 149, 155, 157fourierdlem82 31812 . . . . 5 ..^
159157adantr 465 . . . . . . . . . 10 ..^
16059adantr 465 . . . . . . . . . . . 12 ..^
161160, 159resubcld 9999 . . . . . . . . . . 11 ..^
16265adantr 465 . . . . . . . . . . . 12 ..^
163162, 159resubcld 9999 . . . . . . . . . . 11 ..^
164 simpr 461 . . . . . . . . . . 11 ..^
165 eliccre 31427 . . . . . . . . . . 11
166161, 163, 164, 165syl3anc 1228 . . . . . . . . . 10 ..^
167159, 166readdcld 9635 . . . . . . . . 9 ..^
168 elicc2 11601 . . . . . . . . . . . . 13
169161, 163, 168syl2anc 661 . . . . . . . . . . . 12 ..^
170164, 169mpbid 210 . . . . . . . . . . 11 ..^
171170simp2d 1009 . . . . . . . . . 10 ..^
172 lesubadd2 10037 . . . . . . . . . . 11
173160, 159, 166, 172syl3anc 1228 . . . . . . . . . 10 ..^
174171, 173mpbid 210 . . . . . . . . 9 ..^
175170simp3d 1010 . . . . . . . . . 10 ..^
176 leaddsub2 10041 . . . . . . . . . . 11
177159, 166, 162, 176syl3anc 1228 . . . . . . . . . 10 ..^
178175, 177mpbird 232 . . . . . . . . 9 ..^
179167, 174, 1783jca 1176 . . . . . . . 8 ..^
180 elicc2 11601 . . . . . . . . 9
181160, 162, 180syl2anc 661 . . . . . . . 8 ..^
182179, 181mpbird 232 . . . . . . 7 ..^
183 fvres 5886 . . . . . . 7
184182, 183syl 16 . . . . . 6 ..^
185184itgeq2dv 22056 . . . . 5 ..^
186137, 158, 1853eqtrd 2512 . . . 4 ..^
187186sumeq2dv 13505 . . 3 ..^ ..^
188 oveq2 6303 . . . . . . 7
189188fveq2d 5876 . . . . . 6
190 nfcv 2629 . . . . . 6
191 nfcv 2629 . . . . . 6
192189, 190, 191cbvitg 22050 . . . . 5
193192a1i 11 . . . 4
194 fourierdlem93.2 . . . . . . . . 9
195194a1i 11 . . . . . . . 8
196 fveq2 5872 . . . . . . . . . 10
197196oveq1d 6310 . . . . . . . . 9
198197adantl 466 . . . . . . . 8
1992nnzd 10977 . . . . . . . . . . 11
20021, 199, 213jca 1176 . . . . . . . . . 10
201 0re 9608 . . . . . . . . . . . . 13
202201leidi 10099 . . . . . . . . . . . 12
203202a1i 11 . . . . . . . . . . 11
204201a1i 11 . . . . . . . . . . . 12
2052nnred 10563 . . . . . . . . . . . 12
2062nngt0d 10591 . . . . . . . . . . . 12
207204, 205, 206ltled 9744 . . . . . . . . . . 11
208203, 207jca 532 . . . . . . . . . 10
209200, 208jca 532 . . . . . . . . 9
210 elfz2 11691 . . . . . . . . 9
211209, 210sylibr 212 . . . . . . . 8
2129, 30syl6eqel 2563 . . . . . . . . 9
213212, 156resubcld 9999 . . . . . . . 8
214195, 198, 211, 213fvmptd 5962 . . . . . . 7
2159oveq1d 6310 . . . . . . 7
216214, 215eqtr2d 2509 . . . . . 6
217 fveq2 5872 . . . . . . . . . 10
218217oveq1d 6310 . . . . . . . . 9
219218adantl 466 . . . . . . . 8
22021, 199, 1993jca 1176 . . . . . . . . . 10
221205leidd 10131 . . . . . . . . . . 11
222207, 221jca 532 . . . . . . . . . 10
223220, 222jca 532 . . . . . . . . 9
224 elfz2 11691 . . . . . . . . 9
225223, 224sylibr 212 . . . . . . . 8
22610, 29syl6eqel 2563 . . . . . . . . 9
227226, 156resubcld 9999 . . . . . . . 8
228195, 219, 225, 227fvmptd 5962 . . . . . . 7
22910oveq1d 6310 . . . . . . 7
230228, 229eqtr2d 2509 . . . . . 6
231216, 230oveq12d 6313 . . . . 5
232 itgeq1 22047 . . . . 5
233231, 232syl 16 . . . 4
23437, 58sylan 471 . . . . . . . . 9
235156adantr 465 . . . . . . . . 9
236234, 235resubcld 9999 . . . . . . . 8
237236ralrimiva 2881 . . . . . . 7
238194fmpt 6053 . . . . . . 7
239237, 238sylib 196 . . . . . 6
24059, 65, 157ltsub1d 10173 . . . . . . . 8 ..^
24138, 240mpbid 210 . . . . . . 7 ..^
24256, 236syldan 470 . . . . . . . 8 ..^
243194fvmpt2 5964 . . . . . . . 8
24456, 242, 243syl2anc 661 . . . . . . 7 ..^
245 nfcv 2629 . . . . . . . . . . 11
246 nfcv 2629 . . . . . . . . . . 11
247 fveq2 5872 . . . . . . . . . . . 12
248247oveq1d 6310 . . . . . . . . . . 11
249245, 246, 248cbvmpt 4543 . . . . . . . . . 10
250194, 249eqtri 2496 . . . . . . . . 9
251250a1i 11 . . . . . . . 8 ..^
252 fveq2 5872 . . . . . . . . . 10
253252oveq1d 6310 . . . . . . . . 9
254253adantl 466 . . . . . . . 8 ..^
25565, 157resubcld 9999 . . . . . . . 8 ..^
256251, 254, 62, 255fvmptd 5962 . . . . . . 7 ..^
257241, 244, 2563brtr4d 4483 . . . . . 6 ..^
258 ffun 5739 . . . . . . . . . 10
25939, 258syl 16 . . . . . . . . 9
260259adantr 465 . . . . . . . 8
261156adantr 465 . . . . . . . . . . . 12
262214, 213eqeltrd 2555 . . . . . . . . . . . . . 14
263262adantr 465 . . . . . . . . . . . . 13
264228, 227eqeltrd 2555 . . . . . . . . . . . . . 14
265264adantr 465 . . . . . . . . . . . . 13
266 simpr 461 . . . . . . . . . . . . 13
267 eliccre 31427 . . . . . . . . . . . . 13
268263, 265, 266, 267syl3anc 1228 . . . . . . . . . . . 12
269261, 268readdcld 9635 . . . . . . . . . . 11
270 elicc2 11601 . . . . . . . . . . . . . . . 16
271263, 265, 270syl2anc 661 . . . . . . . . . . . . . . 15
272266, 271mpbid 210 . . . . . . . . . . . . . 14
273272simp2d 1009 . . . . . . . . . . . . 13
274263, 268, 2613jca 1176 . . . . . . . . . . . . . 14
275 leadd2 10033 . . . . . . . . . . . . . 14
276274, 275syl 16 . . . . . . . . . . . . 13
277273, 276mpbid 210 . . . . . . . . . . . 12
278196adantl 466 . . . . . . . . . . . . . . . . . 18
279278oveq1d 6310 . . . . . . . . . . . . . . . . 17
280195, 279, 211, 213fvmptd 5962 . . . . . . . . . . . . . . . 16
281280oveq2d 6311 . . . . . . . . . . . . . . 15
282 ax-resscn 9561 . . . . . . . . . . . . . . . . 17
283282, 156sseldi 3507 . . . . . . . . . . . . . . . 16
284282, 212sseldi 3507 . . . . . . . . . . . . . . . 16
285 pncan3 9840 . . . . . . . . . . . . . . . 16
286283, 284, 285syl2anc 661 . . . . . . . . . . . . . . 15
287281, 286, 93eqtrrd 2513 . . . . . . . . . . . . . 14
288287adantr 465 . . . . . . . . . . . . 13
289288breq1d 4463 . . . . . . . . . . . 12
290277, 289mpbird 232 . . . . . . . . . . 11
291272simp3d 1010 . . . . . . . . . . . . 13
292 leadd2 10033 . . . . . . . . . . . . . 14
293268, 265, 261, 292syl3anc 1228 . . . . . . . . . . . . 13
294291, 293mpbid 210 . . . . . . . . . . . 12
295228oveq2d 6311 . . . . . . . . . . . . . . 15
296282, 226sseldi 3507 . . . . . . . . . . . . . . . 16
297 pncan3 9840 . . . . . . . . . . . . . . . 16
298283, 296, 297syl2anc 661 . . . . . . . . . . . . . . 15
299295, 298, 103eqtrrd 2513 . . . . . . . . . . . . . 14
300299adantr 465 . . . . . . . . . . . . 13
301300breq2d 4465 . . . . . . . . . . . 12
302294, 301mpbird 232 . . . . . . . . . . 11
303269, 290, 3023jca 1176 . . . . . . . . . 10
30430a1i 11 . . . . . . . . . . 11
30529a1i 11 . . . . . . . . . . 11
306 elicc2 11601 . . . . . . . . . . 11
307304, 305, 306syl2anc 661 . . . . . . . . . 10
308303, 307mpbird 232 . . . . . . . . 9
309 fdm 5741 . . . . . . . . . . . 12
31039, 309syl 16 . . . . . . . . . . 11
311310eqcomd 2475 . . . . . . . . . 10
312311adantr 465 . . . . . . . . 9
313308, 312eleqtrd 2557 . . . . . . . 8
314 fvelrn 6025 . . . . . . . 8
315260, 313, 314syl2anc 661 . . . . . . 7
316 frn 5743 . . . . . . . . . 10
31739, 316syl 16 . . . . . . . . 9
318317adantr 465 . . . . . . . 8
319318sseld 3508 . . . . . . 7
320315, 319mpd 15 . . . . . 6
321244, 242eqeltrd 2555 . . . . . . . 8 ..^
322256, 255eqeltrd 2555 . . . . . . . 8 ..^
323 fssres 5757 . . . . . . . . . . . 12
324139, 91, 323syl2anc 661 . . . . . . . . . . 11 ..^
32560adantr 465 . . . . . . . . . . . . . . . 16 ..^
32666adantr 465 . . . . . . . . . . . . . . . 16 ..^
327157adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
328 elioore 11571 . . . . . . . . . . . . . . . . . . 19
329328adantl 466 . . . . . . . . . . . . . . . . . 18 ..^
330327, 329readdcld 9635 . . . . . . . . . . . . . . . . 17 ..^
331330rexrd 9655 . . . . . . . . . . . . . . . 16 ..^
332325, 326, 3313jca 1176 . . . . . . . . . . . . . . 15 ..^
333 simpr 461 . . . . . . . . . . . . . . . . . . . 20 ..^
334321adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
335334rexrd 9655 . . . . . . . . . . . . . . . . . . . . 21 ..^
336322rexrd 9655 . . . . . . . . . . . . . . . . . . . . . 22 ..^
337336adantr 465 . . . . . . . . . . . . . . . . . . . . 21 ..^
338 elioo2 11582 . . . . . . . . . . . . . . . . . . . . 21
339335, 337, 338syl2anc 661 . . . . . . . . . . . . . . . . . . . 20 ..^
340333, 339mpbid 210 . . . . . . . . . . . . . . . . . . 19 ..^
341340simp2d 1009 . . . . . . . . . . . . . . . . . 18 ..^
342334, 329, 327ltadd2d 9749 . . . . . . . . . . . . . . . . . 18 ..^
343341, 342mpbid 210 . . . . . . . . . . . . . . . . 17 ..^
344244oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20 ..^
345283adantr 465 . . . . . . . . . . . . . . . . . . . . 21 ..^
346282, 59sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21 ..^
347 pncan3 9840 . . . . . . . . . . . . . . . . . . . . 21
348345, 346, 347syl2anc 661 . . . . . . . . . . . . . . . . . . . 20 ..^
349 eqidd 2468 . . . . . . . . . . . . . . . . . . . 20 ..^
350344, 348, 3493eqtrrd 2513 . . . . . . . . . . . . . . . . . . 19 ..^
351350adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
352351breq1d 4463 . . . . . . . . . . . . . . . . 17 ..^
353343, 352mpbird 232 . . . . . . . . . . . . . . . 16 ..^
354340simp3d 1010 . . . . . . . . . . . . . . . . . 18 ..^
355322adantr 465 . . . . . . . . . . . . . . . . . . 19 ..^
356329, 355, 327ltadd2d 9749 . . . . . . . . . . . . . . . . . 18 ..^
357354, 356mpbid 210 . . . . . . . . . . . . . . . . 17 ..^
358256oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20 ..^
359282, 65sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21 ..^
360 pncan3 9840 . . . . . . . . . . . . . . . . . . . . 21
361345, 359, 360syl2anc 661 . . . . . . . . . . . . . . . . . . . 20 ..^
362 eqidd 2468 . . . . . . . . . . . . . . . . . . . 20 ..^
363358, 361, 3623eqtrd 2512 . . . . . . . . . . . . . . . . . . 19 ..^
364363adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
365364breq2d 4465 . . . . . . . . . . . . . . . . 17 ..^
366357, 365mpbid 210 . . . . . . . . . . . . . . . 16 ..^
367353, 366jca 532 . . . . . . . . . . . . . . 15 ..^
368332, 367jca 532 . . . . . . . . . . . . . 14 ..^
369 elioo3g 11570 . . . . . . . . . . . . . 14
370368, 369sylibr 212 . . . . . . . . . . . . 13 ..^
371370ralrimiva 2881 . . . . . . . . . . . 12 ..^
372 eqid 2467 . . . . . . . . . . . . 13
373372fmpt 6053 . . . . . . . . . . . 12
374371, 373sylib 196 . . . . . . . . . . 11 ..^
375 fcompt 6068 . . . . . . . . . . 11