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

Theorem fourierdlem93 38175
 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 . . . . . . . 8
2 fourierdlem93.3 . . . . . . . . 9
3 fourierdlem93.1 . . . . . . . . . 10 ..^
43fourierdlem2 38083 . . . . . . . . 9 ..^
52, 4syl 17 . . . . . . . 8 ..^
61, 5mpbid 215 . . . . . . 7 ..^
76simprd 470 . . . . . 6 ..^
87simplld 769 . . . . 5
98eqcomd 2477 . . . 4
107simplrd 771 . . . . 5
1110eqcomd 2477 . . . 4
129, 11oveq12d 6326 . . 3
1312itgeq1d 37930 . 2
14 0zd 10973 . . 3
15 nnuz 11218 . . . . 5
162, 15syl6eleq 2559 . . . 4
17 1e0p1 11102 . . . . . 6
1817a1i 11 . . . . 5
1918fveq2d 5883 . . . 4
2016, 19eleqtrd 2551 . . 3
213, 2, 1fourierdlem15 38096 . . . 4
22 pire 23492 . . . . . . 7
2322renegcli 9955 . . . . . 6
24 iccssre 11741 . . . . . 6
2523, 22, 24mp2an 686 . . . . 5
2625a1i 11 . . . 4
2721, 26fssd 5750 . . 3
287simprd 470 . . . 4 ..^
2928r19.21bi 2776 . . 3 ..^
30 fourierdlem93.6 . . . . 5
3130adantr 472 . . . 4
32 simpr 468 . . . . 5
3312eqcomd 2477 . . . . . 6
3433adantr 472 . . . . 5
3532, 34eleqtrd 2551 . . . 4
3631, 35ffvelrnd 6038 . . 3
3727adantr 472 . . . . 5 ..^
38 elfzofz 11962 . . . . . 6 ..^
3938adantl 473 . . . . 5 ..^
4037, 39ffvelrnd 6038 . . . 4 ..^
41 fzofzp1 12037 . . . . . 6 ..^
4241adantl 473 . . . . 5 ..^
4337, 42ffvelrnd 6038 . . . 4 ..^
4430feqmptd 5932 . . . . . . . . . 10
4544adantr 472 . . . . . . . . 9 ..^
4645reseq1d 5110 . . . . . . . 8 ..^
47 ioossicc 11745 . . . . . . . . . . 11
4847a1i 11 . . . . . . . . . 10 ..^
4923rexri 9711 . . . . . . . . . . . . . 14
5049a1i 11 . . . . . . . . . . . . 13 ..^
5122rexri 9711 . . . . . . . . . . . . . 14
5251a1i 11 . . . . . . . . . . . . 13 ..^
5321ad2antrr 740 . . . . . . . . . . . . 13 ..^
54 simplr 770 . . . . . . . . . . . . 13 ..^ ..^
55 simpr 468 . . . . . . . . . . . . 13 ..^
5650, 52, 53, 54, 55fourierdlem1 38082 . . . . . . . . . . . 12 ..^
5756ralrimiva 2809 . . . . . . . . . . 11 ..^
58 dfss3 3408 . . . . . . . . . . 11
5957, 58sylibr 217 . . . . . . . . . 10 ..^
6048, 59sstrd 3428 . . . . . . . . 9 ..^
6160resmptd 5162 . . . . . . . 8 ..^
6246, 61eqtrd 2505 . . . . . . 7 ..^
6362eqcomd 2477 . . . . . 6 ..^
64 fourierdlem93.7 . . . . . 6 ..^
6563, 64eqeltrd 2549 . . . . 5 ..^
66 fourierdlem93.9 . . . . . 6 ..^ lim
6762oveq1d 6323 . . . . . 6 ..^ lim lim
6866, 67eleqtrd 2551 . . . . 5 ..^ lim
69 fourierdlem93.8 . . . . . 6 ..^ lim
7062oveq1d 6323 . . . . . 6 ..^ lim lim
7169, 70eleqtrd 2551 . . . . 5 ..^ lim
7240, 43, 65, 68, 71iblcncfioo 37952 . . . 4 ..^
7330ad2antrr 740 . . . . 5 ..^
7473, 56ffvelrnd 6038 . . . 4 ..^
7540, 43, 72, 74ibliooicc 37945 . . 3 ..^
7614, 20, 27, 29, 36, 75itgspltprt 37953 . 2 ..^
77 fvres 5893 . . . . . . . 8
7877eqcomd 2477 . . . . . . 7
7978adantl 473 . . . . . 6 ..^
8079itgeq2dv 22818 . . . . 5 ..^
81 eqid 2471 . . . . . 6
8230adantr 472 . . . . . . 7 ..^
8382, 59fssresd 5762 . . . . . 6 ..^
8448resabs1d 5140 . . . . . . 7 ..^
8584, 64eqeltrd 2549 . . . . . 6 ..^
8684oveq1d 6323 . . . . . . . 8 ..^ lim lim
8740, 43, 29, 83limcicciooub 37814 . . . . . . . 8 ..^ lim lim
8886, 87eqtr3d 2507 . . . . . . 7 ..^ lim lim
8966, 88eleqtrd 2551 . . . . . 6 ..^ lim
9084eqcomd 2477 . . . . . . . . 9 ..^
9190oveq1d 6323 . . . . . . . 8 ..^ lim lim
9240, 43, 29, 83limciccioolb 37798 . . . . . . . 8 ..^ lim lim
9391, 92eqtrd 2505 . . . . . . 7 ..^ lim lim
9469, 93eleqtrd 2551 . . . . . 6 ..^ lim
95 fourierdlem93.5 . . . . . . 7
9695adantr 472 . . . . . 6 ..^
9781, 40, 43, 29, 83, 85, 89, 94, 96fourierdlem82 38164 . . . . 5 ..^
9840adantr 472 . . . . . . . 8 ..^
9943adantr 472 . . . . . . . 8 ..^
10095ad2antrr 740 . . . . . . . . 9 ..^
10198, 100resubcld 10068 . . . . . . . . . 10 ..^
10299, 100resubcld 10068 . . . . . . . . . 10 ..^
103 simpr 468 . . . . . . . . . 10 ..^
104 eliccre 37699 . . . . . . . . . 10
105101, 102, 103, 104syl3anc 1292 . . . . . . . . 9 ..^
106100, 105readdcld 9688 . . . . . . . 8 ..^
107 elicc2 11724 . . . . . . . . . . . 12
108101, 102, 107syl2anc 673 . . . . . . . . . . 11 ..^
109103, 108mpbid 215 . . . . . . . . . 10 ..^
110109simp2d 1043 . . . . . . . . 9 ..^
11198, 100, 105lesubadd2d 10233 . . . . . . . . 9 ..^
112110, 111mpbid 215 . . . . . . . 8 ..^
113109simp3d 1044 . . . . . . . . 9 ..^
114100, 105, 99leaddsub2d 10236 . . . . . . . . 9 ..^
115113, 114mpbird 240 . . . . . . . 8 ..^
11698, 99, 106, 112, 115eliccd 37697 . . . . . . 7 ..^
117 fvres 5893 . . . . . . 7
118116, 117syl 17 . . . . . 6 ..^
119118itgeq2dv 22818 . . . . 5 ..^
12080, 97, 1193eqtrd 2509 . . . 4 ..^
121120sumeq2dv 13846 . . 3 ..^ ..^
122 oveq2 6316 . . . . . . 7
123122fveq2d 5883 . . . . . 6
124123cbvitgv 22813 . . . . 5
125124a1i 11 . . . 4
126 fourierdlem93.2 . . . . . . . . 9
127126a1i 11 . . . . . . . 8
128 fveq2 5879 . . . . . . . . . 10
129128oveq1d 6323 . . . . . . . . 9
130129adantl 473 . . . . . . . 8
1312nnzd 11062 . . . . . . . . . 10
13214, 131, 143jca 1210 . . . . . . . . 9
133 0le0 10721 . . . . . . . . . . 11
134133a1i 11 . . . . . . . . . 10
135 0red 9662 . . . . . . . . . . 11
1362nnred 10646 . . . . . . . . . . 11
1372nngt0d 10675 . . . . . . . . . . 11
138135, 136, 137ltled 9800 . . . . . . . . . 10
139134, 138jca 541 . . . . . . . . 9
140 elfz2 11817 . . . . . . . . 9
141132, 139, 140sylanbrc 677 . . . . . . . 8
1428, 23syl6eqel 2557 . . . . . . . . 9
143142, 95resubcld 10068 . . . . . . . 8
144127, 130, 141, 143fvmptd 5969 . . . . . . 7
1458oveq1d 6323 . . . . . . 7
146144, 145eqtr2d 2506 . . . . . 6
147 fveq2 5879 . . . . . . . . . 10
148147oveq1d 6323 . . . . . . . . 9
149148adantl 473 . . . . . . . 8
15014, 131, 1313jca 1210 . . . . . . . . 9
151136leidd 10201 . . . . . . . . . 10
152138, 151jca 541 . . . . . . . . 9
153 elfz2 11817 . . . . . . . . 9
154150, 152, 153sylanbrc 677 . . . . . . . 8
15510, 22syl6eqel 2557 . . . . . . . . 9
156155, 95resubcld 10068 . . . . . . . 8
157127, 149, 154, 156fvmptd 5969 . . . . . . 7
15810oveq1d 6323 . . . . . . 7
159157, 158eqtr2d 2506 . . . . . 6
160146, 159oveq12d 6326 . . . . 5
161160itgeq1d 37930 . . . 4
16227fnvinran 37398 . . . . . . . 8
16395adantr 472 . . . . . . . 8
164162, 163resubcld 10068 . . . . . . 7
165164, 126fmptd 6061 . . . . . 6
16640, 43, 96, 29ltsub1dd 10246 . . . . . . 7 ..^
16739, 164syldan 478 . . . . . . . 8 ..^
168126fvmpt2 5972 . . . . . . . 8
16939, 167, 168syl2anc 673 . . . . . . 7 ..^
170 fveq2 5879 . . . . . . . . . . . 12
171170oveq1d 6323 . . . . . . . . . . 11
172171cbvmptv 4488 . . . . . . . . . 10
173126, 172eqtri 2493 . . . . . . . . 9
174173a1i 11 . . . . . . . 8 ..^
175 fveq2 5879 . . . . . . . . . 10
176175oveq1d 6323 . . . . . . . . 9
177176adantl 473 . . . . . . . 8 ..^
17843, 96resubcld 10068 . . . . . . . 8 ..^
179174, 177, 42, 178fvmptd 5969 . . . . . . 7 ..^
180166, 169, 1793brtr4d 4426 . . . . . 6 ..^
181 frn 5747 . . . . . . . . 9
18230, 181syl 17 . . . . . . . 8
183182adantr 472 . . . . . . 7
184 ffun 5742 . . . . . . . . . 10
18530, 184syl 17 . . . . . . . . 9
186185adantr 472 . . . . . . . 8
18723a1i 11 . . . . . . . . . 10
18822a1i 11 . . . . . . . . . 10
18995adantr 472 . . . . . . . . . . 11
190144, 143eqeltrd 2549 . . . . . . . . . . . . 13
191190adantr 472 . . . . . . . . . . . 12
192157, 156eqeltrd 2549 . . . . . . . . . . . . 13
193192adantr 472 . . . . . . . . . . . 12
194 simpr 468 . . . . . . . . . . . 12
195 eliccre 37699 . . . . . . . . . . . 12
196191, 193, 194, 195syl3anc 1292 . . . . . . . . . . 11
197189, 196readdcld 9688 . . . . . . . . . 10
198128adantl 473 . . . . . . . . . . . . . . . 16
199198oveq1d 6323 . . . . . . . . . . . . . . 15
200127, 199, 141, 143fvmptd 5969 . . . . . . . . . . . . . 14
201200oveq2d 6324 . . . . . . . . . . . . 13
20295recnd 9687 . . . . . . . . . . . . . 14
203142recnd 9687 . . . . . . . . . . . . . 14
204202, 203pncan3d 10008 . . . . . . . . . . . . 13
205201, 204, 83eqtrrd 2510 . . . . . . . . . . . 12
206205adantr 472 . . . . . . . . . . 11
207 elicc2 11724 . . . . . . . . . . . . . . 15
208191, 193, 207syl2anc 673 . . . . . . . . . . . . . 14
209194, 208mpbid 215 . . . . . . . . . . . . 13
210209simp2d 1043 . . . . . . . . . . . 12
211191, 196, 189, 210leadd2dd 10249 . . . . . . . . . . 11
212206, 211eqbrtrd 4416 . . . . . . . . . 10
213209simp3d 1044 . . . . . . . . . . . 12
214196, 193, 189, 213leadd2dd 10249 . . . . . . . . . . 11
215157oveq2d 6324 . . . . . . . . . . . . 13
216155recnd 9687 . . . . . . . . . . . . . 14
217202, 216pncan3d 10008 . . . . . . . . . . . . 13
218215, 217, 103eqtrrd 2510 . . . . . . . . . . . 12
219218adantr 472 . . . . . . . . . . 11
220214, 219breqtrrd 4422 . . . . . . . . . 10
221187, 188, 197, 212, 220eliccd 37697 . . . . . . . . 9
222 fdm 5745 . . . . . . . . . . . 12
22330, 222syl 17 . . . . . . . . . . 11
224223eqcomd 2477 . . . . . . . . . 10
225224adantr 472 . . . . . . . . 9
226221, 225eleqtrd 2551 . . . . . . . 8
227 fvelrn 6030 . . . . . . . 8
228186, 226, 227syl2anc 673 . . . . . . 7
229183, 228sseldd 3419 . . . . . 6
230169, 167eqeltrd 2549 . . . . . . 7 ..^
231179, 178eqeltrd 2549 . . . . . . 7 ..^
23282, 60fssresd 5762 . . . . . . . . . . 11 ..^
23340rexrd 9708 . . . . . . . . . . . . . 14 ..^
234233adantr 472 . . . . . . . . . . . . 13 ..^
23543rexrd 9708 . . . . . . . . . . . . . 14 ..^
236235adantr 472 . . . . . . . . . . . . 13 ..^
23795ad2antrr 740 . . . . . . . . . . . . . 14 ..^
238 elioore 11691 . . . . . . . . . . . . . . 15
239238adantl 473 . . . . . . . . . . . . . 14 ..^
240237, 239readdcld 9688 . . . . . . . . . . . . 13 ..^
241169oveq2d 6324 . . . . . . . . . . . . . . . 16 ..^
242202adantr 472 . . . . . . . . . . . . . . . . 17 ..^
24340recnd 9687 . . . . . . . . . . . . . . . . 17 ..^
244242, 243pncan3d 10008 . . . . . . . . . . . . . . . 16 ..^
245 eqidd 2472 . . . . . . . . . . . . . . . 16 ..^
246241, 244, 2453eqtrrd 2510 . . . . . . . . . . . . . . 15 ..^
247246adantr 472 . . . . . . . . . . . . . 14 ..^
248230adantr 472 . . . . . . . . . . . . . . 15 ..^
249 simpr 468 . . . . . . . . . . . . . . . . 17 ..^
250248rexrd 9708 . . . . . . . . . . . . . . . . . 18 ..^
251231rexrd 9708 . . . . . . . . . . . . . . . . . . 19 ..^
252251adantr 472 . . . . . . . . . . . . . . . . . 18 ..^
253 elioo2 11702 . . . . . . . . . . . . . . . . . 18
254250, 252, 253syl2anc 673 . . . . . . . . . . . . . . . . 17 ..^
255249, 254mpbid 215 . . . . . . . . . . . . . . . 16 ..^
256255simp2d 1043 . . . . . . . . . . . . . . 15 ..^
257248, 239, 237, 256ltadd2dd 9811 . . . . . . . . . . . . . 14 ..^
258247, 257eqbrtrd 4416 . . . . . . . . . . . . 13 ..^
259231adantr 472 . . . . . . . . . . . . . . 15 ..^
260255simp3d 1044 . . . . . . . . . . . . . . 15 ..^
261239, 259, 237, 260ltadd2dd 9811 . . . . . . . . . . . . . 14 ..^
262179oveq2d 6324 . . . . . . . . . . . . . . . 16 ..^
26343recnd 9687 . . . . . . . . . . . . . . . . 17 ..^
264242, 263pncan3d 10008 . . . . . . . . . . . . . . . 16 ..^
265262, 264eqtrd 2505 . . . . . . . . . . . . . . 15 ..^
266265adantr 472 . . . . . . . . . . . . . 14 ..^
267261, 266breqtrd 4420 . . . . . . . . . . . . 13 ..^
268234, 236, 240, 258, 267eliood 37691 . . . . . . . . . . . 12 ..^
269 eqid 2471 . . . . . . . . . . . 12
270268, 269fmptd 6061 . . . . . . . . . . 11 ..^
271 fcompt 6075 . . . . . . . . . . 11
272232, 270, 271syl2anc 673 . . . . . . . . . 10 ..^
273 oveq2 6316 . . . . . . . . . . . . . . . 16
274273cbvmptv 4488 . . . . . . . . . . . . . . 15
275274fveq1i 5880 . . . . . . . . . . . . . 14
276275fveq2i 5882 . . . . . . . . . . . . 13
277276mpteq2i 4479 . . . . . . . . . . . 12
278277a1i 11 . . . . . . . . . . 11 ..^
279 fveq2 5879 . . . . . . . . . . . . . 14
280279fveq2d 5883 . . . . . . . . . . . . 13
281280cbvmptv 4488 . . . . . . . . . . . 12
282281a1i 11 . . . . . . . . . . 11 ..^
283 eqidd 2472 . . . . . . . . . . . . . . 15 ..^
284 oveq2 6316 . . . . . . . . . . . . . . . 16
285284adantl 473 . . . . . . . . . . . . . . 15 ..^
286283, 285, 249, 240fvmptd 5969 . . . . . . . . . . . . . 14 ..^
287286fveq2d 5883 . . . . . . . . . . . . 13 ..^
288 fvres 5893 . . . . . . . . . . . . . 14
289268, 288syl 17 . . . . . . . . . . . . 13 ..^
290287, 289eqtrd 2505 . . . . . . . . . . . 12 ..^
291290mpteq2dva 4482 . . . . . . . . . . 11 ..^
292278, 282, 2913eqtrd 2509 . . . . . . . . . 10 ..^
293272, 292eqtr2d 2506 . . . . . . . . 9 ..^
294 eqid 2471 . . . . . . . . . . 11
295 ssid 3437 . . . . . . . . . . . . . . 15
296295a1i 11 . . . . . . . . . . . . . 14
297 id 22 . . . . . . . . . . . . . 14
298296, 297, 296constcncfg 37845 . . . . . . . . . . . . 13
299 cncfmptid 22022 . . . . . . . . . . . . . . 15
300295, 295, 299mp2an 686 . . . . . . . . . . . . . 14
301300a1i 11 . . . . . . . . . . . . 13
302298, 301addcncf 37847 . . . . . . . . . . . 12
303242, 302syl 17 . . . . . . . . . . 11 ..^
304 ioosscn 37687 . . . . . . . . . . . 12
305304a1i 11 . . . . . . . . . . 11 ..^
306 ioosscn 37687 . . . . . . . . . . . 12
307306a1i 11 . . . . . . . . . . 11 ..^
308294, 303, 305, 307, 268cncfmptssg 37844 . . . . . . . . . 10 ..^
309308, 64cncfco 22017 . . . . . . . . 9 ..^
310293, 309eqeltrd 2549 . . . . . . . 8 ..^
311233adantr 472 . . . . . . . . . . . . . . 15 ..^
312235adantr 472 . . . . . . . . . . . . . . 15 ..^
313 simpr 468 . . . . . . . . . . . . . . . . 17 ..^
314 vex 3034 . . . . . . . . . . . . . . . . . 18
315269elrnmpt 5087 . . . . . . . . . . . . . . . . . 18
316314, 315ax-mp 5 . . . . . . . . . . . . . . . . 17
317313, 316sylib 201 . . . . . . . . . . . . . . . 16 ..^
318 nfv 1769 . . . . . . . . . . . . . . . . . 18 ..^
319 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . 20
320319nfrn 5083 . . . . . . . . . . . . . . . . . . 19
321320nfcri 2606 . . . . . . . . . . . . . . . . . 18
322318, 321nfan 2031 . . . . . . . . . . . . . . . . 17 ..^
323 nfv 1769 . . . . . . . . . . . . . . . . 17
324 simp3 1032 . . . . . . . . . . . . . . . . . . . 20
325953ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . 21
3262383ad2ant2 1052 . . . . . . . . . . . . . . . . . . . . 21
327325, 326readdcld 9688 . . . . . . . . . . . . . . . . . . . 20
328324, 327eqeltrd 2549 . . . . . . . . . . . . . . . . . . 19
3293283exp 1230 . . . . . . . . . . . . . . . . . 18
330329ad2antrr 740 . . . . . . . . . . . . . . . . 17 ..^
331322, 323, 330rexlimd 2866 . . . . . . . . . . . . . . . 16 ..^
332317, 331mpd 15 . . . . . . . . . . . . . . 15 ..^
333 nfv 1769 . . . . . . . . . . . . . . . . 17
3342583adant3 1050 . . . . . . . . . . . . . . . . . . . 20 ..^
335 simp3 1032 . . . . . . . . . . . . . . . . . . . 20 ..^
336334, 335breqtrrd 4422 . . . . . . . . . . . . . . . . . . 19 ..^
3373363exp 1230 . . . . . . . . . . . . . . . . . 18 ..^
338337adantr 472 . . . . . . . . . . . . . . . . 17 ..^
339322, 333, 338rexlimd 2866 . . . . . . . . . . . . . . . 16 ..^
340317, 339mpd 15 . . . . . . . . . . . . . . 15 ..^
341 nfv 1769 . . . . . . . . . . . . . . . . 17
3422673adant3 1050 . . . . . . . . . . . . . . . . . . . 20 ..^
343335, 342eqbrtrd 4416 . . . . . . . . . . . . . . . . . . 19 ..^
3443433exp 1230 . . . . . . . . . . . . . . . . . 18 ..^
345344adantr 472 . . . . . . . . . . . . . . . . 17 ..^
346322, 341, 345rexlimd 2866 . . . . . . . . . . . . . . . 16 ..^
347317, 346mpd 15 . . . . . . . . . . . . . . 15 ..^
348311, 312, 332, 340, 347eliood 37691 . . . . . . . . . . . . . 14 ..^
349223ineq2d 3625 . . . . . . . . . . . . . . . . 17
350349adantr 472 . . . . . . . . . . . . . . . 16 ..^
351 dmres 5131 . . . . . . . . . . . . . . . . 17
352351a1i 11 . . . . . . . . . . . . . . . 16 ..^
353 dfss 3405 . . . . . . . . . . . . . . . . 17
35460, 353sylib 201 . . . . . . . . . . . . . . . 16 ..^
355350, 352, 3543eqtr4d 2515 . . . . . . . . . . . . . . 15 ..^
356355adantr 472 . . . . . . . . . . . . . 14 ..^
357348, 356eleqtrrd 2552 . . . . . . . . . . . . 13 ..^