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

Theorem fourierdlem113 38195
 Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem113.f
fourierdlem113.t
fourierdlem113.per
fourierdlem113.x
fourierdlem113.l lim
fourierdlem113.r lim
fourierdlem113.p ..^
fourierdlem113.m
fourierdlem113.q
fourierdlem113.dvcn ..^
fourierdlem113.dvlb ..^ lim
fourierdlem113.dvub ..^ lim
fourierdlem113.a
fourierdlem113.b
fourierdlem113.15
fourierdlem113.e
fourierdlem113.exq
Assertion
Ref Expression
fourierdlem113
Distinct variable groups:   ,   ,   ,   ,,,   ,,   ,,,   ,,,   ,,,   ,   ,,   ,,,   ,   ,,,   ,   ,,,
Allowed substitution hints:   ()   (,,)   (,,)   (,,,)   (,)   (,,,)   (,,)   ()   (,)

Proof of Theorem fourierdlem113
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem113.f . 2
2 oveq1 6315 . . . . . . 7
32eqeq1d 2473 . . . . . 6
4 oveq2 6316 . . . . . . . 8
54fveq2d 5883 . . . . . . 7
6 oveq1 6315 . . . . . . . . 9
76fveq2d 5883 . . . . . . . 8
87oveq2d 6324 . . . . . . 7
95, 8oveq12d 6326 . . . . . 6
103, 9ifbieq2d 3897 . . . . 5
1110cbvmptv 4488 . . . 4
12 oveq2 6316 . . . . . . . 8
1312oveq1d 6323 . . . . . . 7
1413oveq1d 6323 . . . . . 6
15 oveq1 6315 . . . . . . . . 9
1615oveq1d 6323 . . . . . . . 8
1716fveq2d 5883 . . . . . . 7
1817oveq1d 6323 . . . . . 6
1914, 18ifeq12d 3892 . . . . 5
2019mpteq2dv 4483 . . . 4
2111, 20syl5eq 2517 . . 3
2221cbvmptv 4488 . 2
23 fourierdlem113.p . 2 ..^
24 fourierdlem113.m . 2
25 fourierdlem113.q . 2
26 oveq1 6315 . . . . . . . 8
2726eleq1d 2533 . . . . . . 7
2827rexbidv 2892 . . . . . 6
2928cbvrabv 3030 . . . . 5
3029uneq2i 3576 . . . 4
3130fveq2i 5882 . . 3
3231oveq1i 6318 . 2
33 oveq1 6315 . . . . . . . . . . . 12
3433oveq2d 6324 . . . . . . . . . . 11
3534eleq1d 2533 . . . . . . . . . 10
3635cbvrexv 3006 . . . . . . . . 9
3736a1i 11 . . . . . . . 8
3837rabbiia 3019 . . . . . . 7
3938uneq2i 3576 . . . . . 6
40 isoeq5 6232 . . . . . 6
4139, 40ax-mp 5 . . . . 5
4241a1i 11 . . . 4
4333oveq2d 6324 . . . . . . . . . . . . . 14
4443eleq1d 2533 . . . . . . . . . . . . 13
4544cbvrexv 3006 . . . . . . . . . . . 12
4645a1i 11 . . . . . . . . . . 11
4746rabbiia 3019 . . . . . . . . . 10
4847uneq2i 3576 . . . . . . . . 9
4948fveq2i 5882 . . . . . . . 8
5049oveq1i 6318 . . . . . . 7
5150oveq2i 6319 . . . . . 6
52 isoeq4 6231 . . . . . 6
5351, 52ax-mp 5 . . . . 5
5453a1i 11 . . . 4
55 isoeq1 6228 . . . 4
5642, 54, 553bitrd 287 . . 3
5756cbviotav 5559 . 2
58 fourierdlem113.x . 2
59 pire 23492 . . . . 5
6059renegcli 9955 . . . 4
6160a1i 11 . . 3
6259a1i 11 . . 3
63 negpilt0 37580 . . . 4
6463a1i 11 . . 3
65 pipos 23494 . . . 4
6665a1i 11 . . 3
67 picn 23493 . . . . 5
68672timesi 10753 . . . 4
69 fourierdlem113.t . . . 4
7067, 67subnegi 9973 . . . 4
7168, 69, 703eqtr4i 2503 . . 3
7223fourierdlem2 38083 . . . . . . . 8 ..^
7324, 72syl 17 . . . . . . 7 ..^
7425, 73mpbid 215 . . . . . 6 ..^
7574simpld 466 . . . . 5
76 elmapi 7511 . . . . 5
7775, 76syl 17 . . . 4
78 fzfid 12224 . . . 4
79 rnffi 37513 . . . 4
8077, 78, 79syl2anc 673 . . 3
8123, 24, 25fourierdlem15 38096 . . . 4
82 frn 5747 . . . 4
8381, 82syl 17 . . 3
8474simprd 470 . . . . 5 ..^
8584simplrd 771 . . . 4
86 ffun 5742 . . . . . 6
8781, 86syl 17 . . . . 5
8824nnnn0d 10949 . . . . . . . 8
89 nn0uz 11217 . . . . . . . 8
9088, 89syl6eleq 2559 . . . . . . 7
91 eluzfz2 11833 . . . . . . 7
9290, 91syl 17 . . . . . 6
93 fdm 5745 . . . . . . . 8
9481, 93syl 17 . . . . . . 7
9594eqcomd 2477 . . . . . 6
9692, 95eleqtrd 2551 . . . . 5
97 fvelrn 6030 . . . . 5
9887, 96, 97syl2anc 673 . . . 4
9985, 98eqeltrrd 2550 . . 3
100 fourierdlem113.e . . 3
101 fourierdlem113.exq . . 3
102 eqid 2471 . . 3
103 isoeq1 6228 . . . . 5
10430, 48, 393eqtr4ri 2504 . . . . . 6
105 isoeq5 6232 . . . . . 6
106104, 105ax-mp 5 . . . . 5
107103, 106syl6bb 269 . . . 4
108107cbviotav 5559 . . 3
109 eqid 2471 . . 3
11061, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109fourierdlem51 38133 . 2
111 fourierdlem113.per . 2
112 ax-resscn 9614 . . . 4
113112a1i 11 . . 3 ..^
114 ioossre 11721 . . . . . . 7
115114a1i 11 . . . . . 6
1161, 115fssresd 5762 . . . . 5
117112a1i 11 . . . . 5
118116, 117fssd 5750 . . . 4
119118adantr 472 . . 3 ..^
120114a1i 11 . . 3 ..^
1211, 117fssd 5750 . . . . . . 7
122121adantr 472 . . . . . 6 ..^
123 ssid 3437 . . . . . . 7
124123a1i 11 . . . . . 6 ..^
125 eqid 2471 . . . . . . 7 fld fld
126125tgioo2 21899 . . . . . . 7 fldt
127125, 126dvres 22945 . . . . . 6
128113, 122, 124, 120, 127syl22anc 1293 . . . . 5 ..^
129128dmeqd 5042 . . . 4 ..^
130 ioontr 37707 . . . . . . 7
131130reseq2i 5108 . . . . . 6
132131dmeqi 5041 . . . . 5
133132a1i 11 . . . 4 ..^
134 fourierdlem113.dvcn . . . . 5 ..^
135 cncff 22003 . . . . 5
136 fdm 5745 . . . . 5
137134, 135, 1363syl 18 . . . 4 ..^
138129, 133, 1373eqtrd 2509 . . 3 ..^
139 dvcn 22954 . . 3
140113, 119, 120, 138, 139syl31anc 1295 . 2 ..^
141120, 113sstrd 3428 . . 3 ..^
14277adantr 472 . . . . . 6 ..^
143 fzofzp1 12037 . . . . . . 7 ..^
144143adantl 473 . . . . . 6 ..^
145142, 144ffvelrnd 6038 . . . . 5 ..^
146145rexrd 9708 . . . 4 ..^
147 elfzofz 11962 . . . . . 6 ..^
148147adantl 473 . . . . 5 ..^
149142, 148ffvelrnd 6038 . . . 4 ..^
15074simprrd 775 . . . . 5 ..^
151150r19.21bi 2776 . . . 4 ..^
152125, 146, 149, 151lptioo1cn 37824 . . 3 ..^ fld
153116adantr 472 . . . 4 ..^
154123a1i 11 . . . . . . . 8
155117, 121, 154dvbss 22935 . . . . . . 7
156 dvfre 22984 . . . . . . . 8
1571, 154, 156syl2anc 673 . . . . . . 7
158 0re 9661 . . . . . . . . . 10
15960, 158, 59lttri 9778 . . . . . . . . 9
16063, 65, 159mp2an 686 . . . . . . . 8
161160a1i 11 . . . . . . 7
16284simplld 769 . . . . . . 7
163134, 135syl 17 . . . . . . . 8 ..^
164 fourierdlem113.dvlb . . . . . . . 8 ..^ lim
165163, 141, 152, 164, 125ellimciota 37791 . . . . . . 7 ..^ lim lim
166149rexrd 9708 . . . . . . . . 9 ..^
167125, 166, 145, 151lptioo2cn 37823 . . . . . . . 8 ..^ fld
168 fourierdlem113.dvub . . . . . . . 8 ..^ lim
169163, 141, 167, 168, 125ellimciota 37791 . . . . . . 7 ..^ lim lim
170121adantr 472 . . . . . . . . . 10
171 zre 10965 . . . . . . . . . . . 12
172171adantl 473 . . . . . . . . . . 11
173 2re 10701 . . . . . . . . . . . . . . 15
174173, 59remulcli 9675 . . . . . . . . . . . . . 14
175174a1i 11 . . . . . . . . . . . . 13
17669, 175syl5eqel 2553 . . . . . . . . . . . 12
177176adantr 472 . . . . . . . . . . 11
178172, 177remulcld 9689 . . . . . . . . . 10
179170adantr 472 . . . . . . . . . . 11
180177adantr 472 . . . . . . . . . . 11
181 simplr 770 . . . . . . . . . . 11
182 simpr 468 . . . . . . . . . . 11
183111adant423 37430 . . . . . . . . . . 11
184179, 180, 181, 182, 183fperiodmul 37610 . . . . . . . . . 10
185 eqid 2471 . . . . . . . . . 10
186170, 178, 184, 185fperdvper 37887 . . . . . . . . 9
187186an32s 821 . . . . . . . 8
188187simpld 466 . . . . . . 7
189187simprd 470 . . . . . . 7
190 fveq2 5879 . . . . . . . . 9
191 oveq1 6315 . . . . . . . . . 10
192191fveq2d 5883 . . . . . . . . 9
193190, 192oveq12d 6326 . . . . . . . 8
194193cbvmptv 4488 . . . . . . 7 ..^ ..^
195 eqid 2471 . . . . . . 7
196155, 157, 61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195fourierdlem71 38153 . . . . . 6
197196adantr 472 . . . . 5 ..^
198 nfv 1769 . . . . . . . . 9 ..^
199 nfra1 2785 . . . . . . . . 9
200198, 199nfan 2031 . . . . . . . 8 ..^
201128, 131syl6eq 2521 . . . . . . . . . . . . . 14 ..^
202201fveq1d 5881 . . . . . . . . . . . . 13 ..^
203 fvres 5893 . . . . . . . . . . . . 13
204202, 203sylan9eq 2525 . . . . . . . . . . . 12 ..^
205204fveq2d 5883 . . . . . . . . . . 11 ..^
206205adantlr 729 . . . . . . . . . 10 ..^
207 simplr 770 . . . . . . . . . . 11 ..^
208 ssdmres 5132 . . . . . . . . . . . . . 14
209137, 208sylibr 217 . . . . . . . . . . . . 13 ..^
210209ad2antrr 740 . . . . . . . . . . . 12 ..^
211 simpr 468 . . . . . . . . . . . 12 ..^
212210, 211sseldd 3419 . . . . . . . . . . 11 ..^
213 rspa 2774 . . . . . . . . . . 11
214207, 212, 213syl2anc 673 . . . . . . . . . 10 ..^
215206, 214eqbrtrd 4416 . . . . . . . . 9 ..^
216215ex 441 . . . . . . . 8 ..^
217200, 216ralrimi 2800 . . . . . . 7 ..^
218217ex 441 . . . . . 6 ..^
219218reximdv 2857 . . . . 5 ..^
220197, 219mpd 15 . . . 4 ..^
221149, 145, 153, 138, 220ioodvbdlimc1 37904 . . 3 ..^ lim
222119, 141, 152, 221, 125ellimciota 37791 . 2 ..^ lim lim
223149, 145, 153, 138, 220ioodvbdlimc2 37907 . . 3 ..^ lim
224119, 141, 167, 223, 125ellimciota 37791 . 2 ..^ lim lim
225 frel 5744 . . . . . . 7
226157, 225syl 17 . . . . . 6
227 resindm 5155 . . . . . 6
228226, 227syl 17 . . . . 5
229 inss2 3644 . . . . . . 7
230229a1i 11 . . . . . 6
231157, 230fssresd 5762 . . . . 5
232228, 231feq1dd 37503 . . . 4
233232, 117fssd 5750 . . 3
234 ioosscn 37687 . . . . 5
235 ssinss1 3651 . . . . 5
236234, 235ax-mp 5 . . . 4
237236a1i 11 . . 3
238 3simpb 1028 . . . . . . . 8
239 simp2 1031 . . . . . . . 8
240170adantr 472 . . . . . . . . . 10
241177adantr 472 . . . . . . . . . 10
242 simplr 770 . . . . . . . . . 10
243 simpr 468 . . . . . . . . . 10
244 eleq1 2537 . . . . . . . . . . . . . 14
245244anbi2d 718 . . . . . . . . . . . . 13
246 oveq1 6315 . . . . . . . . . . . . . . 15
247246fveq2d 5883 . . . . . . . . . . . . . 14
248 fveq2 5879 . . . . . . . . . . . . . 14
249247, 248eqeq12d 2486 . . . . . . . . . . . . 13
250245, 249imbi12d 327 . . . . . . . . . . . 12
251250, 111chvarv 2120 . . . . . . . . . . 11
252251adant423 37430 . . . . . . . . . 10
253240, 241, 242, 243, 252fperiodmul 37610 . . . . . . . . 9
254170, 178, 253, 185fperdvper 37887 . . . . . . . 8
255238, 239, 254syl2anc 673 . . . . . . 7
256255simpld 466 . . . . . 6
257 oveq2 6316 . . . . . . . . . 10
258257oveq1d 6323 . . . . . . . . 9
259258fveq2d 5883 . . . . . . . 8
260259oveq1d 6323 . . . . . . 7
261260cbvmptv 4488 . . . . . 6
262 eqid 2471 . . . . . 6
26361, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209fourierdlem41 38123 . . . . 5
264263simpld 466 . . . 4
265125cnfldtop 21882 . . . . . . . . 9 fld
266265a1i 11 . . . . . . . 8 fld
267236a1i 11 . . . . . . . 8
268 mnfxr 11437 . . . . . . . . . . . 12
269268a1i 11 . . . . . . . . . . 11
270 rexr 9704 . . . . . . . . . . . 12
271 mnflt 11448 . . . . . . . . . . . 12
272269, 270, 271xrltled 37574 . . . . . . . . . . 11
273 iooss1 11696 . . . . . . . . . . 11
274269, 272, 273syl2anc 673 . . . . . . . . . 10
2752743ad2ant2 1052 . . . . . . . . 9
276 simp3 1032 . . . . . . . . 9
277275, 276ssind 3647 . . . . . . . 8
278 unicntop 37433 . . . . . . . . 9 fld
279278lpss3 20237 . . . . . . . 8 fld fld fld
280266, 267, 277, 279syl3anc 1292 . . . . . . 7 fld fld
2812803adant3l 1288 . . . . . 6 fld fld
2822703ad2ant2 1052 . . . . . . 7
283583ad2ant1 1051 . . . . . . 7
284 simp3l 1058 . . . . . . 7
285125, 282, 283, 284lptioo2cn 37823 . . . . . 6 fld
286281, 285sseldd 3419 . . . . 5 fld
287286rexlimdv3a 2873 . . . 4 fld
288264, 287mpd 15 . . 3 fld
289255simprd 470 . . . 4
290 oveq2 6316 . . . . . . . 8
291290oveq1d 6323 . . . . . . 7
292291fveq2d 5883 . . . . . 6
293292oveq1d 6323 . . . . 5
294293cbvmptv 4488 . . . 4
295 id 22 . . . . . 6
296 fveq2 5879 . . . . . 6