Metamath Proof Explorer


Theorem fourierswlem

Description: The Fourier series for the square wave F converges to Y , a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierswlem.t T = 2 π
fourierswlem.f F = x if x mod T < π 1 1
fourierswlem.x X
fourierswlem.y Y = if X mod π = 0 0 F X
Assertion fourierswlem Y = if X mod T 0 π 1 1 + F X 2

Proof

Step Hyp Ref Expression
1 fourierswlem.t T = 2 π
2 fourierswlem.f F = x if x mod T < π 1 1
3 fourierswlem.x X
4 fourierswlem.y Y = if X mod π = 0 0 F X
5 simpr X mod π = 0 2 X π 2 X π
6 2z 2
7 6 a1i X mod π = 0 2 X π 2
8 pirp π +
9 mod0 X π + X mod π = 0 X π
10 3 8 9 mp2an X mod π = 0 X π
11 10 biimpi X mod π = 0 X π
12 11 adantr X mod π = 0 2 X π X π
13 divides 2 X π 2 X π k k 2 = X π
14 7 12 13 syl2anc X mod π = 0 2 X π 2 X π k k 2 = X π
15 5 14 mpbid X mod π = 0 2 X π k k 2 = X π
16 2cnd k 2
17 picn π
18 17 a1i k π
19 zcn k k
20 16 18 19 mulassd k 2 π k = 2 π k
21 18 19 mulcld k π k
22 16 21 mulcomd k 2 π k = π k 2
23 20 22 eqtrd k 2 π k = π k 2
24 23 adantr k k 2 = X π 2 π k = π k 2
25 18 19 16 mulassd k π k 2 = π k 2
26 25 adantr k k 2 = X π π k 2 = π k 2
27 id k 2 = X π k 2 = X π
28 27 eqcomd k 2 = X π X π = k 2
29 28 adantl k k 2 = X π X π = k 2
30 3 recni X
31 30 a1i k k 2 = X π X
32 17 a1i k k 2 = X π π
33 19 adantr k k 2 = X π k
34 2cnd k k 2 = X π 2
35 33 34 mulcld k k 2 = X π k 2
36 pire π
37 pipos 0 < π
38 36 37 gt0ne0ii π 0
39 38 a1i k k 2 = X π π 0
40 31 32 35 39 divmuld k k 2 = X π X π = k 2 π k 2 = X
41 29 40 mpbid k k 2 = X π π k 2 = X
42 24 26 41 3eqtrrd k k 2 = X π X = 2 π k
43 1 a1i k k 2 = X π T = 2 π
44 42 43 oveq12d k k 2 = X π X T = 2 π k 2 π
45 16 18 mulcld k 2 π
46 2ne0 2 0
47 46 a1i k 2 0
48 38 a1i k π 0
49 16 18 47 48 mulne0d k 2 π 0
50 19 45 49 divcan3d k 2 π k 2 π = k
51 50 adantr k k 2 = X π 2 π k 2 π = k
52 44 51 eqtrd k k 2 = X π X T = k
53 simpl k k 2 = X π k
54 52 53 eqeltrd k k 2 = X π X T
55 54 ex k k 2 = X π X T
56 55 a1i X mod π = 0 2 X π k k 2 = X π X T
57 56 rexlimdv X mod π = 0 2 X π k k 2 = X π X T
58 15 57 mpd X mod π = 0 2 X π X T
59 2re 2
60 59 36 remulcli 2 π
61 1 60 eqeltri T
62 2pos 0 < 2
63 59 36 62 37 mulgt0ii 0 < 2 π
64 63 1 breqtrri 0 < T
65 61 64 elrpii T +
66 mod0 X T + X mod T = 0 X T
67 3 65 66 mp2an X mod T = 0 X T
68 58 67 sylibr X mod π = 0 2 X π X mod T = 0
69 68 orcd X mod π = 0 2 X π X mod T = 0 X mod T = π
70 odd2np1 X π ¬ 2 X π k 2 k + 1 = X π
71 10 70 sylbi X mod π = 0 ¬ 2 X π k 2 k + 1 = X π
72 71 biimpa X mod π = 0 ¬ 2 X π k 2 k + 1 = X π
73 16 19 mulcld k 2 k
74 73 adantr k 2 k + 1 = X π 2 k
75 1cnd k 2 k + 1 = X π 1
76 17 a1i k 2 k + 1 = X π π
77 74 75 76 adddird k 2 k + 1 = X π 2 k + 1 π = 2 k π + 1 π
78 16 19 mulcomd k 2 k = k 2
79 78 oveq1d k 2 k π = k 2 π
80 19 16 18 mulassd k k 2 π = k 2 π
81 1 eqcomi 2 π = T
82 81 a1i k 2 π = T
83 82 oveq2d k k 2 π = k T
84 79 80 83 3eqtrd k 2 k π = k T
85 17 mulid2i 1 π = π
86 85 a1i k 1 π = π
87 84 86 oveq12d k 2 k π + 1 π = k T + π
88 87 adantr k 2 k + 1 = X π 2 k π + 1 π = k T + π
89 1 45 eqeltrid k T
90 19 89 mulcld k k T
91 90 18 addcomd k k T + π = π + k T
92 91 adantr k 2 k + 1 = X π k T + π = π + k T
93 77 88 92 3eqtrrd k 2 k + 1 = X π π + k T = 2 k + 1 π
94 peano2cn 2 k 2 k + 1
95 73 94 syl k 2 k + 1
96 95 18 mulcomd k 2 k + 1 π = π 2 k + 1
97 96 adantr k 2 k + 1 = X π 2 k + 1 π = π 2 k + 1
98 id 2 k + 1 = X π 2 k + 1 = X π
99 98 eqcomd 2 k + 1 = X π X π = 2 k + 1
100 99 adantl k 2 k + 1 = X π X π = 2 k + 1
101 30 a1i k 2 k + 1 = X π X
102 95 adantr k 2 k + 1 = X π 2 k + 1
103 38 a1i k 2 k + 1 = X π π 0
104 101 76 102 103 divmuld k 2 k + 1 = X π X π = 2 k + 1 π 2 k + 1 = X
105 100 104 mpbid k 2 k + 1 = X π π 2 k + 1 = X
106 93 97 105 3eqtrrd k 2 k + 1 = X π X = π + k T
107 106 oveq1d k 2 k + 1 = X π X mod T = π + k T mod T
108 modcyc π T + k π + k T mod T = π mod T
109 36 65 108 mp3an12 k π + k T mod T = π mod T
110 109 adantr k 2 k + 1 = X π π + k T mod T = π mod T
111 36 a1i k 2 k + 1 = X π π
112 65 a1i k 2 k + 1 = X π T +
113 0re 0
114 113 36 37 ltleii 0 π
115 114 a1i k 2 k + 1 = X π 0 π
116 2timesgt π + π < 2 π
117 8 116 ax-mp π < 2 π
118 117 1 breqtrri π < T
119 118 a1i k 2 k + 1 = X π π < T
120 modid π T + 0 π π < T π mod T = π
121 111 112 115 119 120 syl22anc k 2 k + 1 = X π π mod T = π
122 107 110 121 3eqtrd k 2 k + 1 = X π X mod T = π
123 122 ex k 2 k + 1 = X π X mod T = π
124 123 a1i X mod π = 0 ¬ 2 X π k 2 k + 1 = X π X mod T = π
125 124 rexlimdv X mod π = 0 ¬ 2 X π k 2 k + 1 = X π X mod T = π
126 72 125 mpd X mod π = 0 ¬ 2 X π X mod T = π
127 126 olcd X mod π = 0 ¬ 2 X π X mod T = 0 X mod T = π
128 69 127 pm2.61dan X mod π = 0 X mod T = 0 X mod T = π
129 0xr 0 *
130 36 rexri π *
131 iocgtlb 0 * π * X mod T 0 π 0 < X mod T
132 129 130 131 mp3an12 X mod T 0 π 0 < X mod T
133 132 gt0ne0d X mod T 0 π X mod T 0
134 133 neneqd X mod T 0 π ¬ X mod T = 0
135 pm2.53 X mod T = 0 X mod T = π ¬ X mod T = 0 X mod T = π
136 135 imp X mod T = 0 X mod T = π ¬ X mod T = 0 X mod T = π
137 128 134 136 syl2anr X mod T 0 π X mod π = 0 X mod T = π
138 129 a1i X mod T = π 0 *
139 130 a1i X mod T = π π *
140 modcl X T + X mod T
141 3 65 140 mp2an X mod T
142 141 rexri X mod T *
143 142 a1i X mod T = π X mod T *
144 id X mod T = π X mod T = π
145 37 144 breqtrrid X mod T = π 0 < X mod T
146 36 eqlei2 X mod T = π X mod T π
147 138 139 143 145 146 eliocd X mod T = π X mod T 0 π
148 147 iftrued X mod T = π if X mod T 0 π 1 1 = 1
149 148 adantl X mod π = 0 X mod T = π if X mod T 0 π 1 1 = 1
150 oveq1 x = X x mod T = X mod T
151 150 breq1d x = X x mod T < π X mod T < π
152 151 ifbid x = X if x mod T < π 1 1 = if X mod T < π 1 1
153 1ex 1 V
154 negex 1 V
155 153 154 ifex if X mod T < π 1 1 V
156 152 2 155 fvmpt X F X = if X mod T < π 1 1
157 3 156 ax-mp F X = if X mod T < π 1 1
158 141 a1i X mod T < π X mod T
159 id X mod T < π X mod T < π
160 158 159 ltned X mod T < π X mod T π
161 160 necon2bi X mod T = π ¬ X mod T < π
162 161 iffalsed X mod T = π if X mod T < π 1 1 = 1
163 157 162 syl5eq X mod T = π F X = 1
164 163 adantl X mod π = 0 X mod T = π F X = 1
165 149 164 oveq12d X mod π = 0 X mod T = π if X mod T 0 π 1 1 + F X = 1 + -1
166 1pneg1e0 1 + -1 = 0
167 165 166 eqtrdi X mod π = 0 X mod T = π if X mod T 0 π 1 1 + F X = 0
168 167 oveq1d X mod π = 0 X mod T = π if X mod T 0 π 1 1 + F X 2 = 0 2
169 168 adantll X mod T 0 π X mod π = 0 X mod T = π if X mod T 0 π 1 1 + F X 2 = 0 2
170 2cn 2
171 170 46 div0i 0 2 = 0
172 171 a1i X mod T 0 π X mod π = 0 X mod T = π 0 2 = 0
173 iftrue X mod π = 0 if X mod π = 0 0 F X = 0
174 4 173 eqtr2id X mod π = 0 0 = Y
175 174 ad2antlr X mod T 0 π X mod π = 0 X mod T = π 0 = Y
176 169 172 175 3eqtrrd X mod T 0 π X mod π = 0 X mod T = π Y = if X mod T 0 π 1 1 + F X 2
177 137 176 mpdan X mod T 0 π X mod π = 0 Y = if X mod T 0 π 1 1 + F X 2
178 iftrue X mod T 0 π if X mod T 0 π 1 1 = 1
179 178 adantr X mod T 0 π ¬ X mod π = 0 if X mod T 0 π 1 1 = 1
180 141 a1i X mod T 0 π ¬ X mod π = 0 X mod T
181 36 a1i X mod T 0 π ¬ X mod π = 0 π
182 iocleub 0 * π * X mod T 0 π X mod T π
183 129 130 182 mp3an12 X mod T 0 π X mod T π
184 183 adantr X mod T 0 π ¬ X mod π = 0 X mod T π
185 ax-1cn 1
186 185 17 mulcomi 1 π = π 1
187 85 186 eqtr3i π = π 1
188 187 oveq1i π + π 2 X T = π 1 + π 2 X T
189 170 17 mulcomi 2 π = π 2
190 1 189 eqtri T = π 2
191 190 oveq1i T X T = π 2 X T
192 113 64 gtneii T 0
193 3 61 192 redivcli X T
194 flcl X T X T
195 193 194 ax-mp X T
196 zcn X T X T
197 195 196 ax-mp X T
198 17 170 197 mulassi π 2 X T = π 2 X T
199 191 198 eqtri T X T = π 2 X T
200 199 oveq2i π + T X T = π + π 2 X T
201 170 197 mulcli 2 X T
202 17 185 201 adddii π 1 + 2 X T = π 1 + π 2 X T
203 188 200 202 3eqtr4ri π 1 + 2 X T = π + T X T
204 203 a1i π = X mod T π 1 + 2 X T = π + T X T
205 id π = X mod T π = X mod T
206 modval X T + X mod T = X T X T
207 3 65 206 mp2an X mod T = X T X T
208 205 207 eqtrdi π = X mod T π = X T X T
209 208 oveq1d π = X mod T π + T X T = X - T X T + T X T
210 30 a1i π = X mod T X
211 61 recni T
212 211 197 mulcli T X T
213 212 a1i π = X mod T T X T
214 210 213 npcand π = X mod T X - T X T + T X T = X
215 204 209 214 3eqtrrd π = X mod T X = π 1 + 2 X T
216 215 oveq1d π = X mod T X π = π 1 + 2 X T π
217 185 201 addcli 1 + 2 X T
218 217 17 38 divcan3i π 1 + 2 X T π = 1 + 2 X T
219 216 218 eqtrdi π = X mod T X π = 1 + 2 X T
220 1z 1
221 zmulcl 2 X T 2 X T
222 6 195 221 mp2an 2 X T
223 zaddcl 1 2 X T 1 + 2 X T
224 220 222 223 mp2an 1 + 2 X T
225 224 a1i π = X mod T 1 + 2 X T
226 219 225 eqeltrd π = X mod T X π
227 226 10 sylibr π = X mod T X mod π = 0
228 227 necon3bi ¬ X mod π = 0 π X mod T
229 228 adantl X mod T 0 π ¬ X mod π = 0 π X mod T
230 180 181 184 229 leneltd X mod T 0 π ¬ X mod π = 0 X mod T < π
231 iftrue X mod T < π if X mod T < π 1 1 = 1
232 157 231 syl5eq X mod T < π F X = 1
233 230 232 syl X mod T 0 π ¬ X mod π = 0 F X = 1
234 179 233 oveq12d X mod T 0 π ¬ X mod π = 0 if X mod T 0 π 1 1 + F X = 1 + 1
235 234 oveq1d X mod T 0 π ¬ X mod π = 0 if X mod T 0 π 1 1 + F X 2 = 1 + 1 2
236 1p1e2 1 + 1 = 2
237 236 oveq1i 1 + 1 2 = 2 2
238 2div2e1 2 2 = 1
239 237 238 eqtr2i 1 = 1 + 1 2
240 233 239 eqtr2di X mod T 0 π ¬ X mod π = 0 1 + 1 2 = F X
241 iffalse ¬ X mod π = 0 if X mod π = 0 0 F X = F X
242 4 241 eqtr2id ¬ X mod π = 0 F X = Y
243 242 adantl X mod T 0 π ¬ X mod π = 0 F X = Y
244 235 240 243 3eqtrrd X mod T 0 π ¬ X mod π = 0 Y = if X mod T 0 π 1 1 + F X 2
245 177 244 pm2.61dan X mod T 0 π Y = if X mod T 0 π 1 1 + F X 2
246 133 necon2bi X mod T = 0 ¬ X mod T 0 π
247 246 iffalsed X mod T = 0 if X mod T 0 π 1 1 = 1
248 id X mod T = 0 X mod T = 0
249 248 37 eqbrtrdi X mod T = 0 X mod T < π
250 249 iftrued X mod T = 0 if X mod T < π 1 1 = 1
251 157 250 syl5eq X mod T = 0 F X = 1
252 247 251 oveq12d X mod T = 0 if X mod T 0 π 1 1 + F X = - 1 + 1
253 252 oveq1d X mod T = 0 if X mod T 0 π 1 1 + F X 2 = - 1 + 1 2
254 neg1cn 1
255 185 254 166 addcomli - 1 + 1 = 0
256 255 oveq1i - 1 + 1 2 = 0 2
257 256 171 eqtri - 1 + 1 2 = 0
258 257 a1i X mod T = 0 - 1 + 1 2 = 0
259 1 oveq2i X T = X 2 π
260 2cnne0 2 2 0
261 17 38 pm3.2i π π 0
262 divdiv1 X 2 2 0 π π 0 X 2 π = X 2 π
263 30 260 261 262 mp3an X 2 π = X 2 π
264 30 170 17 46 38 divdiv32i X 2 π = X π 2
265 259 263 264 3eqtr2i X T = X π 2
266 265 oveq2i 2 X T = 2 X π 2
267 30 17 38 divcli X π
268 267 170 46 divcan2i 2 X π 2 = X π
269 266 268 eqtr2i X π = 2 X T
270 6 a1i X T 2
271 id X T X T
272 270 271 zmulcld X T 2 X T
273 269 272 eqeltrid X T X π
274 67 273 sylbi X mod T = 0 X π
275 274 10 sylibr X mod T = 0 X mod π = 0
276 275 iftrued X mod T = 0 if X mod π = 0 0 F X = 0
277 4 276 eqtr2id X mod T = 0 0 = Y
278 253 258 277 3eqtrrd X mod T = 0 Y = if X mod T 0 π 1 1 + F X 2
279 278 adantl ¬ X mod T 0 π X mod T = 0 Y = if X mod T 0 π 1 1 + F X 2
280 130 a1i ¬ X mod T 0 π ¬ X mod T = 0 π *
281 61 rexri T *
282 281 a1i ¬ X mod T 0 π ¬ X mod T = 0 T *
283 141 a1i ¬ X mod T 0 π ¬ X mod T = 0 X mod T
284 pm4.56 ¬ X mod T 0 π ¬ X mod T = 0 ¬ X mod T 0 π X mod T = 0
285 284 biimpi ¬ X mod T 0 π ¬ X mod T = 0 ¬ X mod T 0 π X mod T = 0
286 olc X mod T = 0 X mod T 0 π X mod T = 0
287 286 adantl X mod T π X mod T = 0 X mod T 0 π X mod T = 0
288 129 a1i X mod T π ¬ X mod T = 0 0 *
289 130 a1i X mod T π ¬ X mod T = 0 π *
290 142 a1i X mod T π ¬ X mod T = 0 X mod T *
291 0red ¬ X mod T = 0 0
292 141 a1i ¬ X mod T = 0 X mod T
293 modge0 X T + 0 X mod T
294 3 65 293 mp2an 0 X mod T
295 294 a1i ¬ X mod T = 0 0 X mod T
296 neqne ¬ X mod T = 0 X mod T 0
297 291 292 295 296 leneltd ¬ X mod T = 0 0 < X mod T
298 297 adantl X mod T π ¬ X mod T = 0 0 < X mod T
299 simpl X mod T π ¬ X mod T = 0 X mod T π
300 288 289 290 298 299 eliocd X mod T π ¬ X mod T = 0 X mod T 0 π
301 300 orcd X mod T π ¬ X mod T = 0 X mod T 0 π X mod T = 0
302 287 301 pm2.61dan X mod T π X mod T 0 π X mod T = 0
303 285 302 nsyl ¬ X mod T 0 π ¬ X mod T = 0 ¬ X mod T π
304 36 a1i ¬ X mod T 0 π ¬ X mod T = 0 π
305 304 283 ltnled ¬ X mod T 0 π ¬ X mod T = 0 π < X mod T ¬ X mod T π
306 303 305 mpbird ¬ X mod T 0 π ¬ X mod T = 0 π < X mod T
307 modlt X T + X mod T < T
308 3 65 307 mp2an X mod T < T
309 308 a1i ¬ X mod T 0 π ¬ X mod T = 0 X mod T < T
310 280 282 283 306 309 eliood ¬ X mod T 0 π ¬ X mod T = 0 X mod T π T
311 129 a1i X mod T π T 0 *
312 36 a1i X mod T π T π
313 142 a1i X mod T π T X mod T *
314 ioogtlb π * T * X mod T π T π < X mod T
315 130 281 314 mp3an12 X mod T π T π < X mod T
316 311 312 313 315 gtnelioc X mod T π T ¬ X mod T 0 π
317 316 iffalsed X mod T π T if X mod T 0 π 1 1 = 1
318 141 a1i X mod T π T X mod T
319 312 318 315 ltnsymd X mod T π T ¬ X mod T < π
320 319 iffalsed X mod T π T if X mod T < π 1 1 = 1
321 157 320 syl5eq X mod T π T F X = 1
322 317 321 oveq12d X mod T π T if X mod T 0 π 1 1 + F X = - 1 + -1
323 322 oveq1d X mod T π T if X mod T 0 π 1 1 + F X 2 = - 1 + -1 2
324 df-2 2 = 1 + 1
325 324 negeqi 2 = 1 + 1
326 185 185 negdii 1 + 1 = - 1 + -1
327 325 326 eqtr2i - 1 + -1 = 2
328 327 oveq1i - 1 + -1 2 = 2 2
329 divneg 2 2 2 0 2 2 = 2 2
330 170 170 46 329 mp3an 2 2 = 2 2
331 238 negeqi 2 2 = 1
332 328 330 331 3eqtr2i - 1 + -1 2 = 1
333 332 a1i X mod T π T - 1 + -1 2 = 1
334 4 a1i X mod T π T Y = if X mod π = 0 0 F X
335 312 318 ltnled X mod T π T π < X mod T ¬ X mod T π
336 315 335 mpbid X mod T π T ¬ X mod T π
337 248 114 eqbrtrdi X mod T = 0 X mod T π
338 337 adantl X mod π = 0 X mod T = 0 X mod T π
339 128 orcanai X mod π = 0 ¬ X mod T = 0 X mod T = π
340 339 146 syl X mod π = 0 ¬ X mod T = 0 X mod T π
341 338 340 pm2.61dan X mod π = 0 X mod T π
342 336 341 nsyl X mod T π T ¬ X mod π = 0
343 342 iffalsed X mod T π T if X mod π = 0 0 F X = F X
344 334 343 321 3eqtrrd X mod T π T 1 = Y
345 323 333 344 3eqtrrd X mod T π T Y = if X mod T 0 π 1 1 + F X 2
346 310 345 syl ¬ X mod T 0 π ¬ X mod T = 0 Y = if X mod T 0 π 1 1 + F X 2
347 279 346 pm2.61dan ¬ X mod T 0 π Y = if X mod T 0 π 1 1 + F X 2
348 245 347 pm2.61i Y = if X mod T 0 π 1 1 + F X 2