Metamath Proof Explorer


Theorem fouriersw

Description: Fourier series convergence, for the square wave function. Where F is discontinuous, the series converges to 0 , the average value of the left and the right limits. Notice that F is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fouriersw.t T = 2 π
fouriersw.f F = x if x mod T < π 1 1
fouriersw.x X
fouriersw.z S = n sin 2 n 1 X 2 n 1
fouriersw.y Y = if X mod π = 0 0 F X
Assertion fouriersw 4 π k sin 2 k 1 X 2 k 1 = Y seq 1 + S π 4 Y

Proof

Step Hyp Ref Expression
1 fouriersw.t T = 2 π
2 fouriersw.f F = x if x mod T < π 1 1
3 fouriersw.x X
4 fouriersw.z S = n sin 2 n 1 X 2 n 1
5 fouriersw.y Y = if X mod π = 0 0 F X
6 nnuz = 1
7 1zzd 1
8 eqidd k n sin 2 n 1 X 2 n 1 = n sin 2 n 1 X 2 n 1
9 oveq2 n = k 2 n = 2 k
10 9 oveq1d n = k 2 n 1 = 2 k 1
11 10 oveq1d n = k 2 n 1 X = 2 k 1 X
12 11 fveq2d n = k sin 2 n 1 X = sin 2 k 1 X
13 12 10 oveq12d n = k sin 2 n 1 X 2 n 1 = sin 2 k 1 X 2 k 1
14 13 adantl k n = k sin 2 n 1 X 2 n 1 = sin 2 k 1 X 2 k 1
15 id k k
16 ovex sin 2 k 1 X 2 k 1 V
17 16 a1i k sin 2 k 1 X 2 k 1 V
18 8 14 15 17 fvmptd k n sin 2 n 1 X 2 n 1 k = sin 2 k 1 X 2 k 1
19 18 adantl k n sin 2 n 1 X 2 n 1 k = sin 2 k 1 X 2 k 1
20 2z 2
21 20 a1i k 2
22 nnz k k
23 21 22 zmulcld k 2 k
24 1zzd k 1
25 23 24 zsubcld k 2 k 1
26 25 zcnd k 2 k 1
27 3 recni X
28 27 a1i k X
29 26 28 mulcld k 2 k 1 X
30 29 sincld k sin 2 k 1 X
31 0red k 0
32 2re 2
33 32 a1i k 2
34 1red k 1
35 33 34 remulcld k 2 1
36 35 34 resubcld k 2 1 1
37 25 zred k 2 k 1
38 0lt1 0 < 1
39 2t1e2 2 1 = 2
40 39 oveq1i 2 1 1 = 2 1
41 2m1e1 2 1 = 1
42 40 41 eqtr2i 1 = 2 1 1
43 38 42 breqtri 0 < 2 1 1
44 43 a1i k 0 < 2 1 1
45 23 zred k 2 k
46 nnre k k
47 0le2 0 2
48 47 a1i k 0 2
49 nnge1 k 1 k
50 34 46 33 48 49 lemul2ad k 2 1 2 k
51 35 45 34 50 lesub1dd k 2 1 1 2 k 1
52 31 36 37 44 51 ltletrd k 0 < 2 k 1
53 31 52 gtned k 2 k 1 0
54 30 26 53 divcld k sin 2 k 1 X 2 k 1
55 54 adantl k sin 2 k 1 X 2 k 1
56 picn π
57 56 a1i π
58 4cn 4
59 58 a1i 4
60 4ne0 4 0
61 60 a1i 4 0
62 57 59 61 divcld π 4
63 eqid n if 2 n 0 4 n π sin n X = n if 2 n 0 4 n π sin n X
64 0cnd n 0
65 58 a1i n 4
66 nncn n n
67 mulcl n π n π
68 66 56 67 sylancl n n π
69 56 a1i n π
70 nnne0 n n 0
71 0re 0
72 pipos 0 < π
73 71 72 gtneii π 0
74 73 a1i n π 0
75 66 69 70 74 mulne0d n n π 0
76 65 68 75 divcld n 4 n π
77 27 a1i n X
78 66 77 mulcld n n X
79 78 sincld n sin n X
80 76 79 mulcld n 4 n π sin n X
81 64 80 ifcld n if 2 n 0 4 n π sin n X
82 63 81 fmpti n if 2 n 0 4 n π sin n X :
83 82 a1i n if 2 n 0 4 n π sin n X :
84 eqidd k n if 2 n 0 4 n π sin n X = n if 2 n 0 4 n π sin n X
85 breq2 n = k 2 n 2 k
86 oveq1 n = k n π = k π
87 86 oveq2d n = k 4 n π = 4 k π
88 oveq1 n = k n X = k X
89 88 fveq2d n = k sin n X = sin k X
90 87 89 oveq12d n = k 4 n π sin n X = 4 k π sin k X
91 85 90 ifbieq2d n = k if 2 n 0 4 n π sin n X = if 2 k 0 4 k π sin k X
92 91 adantl k n = k if 2 n 0 4 n π sin n X = if 2 k 0 4 k π sin k X
93 c0ex 0 V
94 ovex 4 k π sin k X V
95 93 94 ifex if 2 k 0 4 k π sin k X V
96 95 a1i k if 2 k 0 4 k π sin k X V
97 84 92 15 96 fvmptd k n if 2 n 0 4 n π sin n X k = if 2 k 0 4 k π sin k X
98 97 adantr k k 2 n if 2 n 0 4 n π sin n X k = if 2 k 0 4 k π sin k X
99 simpr k k 2 k 2
100 simpl k k 2 k
101 2nn 2
102 nndivdvds k 2 2 k k 2
103 100 101 102 sylancl k k 2 2 k k 2
104 99 103 mpbird k k 2 2 k
105 104 iftrued k k 2 if 2 k 0 4 k π sin k X = 0
106 98 105 eqtrd k k 2 n if 2 n 0 4 n π sin n X k = 0
107 106 3adant1 k k 2 n if 2 n 0 4 n π sin n X k = 0
108 1re 1
109 108 renegcli 1
110 108 109 ifcli if x mod T < π 1 1
111 110 a1i x if x mod T < π 1 1
112 2 111 fmpti F :
113 oveq1 x = y x mod T = y mod T
114 113 breq1d x = y x mod T < π y mod T < π
115 114 ifbid x = y if x mod T < π 1 1 = if y mod T < π 1 1
116 115 cbvmptv x if x mod T < π 1 1 = y if y mod T < π 1 1
117 2 116 eqtri F = y if y mod T < π 1 1
118 117 a1i x F = y if y mod T < π 1 1
119 oveq1 y = x + T y mod T = x + T mod T
120 pire π
121 32 120 remulcli 2 π
122 1 121 eqeltri T
123 122 recni T
124 123 mulid2i 1 T = T
125 124 eqcomi T = 1 T
126 125 oveq2i x + T = x + 1 T
127 126 oveq1i x + T mod T = x + 1 T mod T
128 119 127 eqtrdi y = x + T y mod T = x + 1 T mod T
129 128 adantl x y = x + T y mod T = x + 1 T mod T
130 simpl x y = x + T x
131 2pos 0 < 2
132 32 120 131 72 mulgt0ii 0 < 2 π
133 1 eqcomi 2 π = T
134 132 133 breqtri 0 < T
135 122 134 elrpii T +
136 135 a1i x y = x + T T +
137 1zzd x y = x + T 1
138 modcyc x T + 1 x + 1 T mod T = x mod T
139 130 136 137 138 syl3anc x y = x + T x + 1 T mod T = x mod T
140 129 139 eqtrd x y = x + T y mod T = x mod T
141 140 breq1d x y = x + T y mod T < π x mod T < π
142 141 ifbid x y = x + T if y mod T < π 1 1 = if x mod T < π 1 1
143 id x x
144 122 a1i x T
145 143 144 readdcld x x + T
146 118 142 145 111 fvmptd x F x + T = if x mod T < π 1 1
147 2 fvmpt2 x if x mod T < π 1 1 F x = if x mod T < π 1 1
148 110 147 mpan2 x F x = if x mod T < π 1 1
149 146 148 eqtr4d x F x + T = F x
150 eqid F π π = F π π
151 snfi 0 Fin
152 eldifi x π π dom F π π x π π
153 0xr 0 *
154 153 a1i x π π 0 < x 0 *
155 120 rexri π *
156 155 a1i x π π 0 < x π *
157 elioore x π π x
158 157 adantr x π π 0 < x x
159 simpr x π π 0 < x 0 < x
160 120 renegcli π
161 160 rexri π *
162 iooltub π * π * x π π x < π
163 161 155 162 mp3an12 x π π x < π
164 163 adantr x π π 0 < x x < π
165 154 156 158 159 164 eliood x π π 0 < x x 0 π
166 negpilt0 π < 0
167 160 71 166 ltleii π 0
168 iooss1 π * π 0 0 π π π
169 161 167 168 mp2an 0 π π π
170 169 sseli x 0 π x π π
171 2 reseq1i F 0 π = x if x mod T < π 1 1 0 π
172 ioossre 0 π
173 resmpt 0 π x if x mod T < π 1 1 0 π = x 0 π if x mod T < π 1 1
174 172 173 ax-mp x if x mod T < π 1 1 0 π = x 0 π if x mod T < π 1 1
175 elioore x 0 π x
176 135 a1i x 0 π T +
177 0red x 0 π 0
178 ioogtlb 0 * π * x 0 π 0 < x
179 153 155 178 mp3an12 x 0 π 0 < x
180 177 175 179 ltled x 0 π 0 x
181 120 a1i x 0 π π
182 122 a1i x 0 π T
183 170 163 syl x 0 π x < π
184 pirp π +
185 2timesgt π + π < 2 π
186 184 185 ax-mp π < 2 π
187 186 133 breqtri π < T
188 187 a1i x 0 π π < T
189 175 181 182 183 188 lttrd x 0 π x < T
190 modid x T + 0 x x < T x mod T = x
191 175 176 180 189 190 syl22anc x 0 π x mod T = x
192 191 183 eqbrtrd x 0 π x mod T < π
193 192 iftrued x 0 π if x mod T < π 1 1 = 1
194 193 mpteq2ia x 0 π if x mod T < π 1 1 = x 0 π 1
195 171 174 194 3eqtrri x 0 π 1 = F 0 π
196 195 oveq2i dx 0 π 1 d x = D F 0 π
197 reelprrecn
198 197 a1i
199 iooretop 0 π topGen ran .
200 eqid TopOpen fld = TopOpen fld
201 200 tgioo2 topGen ran . = TopOpen fld 𝑡
202 199 201 eleqtri 0 π TopOpen fld 𝑡
203 202 a1i 0 π TopOpen fld 𝑡
204 1cnd 1
205 198 203 204 dvmptconst dx 0 π 1 d x = x 0 π 0
206 205 mptru dx 0 π 1 d x = x 0 π 0
207 ssid
208 ax-resscn
209 fss F : F :
210 112 208 209 mp2an F :
211 dvresioo F : D F 0 π = F 0 π
212 207 210 211 mp2an D F 0 π = F 0 π
213 196 206 212 3eqtr3i x 0 π 0 = F 0 π
214 213 dmeqi dom x 0 π 0 = dom F 0 π
215 eqid x 0 π 0 = x 0 π 0
216 93 215 dmmpti dom x 0 π 0 = 0 π
217 214 216 eqtr3i dom F 0 π = 0 π
218 ssdmres 0 π dom F dom F 0 π = 0 π
219 217 218 mpbir 0 π dom F
220 219 sseli x 0 π x dom F
221 170 220 elind x 0 π x π π dom F
222 dmres dom F π π = π π dom F
223 221 222 eleqtrrdi x 0 π x dom F π π
224 165 223 syl x π π 0 < x x dom F π π
225 224 adantlr x π π ¬ x = 0 0 < x x dom F π π
226 161 a1i x π π ¬ x = 0 ¬ 0 < x π *
227 153 a1i x π π ¬ x = 0 ¬ 0 < x 0 *
228 157 ad2antrr x π π ¬ x = 0 ¬ 0 < x x
229 ioogtlb π * π * x π π π < x
230 161 155 229 mp3an12 x π π π < x
231 230 ad2antrr x π π ¬ x = 0 ¬ 0 < x π < x
232 0red x π π ¬ x = 0 ¬ 0 < x 0
233 neqne ¬ x = 0 x 0
234 233 ad2antlr x π π ¬ x = 0 ¬ 0 < x x 0
235 simpr x π π ¬ x = 0 ¬ 0 < x ¬ 0 < x
236 228 232 234 235 lttri5d x π π ¬ x = 0 ¬ 0 < x x < 0
237 226 227 228 231 236 eliood x π π ¬ x = 0 ¬ 0 < x x π 0
238 71 120 72 ltleii 0 π
239 iooss2 π * 0 π π 0 π π
240 155 238 239 mp2an π 0 π π
241 240 sseli x π 0 x π π
242 2 reseq1i F π 0 = x if x mod T < π 1 1 π 0
243 ioossre π 0
244 resmpt π 0 x if x mod T < π 1 1 π 0 = x π 0 if x mod T < π 1 1
245 243 244 ax-mp x if x mod T < π 1 1 π 0 = x π 0 if x mod T < π 1 1
246 120 a1i x π 0 π
247 elioore x π 0 x
248 135 a1i x π 0 T +
249 247 248 modcld x π 0 x mod T
250 247 145 syl x π 0 x + T
251 56 2timesi 2 π = π + π
252 1 251 eqtri T = π + π
253 252 oveq2i - π + T = π + π + π
254 negpicn π
255 254 56 56 addassi π + π + π = π + π + π
256 255 eqcomi π + π + π = π + π + π
257 56 negidi π + π = 0
258 56 254 257 addcomli - π + π = 0
259 258 oveq1i π + π + π = 0 + π
260 56 addid2i 0 + π = π
261 259 260 eqtri π + π + π = π
262 253 256 261 3eqtrri π = - π + T
263 262 a1i x π 0 π = - π + T
264 160 a1i x π 0 π
265 122 a1i x π 0 T
266 241 230 syl x π 0 π < x
267 264 247 265 266 ltadd1dd x π 0 - π + T < x + T
268 263 267 eqbrtrd x π 0 π < x + T
269 246 250 268 ltled x π 0 π x + T
270 0red x π 0 0
271 160 122 readdcli - π + T
272 271 a1i x π 0 - π + T
273 72 a1i x π 0 0 < π
274 273 262 breqtrdi x π 0 0 < - π + T
275 270 272 250 274 267 lttrd x π 0 0 < x + T
276 270 250 275 ltled x π 0 0 x + T
277 247 recnd x π 0 x
278 123 a1i x π 0 T
279 277 278 addcomd x π 0 x + T = T + x
280 iooltub π * 0 * x π 0 x < 0
281 161 153 280 mp3an12 x π 0 x < 0
282 ltaddneg x T x < 0 T + x < T
283 247 122 282 sylancl x π 0 x < 0 T + x < T
284 281 283 mpbid x π 0 T + x < T
285 279 284 eqbrtrd x π 0 x + T < T
286 276 285 jca x π 0 0 x + T x + T < T
287 modid2 x + T T + x + T mod T = x + T 0 x + T x + T < T
288 250 135 287 sylancl x π 0 x + T mod T = x + T 0 x + T x + T < T
289 286 288 mpbird x π 0 x + T mod T = x + T
290 127 a1i x x + T mod T = x + 1 T mod T
291 135 a1i x T +
292 1zzd x 1
293 143 291 292 138 syl3anc x x + 1 T mod T = x mod T
294 290 293 eqtrd x x + T mod T = x mod T
295 247 294 syl x π 0 x + T mod T = x mod T
296 289 295 eqtr3d x π 0 x + T = x mod T
297 269 296 breqtrd x π 0 π x mod T
298 246 249 297 lensymd x π 0 ¬ x mod T < π
299 298 iffalsed x π 0 if x mod T < π 1 1 = 1
300 299 mpteq2ia x π 0 if x mod T < π 1 1 = x π 0 1
301 242 245 300 3eqtrri x π 0 1 = F π 0
302 301 oveq2i dx π 0 1 d x = D F π 0
303 iooretop π 0 topGen ran .
304 303 201 eleqtri π 0 TopOpen fld 𝑡
305 304 a1i π 0 TopOpen fld 𝑡
306 204 negcld 1
307 198 305 306 dvmptconst dx π 0 1 d x = x π 0 0
308 307 mptru dx π 0 1 d x = x π 0 0
309 dvresioo F : D F π 0 = F π 0
310 207 210 309 mp2an D F π 0 = F π 0
311 302 308 310 3eqtr3i x π 0 0 = F π 0
312 311 dmeqi dom x π 0 0 = dom F π 0
313 eqid x π 0 0 = x π 0 0
314 93 313 dmmpti dom x π 0 0 = π 0
315 312 314 eqtr3i dom F π 0 = π 0
316 ssdmres π 0 dom F dom F π 0 = π 0
317 315 316 mpbir π 0 dom F
318 317 sseli x π 0 x dom F
319 241 318 elind x π 0 x π π dom F
320 319 222 eleqtrrdi x π 0 x dom F π π
321 237 320 syl x π π ¬ x = 0 ¬ 0 < x x dom F π π
322 225 321 pm2.61dan x π π ¬ x = 0 x dom F π π
323 152 322 sylan x π π dom F π π ¬ x = 0 x dom F π π
324 eldifn x π π dom F π π ¬ x dom F π π
325 324 adantr x π π dom F π π ¬ x = 0 ¬ x dom F π π
326 323 325 condan x π π dom F π π x = 0
327 velsn x 0 x = 0
328 326 327 sylibr x π π dom F π π x 0
329 328 ssriv π π dom F π π 0
330 ssfi 0 Fin π π dom F π π 0 π π dom F π π Fin
331 151 329 330 mp2an π π dom F π π Fin
332 inss1 π π dom F π π
333 222 332 eqsstri dom F π π π π
334 ioosscn π π
335 333 334 sstri dom F π π
336 335 a1i dom F π π
337 dvf F : dom F
338 fresin F : dom F F π π : dom F π π
339 ffdm F π π : dom F π π F π π : dom F π π dom F π π dom F π π
340 337 338 339 mp2b F π π : dom F π π dom F π π dom F π π
341 340 simpli F π π : dom F π π
342 341 a1i F π π : dom F π π
343 161 a1i x dom F π π x < 0 π *
344 153 a1i x dom F π π x < 0 0 *
345 ioossre π π
346 333 sseli x dom F π π x π π
347 345 346 sseldi x dom F π π x
348 347 adantr x dom F π π x < 0 x
349 346 230 syl x dom F π π π < x
350 349 adantr x dom F π π x < 0 π < x
351 simpr x dom F π π x < 0 x < 0
352 343 344 348 350 351 eliood x dom F π π x < 0 x π 0
353 elun1 x π 0 x π 0 0 π
354 352 353 syl x dom F π π x < 0 x π 0 0 π
355 simpl x dom F π π ¬ x < 0 x dom F π π
356 0red x dom F π π ¬ x < 0 0
357 347 adantr x dom F π π ¬ x < 0 x
358 simpr x dom F π π ¬ x < 0 ¬ x < 0
359 356 357 358 nltled x dom F π π ¬ x < 0 0 x
360 id x = 0 x = 0
361 207 a1i
362 eqid topGen ran . = topGen ran .
363 210 a1i F :
364 0red 0
365 mnfxr −∞ *
366 365 a1i −∞ *
367 364 mnfltd −∞ < 0
368 362 366 364 367 lptioo2 0 limPt topGen ran . −∞ 0
369 incom −∞ 0 = −∞ 0
370 ioossre −∞ 0
371 df-ss −∞ 0 −∞ 0 = −∞ 0
372 370 371 mpbi −∞ 0 = −∞ 0
373 369 372 eqtr2i −∞ 0 = −∞ 0
374 373 fveq2i limPt topGen ran . −∞ 0 = limPt topGen ran . −∞ 0
375 368 374 eleqtrdi 0 limPt topGen ran . −∞ 0
376 pnfxr +∞ *
377 376 a1i +∞ *
378 364 ltpnfd 0 < +∞
379 362 364 377 378 lptioo1 0 limPt topGen ran . 0 +∞
380 incom 0 +∞ = 0 +∞
381 ioossre 0 +∞
382 df-ss 0 +∞ 0 +∞ = 0 +∞
383 381 382 mpbi 0 +∞ = 0 +∞
384 380 383 eqtr2i 0 +∞ = 0 +∞
385 384 fveq2i limPt topGen ran . 0 +∞ = limPt topGen ran . 0 +∞
386 379 385 eleqtrdi 0 limPt topGen ran . 0 +∞
387 eqid x π 0 1 = x π 0 1
388 mnfle π * −∞ π
389 161 388 ax-mp −∞ π
390 iooss1 −∞ * −∞ π π 0 −∞ 0
391 365 389 390 mp2an π 0 −∞ 0
392 391 a1i π 0 −∞ 0
393 ioosscn −∞ 0
394 392 393 sstrdi π 0
395 0cnd 0
396 387 394 306 395 constlimc 1 x π 0 1 lim 0
397 resabs1 π 0 −∞ 0 F −∞ 0 π 0 = F π 0
398 391 397 ax-mp F −∞ 0 π 0 = F π 0
399 301 398 eqtr4i x π 0 1 = F −∞ 0 π 0
400 399 oveq1i x π 0 1 lim 0 = F −∞ 0 π 0 lim 0
401 fssres F : −∞ 0 F −∞ 0 : −∞ 0
402 210 370 401 mp2an F −∞ 0 : −∞ 0
403 402 a1i F −∞ 0 : −∞ 0
404 393 a1i −∞ 0
405 eqid TopOpen fld 𝑡 −∞ 0 0 = TopOpen fld 𝑡 −∞ 0 0
406 0le0 0 0
407 elioc2 π * 0 0 π 0 0 π < 0 0 0
408 161 71 407 mp2an 0 π 0 0 π < 0 0 0
409 71 166 406 408 mpbir3an 0 π 0
410 200 cnfldtop TopOpen fld Top
411 ovex −∞ 0 V
412 resttop TopOpen fld Top −∞ 0 V TopOpen fld 𝑡 −∞ 0 Top
413 410 411 412 mp2an TopOpen fld 𝑡 −∞ 0 Top
414 161 a1i π *
415 eqid topGen ran . 𝑡 −∞ 0 = topGen ran . 𝑡 −∞ 0
416 389 a1i −∞ π
417 366 414 364 362 415 416 364 iocopn π 0 topGen ran . 𝑡 −∞ 0
418 417 mptru π 0 topGen ran . 𝑡 −∞ 0
419 201 oveq1i topGen ran . 𝑡 −∞ 0 = TopOpen fld 𝑡 𝑡 −∞ 0
420 iocssre −∞ * 0 −∞ 0
421 365 71 420 mp2an −∞ 0
422 197 elexi V
423 restabs TopOpen fld Top −∞ 0 V TopOpen fld 𝑡 𝑡 −∞ 0 = TopOpen fld 𝑡 −∞ 0
424 410 421 422 423 mp3an TopOpen fld 𝑡 𝑡 −∞ 0 = TopOpen fld 𝑡 −∞ 0
425 419 424 eqtri topGen ran . 𝑡 −∞ 0 = TopOpen fld 𝑡 −∞ 0
426 418 425 eleqtri π 0 TopOpen fld 𝑡 −∞ 0
427 isopn3i TopOpen fld 𝑡 −∞ 0 Top π 0 TopOpen fld 𝑡 −∞ 0 int TopOpen fld 𝑡 −∞ 0 π 0 = π 0
428 413 426 427 mp2an int TopOpen fld 𝑡 −∞ 0 π 0 = π 0
429 mnflt0 −∞ < 0
430 ioounsn −∞ * 0 * −∞ < 0 −∞ 0 0 = −∞ 0
431 365 153 429 430 mp3an −∞ 0 0 = −∞ 0
432 431 eqcomi −∞ 0 = −∞ 0 0
433 432 oveq2i TopOpen fld 𝑡 −∞ 0 = TopOpen fld 𝑡 −∞ 0 0
434 433 fveq2i int TopOpen fld 𝑡 −∞ 0 = int TopOpen fld 𝑡 −∞ 0 0
435 ioounsn π * 0 * π < 0 π 0 0 = π 0
436 161 153 166 435 mp3an π 0 0 = π 0
437 436 eqcomi π 0 = π 0 0
438 434 437 fveq12i int TopOpen fld 𝑡 −∞ 0 π 0 = int TopOpen fld 𝑡 −∞ 0 0 π 0 0
439 428 438 eqtr3i π 0 = int TopOpen fld 𝑡 −∞ 0 0 π 0 0
440 409 439 eleqtri 0 int TopOpen fld 𝑡 −∞ 0 0 π 0 0
441 440 a1i 0 int TopOpen fld 𝑡 −∞ 0 0 π 0 0
442 403 392 404 200 405 441 limcres F −∞ 0 π 0 lim 0 = F −∞ 0 lim 0
443 442 mptru F −∞ 0 π 0 lim 0 = F −∞ 0 lim 0
444 400 443 eqtri x π 0 1 lim 0 = F −∞ 0 lim 0
445 396 444 eleqtrdi 1 F −∞ 0 lim 0
446 eqid x 0 π 1 = x 0 π 1
447 ioosscn 0 π
448 447 a1i 0 π
449 446 448 204 395 constlimc 1 x 0 π 1 lim 0
450 ltpnf π π < +∞
451 xrltle π * +∞ * π < +∞ π +∞
452 155 376 451 mp2an π < +∞ π +∞
453 120 450 452 mp2b π +∞
454 iooss2 +∞ * π +∞ 0 π 0 +∞
455 376 453 454 mp2an 0 π 0 +∞
456 resabs1 0 π 0 +∞ F 0 +∞ 0 π = F 0 π
457 455 456 ax-mp F 0 +∞ 0 π = F 0 π
458 195 457 eqtr4i x 0 π 1 = F 0 +∞ 0 π
459 458 oveq1i x 0 π 1 lim 0 = F 0 +∞ 0 π lim 0
460 fssres F : 0 +∞ F 0 +∞ : 0 +∞
461 210 381 460 mp2an F 0 +∞ : 0 +∞
462 461 a1i F 0 +∞ : 0 +∞
463 455 a1i 0 π 0 +∞
464 ioosscn 0 +∞
465 464 a1i 0 +∞
466 eqid TopOpen fld 𝑡 0 +∞ 0 = TopOpen fld 𝑡 0 +∞ 0
467 elico2 0 π * 0 0 π 0 0 0 0 < π
468 71 155 467 mp2an 0 0 π 0 0 0 0 < π
469 71 406 72 468 mpbir3an 0 0 π
470 ovex 0 +∞ V
471 resttop TopOpen fld Top 0 +∞ V TopOpen fld 𝑡 0 +∞ Top
472 410 470 471 mp2an TopOpen fld 𝑡 0 +∞ Top
473 155 a1i π *
474 eqid topGen ran . 𝑡 0 +∞ = topGen ran . 𝑡 0 +∞
475 453 a1i π +∞
476 364 473 377 362 474 475 icoopn 0 π topGen ran . 𝑡 0 +∞
477 476 mptru 0 π topGen ran . 𝑡 0 +∞
478 201 oveq1i topGen ran . 𝑡 0 +∞ = TopOpen fld 𝑡 𝑡 0 +∞
479 rge0ssre 0 +∞
480 restabs TopOpen fld Top 0 +∞ V TopOpen fld 𝑡 𝑡 0 +∞ = TopOpen fld 𝑡 0 +∞
481 410 479 422 480 mp3an TopOpen fld 𝑡 𝑡 0 +∞ = TopOpen fld 𝑡 0 +∞
482 478 481 eqtri topGen ran . 𝑡 0 +∞ = TopOpen fld 𝑡 0 +∞
483 477 482 eleqtri 0 π TopOpen fld 𝑡 0 +∞
484 isopn3i TopOpen fld 𝑡 0 +∞ Top 0 π TopOpen fld 𝑡 0 +∞ int TopOpen fld 𝑡 0 +∞ 0 π = 0 π
485 472 483 484 mp2an int TopOpen fld 𝑡 0 +∞ 0 π = 0 π
486 0ltpnf 0 < +∞
487 snunioo1 0 * +∞ * 0 < +∞ 0 +∞ 0 = 0 +∞
488 153 376 486 487 mp3an 0 +∞ 0 = 0 +∞
489 488 eqcomi 0 +∞ = 0 +∞ 0
490 489 oveq2i TopOpen fld 𝑡 0 +∞ = TopOpen fld 𝑡 0 +∞ 0
491 490 fveq2i int TopOpen fld 𝑡 0 +∞ = int TopOpen fld 𝑡 0 +∞ 0
492 snunioo1 0 * π * 0 < π 0 π 0 = 0 π
493 153 155 72 492 mp3an 0 π 0 = 0 π
494 493 eqcomi 0 π = 0 π 0
495 491 494 fveq12i int TopOpen fld 𝑡 0 +∞ 0 π = int TopOpen fld 𝑡 0 +∞ 0 0 π 0
496 485 495 eqtr3i 0 π = int TopOpen fld 𝑡 0 +∞ 0 0 π 0
497 469 496 eleqtri 0 int TopOpen fld 𝑡 0 +∞ 0 0 π 0
498 497 a1i 0 int TopOpen fld 𝑡 0 +∞ 0 0 π 0
499 462 463 465 200 466 498 limcres F 0 +∞ 0 π lim 0 = F 0 +∞ lim 0
500 499 mptru F 0 +∞ 0 π lim 0 = F 0 +∞ lim 0
501 459 500 eqtri x 0 π 1 lim 0 = F 0 +∞ lim 0
502 449 501 eleqtrdi 1 F 0 +∞ lim 0
503 neg1lt0 1 < 0
504 109 71 108 lttri 1 < 0 0 < 1 1 < 1
505 503 38 504 mp2an 1 < 1
506 109 505 ltneii 1 1
507 506 a1i 1 1
508 200 361 362 363 364 375 386 445 502 507 jumpncnp ¬ F topGen ran . CnP TopOpen fld 0
509 508 mptru ¬ F topGen ran . CnP TopOpen fld 0
510 208 a1i 0 dom F π π
511 210 a1i 0 dom F π π F :
512 207 a1i 0 dom F π π
513 inss2 π π dom F dom F
514 222 513 eqsstri dom F π π dom F
515 514 sseli 0 dom F π π 0 dom F
516 201 200 dvcnp2 F : 0 dom F F topGen ran . CnP TopOpen fld 0
517 510 511 512 515 516 syl31anc 0 dom F π π F topGen ran . CnP TopOpen fld 0
518 509 517 mto ¬ 0 dom F π π
519 518 a1i x = 0 ¬ 0 dom F π π
520 360 519 eqneltrd x = 0 ¬ x dom F π π
521 520 necon2ai x dom F π π x 0
522 521 adantr x dom F π π ¬ x < 0 x 0
523 356 357 359 522 leneltd x dom F π π ¬ x < 0 0 < x
524 346 165 sylan x dom F π π 0 < x x 0 π
525 elun2 x 0 π x π 0 0 π
526 524 525 syl x dom F π π 0 < x x π 0 0 π
527 355 523 526 syl2anc x dom F π π ¬ x < 0 x π 0 0 π
528 354 527 pm2.61dan x dom F π π x π 0 0 π
529 ovex π 0 V
530 ovex 0 π V
531 529 530 unipr π 0 0 π = π 0 0 π
532 528 531 eleqtrrdi x dom F π π x π 0 0 π
533 532 ssriv dom F π π π 0 0 π
534 533 a1i dom F π π π 0 0 π
535 ineq2 x = π 0 dom F π π x = dom F π π π 0
536 retop topGen ran . Top
537 ovex D F V
538 537 resex F π π V
539 538 dmex dom F π π V
540 536 539 pm3.2i topGen ran . Top dom F π π V
541 320 ssriv π 0 dom F π π
542 ssid π 0 π 0
543 303 541 542 3pm3.2i π 0 topGen ran . π 0 dom F π π π 0 π 0
544 restopnb topGen ran . Top dom F π π V π 0 topGen ran . π 0 dom F π π π 0 π 0 π 0 topGen ran . π 0 topGen ran . 𝑡 dom F π π
545 540 543 544 mp2an π 0 topGen ran . π 0 topGen ran . 𝑡 dom F π π
546 303 545 mpbi π 0 topGen ran . 𝑡 dom F π π
547 inss2 dom F π π π 0 π 0
548 541 542 ssini π 0 dom F π π π 0
549 547 548 eqssi dom F π π π 0 = π 0
550 201 oveq1i topGen ran . 𝑡 dom F π π = TopOpen fld 𝑡 𝑡 dom F π π
551 333 345 sstri dom F π π
552 restabs TopOpen fld Top dom F π π V TopOpen fld 𝑡 𝑡 dom F π π = TopOpen fld 𝑡 dom F π π
553 410 551 422 552 mp3an TopOpen fld 𝑡 𝑡 dom F π π = TopOpen fld 𝑡 dom F π π
554 550 553 eqtr2i TopOpen fld 𝑡 dom F π π = topGen ran . 𝑡 dom F π π
555 546 549 554 3eltr4i dom F π π π 0 TopOpen fld 𝑡 dom F π π
556 535 555 eqeltrdi x = π 0 dom F π π x TopOpen fld 𝑡 dom F π π
557 556 adantl x π 0 0 π x = π 0 dom F π π x TopOpen fld 𝑡 dom F π π
558 neqne ¬ x = π 0 x π 0
559 elprn1 x π 0 0 π x π 0 x = 0 π
560 558 559 sylan2 x π 0 0 π ¬ x = π 0 x = 0 π
561 ineq2 x = 0 π dom F π π x = dom F π π 0 π
562 223 ssriv 0 π dom F π π
563 ssid 0 π 0 π
564 199 562 563 3pm3.2i 0 π topGen ran . 0 π dom F π π 0 π 0 π
565 restopnb topGen ran . Top dom F π π V 0 π topGen ran . 0 π dom F π π 0 π 0 π 0 π topGen ran . 0 π topGen ran . 𝑡 dom F π π
566 540 564 565 mp2an 0 π topGen ran . 0 π topGen ran . 𝑡 dom F π π
567 199 566 mpbi 0 π topGen ran . 𝑡 dom F π π
568 inss2 dom F π π 0 π 0 π
569 562 563 ssini 0 π dom F π π 0 π
570 568 569 eqssi dom F π π 0 π = 0 π
571 567 570 554 3eltr4i dom F π π 0 π TopOpen fld 𝑡 dom F π π
572 561 571 eqeltrdi x = 0 π dom F π π x TopOpen fld 𝑡 dom F π π
573 560 572 syl x π 0 0 π ¬ x = π 0 dom F π π x TopOpen fld 𝑡 dom F π π
574 557 573 pm2.61dan x π 0 0 π dom F π π x TopOpen fld 𝑡 dom F π π
575 574 adantl x π 0 0 π dom F π π x TopOpen fld 𝑡 dom F π π
576 ssid
577 576 a1i
578 394 395 577 constcncfg x π 0 0 : π 0 cn
579 578 mptru x π 0 0 : π 0 cn
580 579 a1i x = π 0 x π 0 0 : π 0 cn
581 reseq2 x = π 0 F π π x = F π π π 0
582 resabs1 π 0 π π F π π π 0 = F π 0
583 240 582 ax-mp F π π π 0 = F π 0
584 583 311 eqtr4i F π π π 0 = x π 0 0
585 581 584 eqtrdi x = π 0 F π π x = x π 0 0
586 535 549 eqtrdi x = π 0 dom F π π x = π 0
587 586 oveq1d x = π 0 dom F π π x cn = π 0 cn
588 580 585 587 3eltr4d x = π 0 F π π x : dom F π π x cn
589 588 adantl x π 0 0 π x = π 0 F π π x : dom F π π x cn
590 448 395 577 constcncfg x 0 π 0 : 0 π cn
591 590 mptru x 0 π 0 : 0 π cn
592 591 a1i x = 0 π x 0 π 0 : 0 π cn
593 reseq2 x = 0 π F π π x = F π π 0 π
594 resabs1 0 π π π F π π 0 π = F 0 π
595 169 594 ax-mp F π π 0 π = F 0 π
596 595 213 eqtr4i F π π 0 π = x 0 π 0
597 593 596 eqtrdi x = 0 π F π π x = x 0 π 0
598 561 570 eqtrdi x = 0 π dom F π π x = 0 π
599 598 oveq1d x = 0 π dom F π π x cn = 0 π cn
600 592 597 599 3eltr4d x = 0 π F π π x : dom F π π x cn
601 560 600 syl x π 0 0 π ¬ x = π 0 F π π x : dom F π π x cn
602 589 601 pm2.61dan x π 0 0 π F π π x : dom F π π x cn
603 602 adantl x π 0 0 π F π π x : dom F π π x cn
604 336 342 534 575 603 cncfuni F π π : dom F π π cn
605 604 mptru F π π : dom F π π cn
606 oveq1 x = π x +∞ = π +∞
607 606 reseq2d x = π F π π x +∞ = F π π π +∞
608 iooss2 +∞ * π +∞ π π π +∞
609 376 453 608 mp2an π π π +∞
610 resabs2 π π π +∞ F π π π +∞ = F π π
611 609 610 ax-mp F π π π +∞ = F π π
612 607 611 eqtrdi x = π F π π x +∞ = F π π
613 id x = π x = π
614 612 613 oveq12d x = π F π π x +∞ lim x = F π π lim π
615 254 a1i π
616 313 394 395 615 constlimc 0 x π 0 0 lim π
617 616 mptru 0 x π 0 0 lim π
618 311 oveq1i x π 0 0 lim π = F π 0 lim π
619 337 a1i F : dom F
620 160 a1i π
621 153 a1i 0 *
622 166 a1i π < 0
623 317 a1i π 0 dom F
624 238 a1i 0 π
625 619 620 621 622 623 473 624 limcresioolb F π 0 lim π = F π π lim π
626 625 mptru F π 0 lim π = F π π lim π
627 618 626 eqtri x π 0 0 lim π = F π π lim π
628 617 627 eleqtri 0 F π π lim π
629 628 ne0ii F π π lim π
630 629 a1i x = π F π π lim π
631 614 630 eqnetrd x = π F π π x +∞ lim x
632 631 adantl x π π dom F π π x = π F π π x +∞ lim x
633 eldifi x π π dom F π π x π π
634 161 a1i x π π ¬ x = π π *
635 155 a1i x π π ¬ x = π π *
636 icossre π π * π π
637 160 155 636 mp2an π π
638 637 sseli x π π x
639 638 adantr x π π ¬ x = π x
640 160 a1i x π π ¬ x = π π
641 icogelb π * π * x π π π x
642 161 155 641 mp3an12 x π π π x
643 642 adantr x π π ¬ x = π π x
644 neqne ¬ x = π x π
645 644 adantl x π π ¬ x = π x π
646 640 639 643 645 leneltd x π π ¬ x = π π < x
647 icoltub π * π * x π π x < π
648 161 155 647 mp3an12 x π π x < π
649 648 adantr x π π ¬ x = π x < π
650 634 635 639 646 649 eliood x π π ¬ x = π x π π
651 633 650 sylan x π π dom F π π ¬ x = π x π π
652 eldifn x π π dom F π π ¬ x dom F π π
653 652 adantr x π π dom F π π ¬ x = π ¬ x dom F π π
654 651 653 eldifd x π π dom F π π ¬ x = π x π π dom F π π
655 oveq1 x = 0 x +∞ = 0 +∞
656 655 reseq2d x = 0 F π π x +∞ = F π π 0 +∞
657 656 360 oveq12d x = 0 F π π x +∞ lim x = F π π 0 +∞ lim 0
658 215 448 395 395 constlimc 0 x 0 π 0 lim 0
659 658 mptru 0 x 0 π 0 lim 0
660 resres F π π 0 +∞ = F π π 0 +∞
661 iooin π * π * 0 * +∞ * π π 0 +∞ = if π 0 0 π if π +∞ π +∞
662 161 155 153 376 661 mp4an π π 0 +∞ = if π 0 0 π if π +∞ π +∞
663 167 iftruei if π 0 0 π = 0
664 453 iftruei if π +∞ π +∞ = π
665 663 664 oveq12i if π 0 0 π if π +∞ π +∞ = 0 π
666 662 665 eqtri π π 0 +∞ = 0 π
667 666 reseq2i F π π 0 +∞ = F 0 π
668 213 eqcomi F 0 π = x 0 π 0
669 660 667 668 3eqtrri x 0 π 0 = F π π 0 +∞
670 669 oveq1i x 0 π 0 lim 0 = F π π 0 +∞ lim 0
671 659 670 eleqtri 0 F π π 0 +∞ lim 0
672 671 ne0ii F π π 0 +∞ lim 0
673 672 a1i x = 0 F π π 0 +∞ lim 0
674 657 673 eqnetrd x = 0 F π π x +∞ lim x
675 654 326 674 3syl x π π dom F π π ¬ x = π F π π x +∞ lim x
676 632 675 pm2.61dan x π π dom F π π F π π x +∞ lim x
677 oveq2 x = π −∞ x = −∞ π
678 677 reseq2d x = π F π π −∞ x = F π π −∞ π
679 id x = π x = π
680 678 679 oveq12d x = π F π π −∞ x lim x = F π π −∞ π lim π
681 iooss1 −∞ * −∞ π π π −∞ π
682 365 389 681 mp2an π π −∞ π
683 resabs2 π π −∞ π F π π −∞ π = F π π
684 682 683 ax-mp F π π −∞ π = F π π
685 684 oveq1i F π π −∞ π lim π = F π π lim π
686 680 685 eqtrdi x = π F π π −∞ x lim x = F π π lim π
687 215 448 395 57 constlimc 0 x 0 π 0 lim π
688 687 mptru 0 x 0 π 0 lim π
689 213 oveq1i x 0 π 0 lim π = F 0 π lim π
690 120 a1i π
691 72 a1i 0 < π
692 219 a1i 0 π dom F
693 167 a1i π 0
694 619 621 690 691 692 414 693 limcresiooub F 0 π lim π = F π π lim π
695 694 mptru F 0 π lim π = F π π lim π
696 689 695 eqtri x 0 π 0 lim π = F π π lim π
697 688 696 eleqtri 0 F π π lim π
698 697 ne0ii F π π lim π
699 698 a1i x = π F π π lim π
700 686 699 eqnetrd x = π F π π −∞ x lim x
701 700 adantl x π π dom F π π x = π F π π −∞ x lim x
702 161 a1i x π π dom F π π ¬ x = π π *
703 155 a1i x π π dom F π π ¬ x = π π *
704 negpitopissre π π
705 eldifi x π π dom F π π x π π
706 704 705 sseldi x π π dom F π π x
707 706 adantr x π π dom F π π ¬ x = π x
708 161 a1i x π π dom F π π π *
709 155 a1i x π π dom F π π π *
710 iocgtlb π * π * x π π π < x
711 708 709 705 710 syl3anc x π π dom F π π π < x
712 711 adantr x π π dom F π π ¬ x = π π < x
713 120 a1i x π π dom F π π ¬ x = π π
714 iocleub π * π * x π π x π
715 708 709 705 714 syl3anc x π π dom F π π x π
716 715 adantr x π π dom F π π ¬ x = π x π
717 id π = x π = x
718 717 eqcomd π = x x = π
719 718 necon3bi ¬ x = π π x
720 719 adantl x π π dom F π π ¬ x = π π x
721 707 713 716 720 leneltd x π π dom F π π ¬ x = π x < π
722 702 703 707 712 721 eliood x π π dom F π π ¬ x = π x π π
723 eldifn x π π dom F π π ¬ x dom F π π
724 723 adantr x π π dom F π π ¬ x = π ¬ x dom F π π
725 722 724 eldifd x π π dom F π π ¬ x = π x π π dom F π π
726 oveq2 x = 0 −∞ x = −∞ 0
727 726 reseq2d x = 0 F π π −∞ x = F π π −∞ 0
728 727 360 oveq12d x = 0 F π π −∞ x lim x = F π π −∞ 0 lim 0
729 313 394 395 395 constlimc 0 x π 0 0 lim 0
730 729 mptru 0 x π 0 0 lim 0
731 resres F π π −∞ 0 = F π π −∞ 0
732 iooin π * π * −∞ * 0 * π π −∞ 0 = if π −∞ −∞ π if π 0 π 0
733 161 155 365 153 732 mp4an π π −∞ 0 = if π −∞ −∞ π if π 0 π 0
734 mnflt π −∞ < π
735 160 734 ax-mp −∞ < π
736 xrltnle −∞ * π * −∞ < π ¬ π −∞
737 365 161 736 mp2an −∞ < π ¬ π −∞
738 735 737 mpbi ¬ π −∞
739 738 iffalsei if π −∞ −∞ π = π
740 xrltnle 0 * π * 0 < π ¬ π 0
741 153 155 740 mp2an 0 < π ¬ π 0
742 72 741 mpbi ¬ π 0
743 742 iffalsei if π 0 π 0 = 0
744 739 743 oveq12i if π −∞ −∞ π if π 0 π 0 = π 0
745 733 744 eqtri π π −∞ 0 = π 0
746 745 reseq2i F π π −∞ 0 = F π 0
747 311 eqcomi F π 0 = x π 0 0
748 731 746 747 3eqtrri x π 0 0 = F π π −∞ 0
749 748 oveq1i x π 0 0 lim 0 = F π π −∞ 0 lim 0
750 730 749 eleqtri 0 F π π −∞ 0 lim 0
751 750 ne0ii F π π −∞ 0 lim 0
752 751 a1i x = 0 F π π −∞ 0 lim 0
753 728 752 eqnetrd x = 0 F π π −∞ x lim x
754 725 326 753 3syl x π π dom F π π ¬ x = π F π π −∞ x lim x
755 701 754 pm2.61dan x π π dom F π π F π π −∞ x lim x
756 eqid x X X mod T X 1 = x X X mod T X 1
757 ioosscn X X mod T X
758 757 a1i X mod T 0 π X X mod T X
759 1cnd X mod T 0 π 1
760 27 a1i X mod T 0 π X
761 756 758 759 760 constlimc X mod T 0 π 1 x X X mod T X 1 lim X
762 ioossioc 0 π 0 π
763 762 sseli X mod T 0 π X mod T 0 π
764 763 iftrued X mod T 0 π if X mod T 0 π 1 1 = 1
765 210 a1i X mod T 0 π F :
766 modcl X T + X mod T
767 3 135 766 mp2an X mod T
768 3 767 resubcli X X mod T
769 768 rexri X X mod T *
770 769 a1i X mod T 0 π X X mod T *
771 3 a1i X mod T 0 π X
772 elioore X mod T 0 π X mod T
773 ioogtlb 0 * π * X mod T 0 π 0 < X mod T
774 153 155 773 mp3an12 X mod T 0 π 0 < X mod T
775 772 774 elrpd X mod T 0 π X mod T +
776 771 775 ltsubrpd X mod T 0 π X X mod T < X
777 ioossre X X mod T X
778 777 a1i X mod T 0 π X X mod T X
779 365 a1i X mod T 0 π −∞ *
780 mnflt X X mod T −∞ < X X mod T
781 xrltle −∞ * X X mod T * −∞ < X X mod T −∞ X X mod T
782 365 769 781 mp2an −∞ < X X mod T −∞ X X mod T
783 768 780 782 mp2b −∞ X X mod T
784 783 a1i X mod T 0 π −∞ X X mod T
785 765 770 771 776 778 779 784 limcresiooub X mod T 0 π F X X mod T X lim X = F −∞ X lim X
786 iooltub 0 * π * X mod T 0 π X mod T < π
787 153 155 786 mp3an12 X mod T 0 π X mod T < π
788 210 a1i X mod T < π F :
789 777 a1i X mod T < π X X mod T X
790 788 789 feqresmpt X mod T < π F X X mod T X = x X X mod T X F x
791 elioore x X X mod T X x
792 791 110 147 sylancl x X X mod T X F x = if x mod T < π 1 1
793 792 adantl X mod T < π x X X mod T X F x = if x mod T < π 1 1
794 791 adantl X mod T < π x X X mod T X x
795 135 a1i X mod T < π x X X mod T X T +
796 794 795 modcld X mod T < π x X X mod T X x mod T
797 767 a1i X mod T < π x X X mod T X X mod T
798 120 a1i X mod T < π x X X mod T X π
799 3 a1i x X X mod T X X
800 135 a1i x X X mod T X T +
801 ioossico X X mod T X X X mod T X
802 801 sseli x X X mod T X x X X mod T X
803 799 800 802 ltmod x X X mod T X x mod T < X mod T
804 803 adantl X mod T < π x X X mod T X x mod T < X mod T
805 simpl X mod T < π x X X mod T X X mod T < π
806 796 797 798 804 805 lttrd X mod T < π x X X mod T X x mod T < π
807 806 iftrued X mod T < π x X X mod T X if x mod T < π 1 1 = 1
808 793 807 eqtrd X mod T < π x X X mod T X F x = 1
809 808 mpteq2dva X mod T < π x X X mod T X F x = x X X mod T X 1
810 790 809 eqtrd X mod T < π F X X mod T X = x X X mod T X 1
811 787 810 syl X mod T 0 π F X X mod T X = x X X mod T X 1
812 811 oveq1d X mod T 0 π F X X mod T X lim X = x X X mod T X 1 lim X
813 785 812 eqtr3d X mod T 0 π F −∞ X lim X = x X X mod T X 1 lim X
814 761 764 813 3eltr4d X mod T 0 π if X mod T 0 π 1 1 F −∞ X lim X
815 eqid x X π X 1 = x X π X 1
816 ioossre X π X
817 816 a1i X π X
818 817 208 sstrdi X π X
819 27 a1i X
820 815 818 306 819 constlimc 1 x X π X 1 lim X
821 820 mptru 1 x X π X 1 lim X
822 821 a1i X mod T = 0 1 x X π X 1 lim X
823 id X mod T = 0 X mod T = 0
824 lbioc ¬ 0 0 π
825 824 a1i X mod T = 0 ¬ 0 0 π
826 823 825 eqneltrd X mod T = 0 ¬ X mod T 0 π
827 826 iffalsed X mod T = 0 if X mod T 0 π 1 1 = 1
828 210 a1i X mod T = 0 F :
829 816 a1i X mod T = 0 X π X
830 828 829 feqresmpt X mod T = 0 F X π X = x X π X F x
831 829 sselda X mod T = 0 x X π X x
832 831 110 147 sylancl X mod T = 0 x X π X F x = if x mod T < π 1 1
833 120 a1i X mod T = 0 x X π X π
834 135 a1i X mod T = 0 x X π X T +
835 831 834 modcld X mod T = 0 x X π X x mod T
836 3 120 resubcli X π
837 836 a1i x X π X X π
838 122 a1i x X π X T
839 837 838 readdcld x X π X X - π + T
840 elioore x X π X x
841 840 838 readdcld x X π X x + T
842 3 a1i x X π X X
843 836 rexri X π *
844 843 a1i x X π X X π *
845 842 rexrd x X π X X *
846 id x X π X x X π X
847 ioogtlb X π * X * x X π X X π < x
848 844 845 846 847 syl3anc x X π X X π < x
849 837 840 838 848 ltadd1dd x X π X X - π + T < x + T
850 839 841 842 849 ltsub1dd x X π X X π + T - X < x + T - X
851 850 adantl X mod T = 0 x X π X X π + T - X < x + T - X
852 252 oveq2i X - π + T = X π + π + π
853 56 56 addcli π + π
854 subadd23 X π π + π X π + π + π = X + π + π - π
855 27 56 853 854 mp3an X π + π + π = X + π + π - π
856 56 56 pncan3oi π + π - π = π
857 856 oveq2i X + π + π - π = X + π
858 852 855 857 3eqtri X - π + T = X + π
859 858 oveq1i X π + T - X = X + π - X
860 pncan2 X π X + π - X = π
861 27 56 860 mp2an X + π - X = π
862 859 861 eqtr2i π = X π + T - X
863 862 a1i X mod T = 0 x X π X π = X π + T - X
864 841 842 resubcld x X π X x + T - X
865 modabs2 x + T - X T + x + T - X mod T mod T = x + T - X mod T
866 864 135 865 sylancl x X π X x + T - X mod T mod T = x + T - X mod T
867 135 a1i x X π X T +
868 0red x X π X 0
869 839 842 resubcld x X π X X π + T - X
870 72 862 breqtri 0 < X π + T - X
871 870 a1i x X π X 0 < X π + T - X
872 868 869 864 871 850 lttrd x X π X 0 < x + T - X
873 868 864 872 ltled x X π X 0 x + T - X
874 842 838 readdcld x X π X X + T
875 iooltub X π * X * x X π X x < X
876 844 845 846 875 syl3anc x X π X x < X
877 840 842 838 876 ltadd1dd x X π X x + T < X + T
878 841 874 842 877 ltsub1dd x X π X x + T - X < X + T - X
879 pncan2 X T X + T - X = T
880 27 123 879 mp2an X + T - X = T
881 878 880 breqtrdi x X π X x + T - X < T
882 modid x + T - X T + 0 x + T - X x + T - X < T x + T - X mod T = x + T - X
883 864 867 873 881 882 syl22anc x X π X x + T - X mod T = x + T - X
884 866 883 eqtr2d x X π X x + T - X = x + T - X mod T mod T
885 884 adantl X mod T = 0 x X π X x + T - X = x + T - X mod T mod T
886 oveq2 X mod T = 0 x + T - X mod T + X mod T = x + T - X mod T + 0
887 886 adantr X mod T = 0 x X π X x + T - X mod T + X mod T = x + T - X mod T + 0
888 864 867 modcld x X π X x + T - X mod T
889 888 recnd x X π X x + T - X mod T
890 889 addid1d x X π X x + T - X mod T + 0 = x + T - X mod T
891 890 adantl X mod T = 0 x X π X x + T - X mod T + 0 = x + T - X mod T
892 887 891 eqtr2d X mod T = 0 x X π X x + T - X mod T = x + T - X mod T + X mod T
893 892 oveq1d X mod T = 0 x X π X x + T - X mod T mod T = x + T - X mod T + X mod T mod T
894 modaddabs x + T - X X T + x + T - X mod T + X mod T mod T = x + T - X + X mod T
895 864 842 867 894 syl3anc x X π X x + T - X mod T + X mod T mod T = x + T - X + X mod T
896 895 adantl X mod T = 0 x X π X x + T - X mod T + X mod T mod T = x + T - X + X mod T
897 885 893 896 3eqtrd X mod T = 0 x X π X x + T - X = x + T - X + X mod T
898 145 recnd x x + T
899 27 a1i x X
900 898 899 npcand x x + T - X + X = x + T
901 124 a1i x 1 T = T
902 901 oveq2d x x + 1 T = x + T
903 900 902 eqtr4d x x + T - X + X = x + 1 T
904 903 oveq1d x x + T - X + X mod T = x + 1 T mod T
905 840 904 syl x X π X x + T - X + X mod T = x + 1 T mod T
906 905 adantl X mod T = 0 x X π X x + T - X + X mod T = x + 1 T mod T
907 1zzd X mod T = 0 x X π X 1
908 831 834 907 138 syl3anc X mod T = 0 x X π X x + 1 T mod T = x mod T
909 897 906 908 3eqtrrd X mod T = 0 x X π X x mod T = x + T - X
910 851 863 909 3brtr4d X mod T = 0 x X π X π < x mod T
911 833 835 910 ltled X mod T = 0 x X π X π x mod T
912 833 835 911 lensymd X mod T = 0 x X π X ¬ x mod T < π
913 912 iffalsed X mod T = 0 x X π X if x mod T < π 1 1 = 1
914 832 913 eqtrd X mod T = 0 x X π X F x = 1
915 914 mpteq2dva X mod T = 0 x X π X F x = x X π X 1
916 830 915 eqtr2d X mod T = 0 x X π X 1 = F X π X
917 916 oveq1d X mod T = 0 x X π X 1 lim X = F X π X lim X
918 843 a1i X π *
919 3 a1i X
920 ltsubrp X π + X π < X
921 3 184 920 mp2an X π < X
922 921 a1i X π < X
923 mnflt X π −∞ < X π
924 xrltle −∞ * X π * −∞ < X π −∞ X π
925 365 843 924 mp2an −∞ < X π −∞ X π
926 836 923 925 mp2b −∞ X π
927 926 a1i −∞ X π
928 363 918 919 922 817 366 927 limcresiooub F X π X lim X = F −∞ X lim X
929 928 mptru F X π X lim X = F −∞ X lim X
930 917 929 eqtr2di X mod T = 0 F −∞ X lim X = x X π X 1 lim X
931 822 827 930 3eltr4d X mod T = 0 if X mod T 0 π 1 1 F −∞ X lim X
932 931 adantl ¬ X mod T 0 π X mod T = 0 if X mod T 0 π 1 1 F −∞ X lim X
933 155 a1i ¬ X mod T 0 π ¬ X mod T = 0 π *
934 122 rexri T *
935 934 a1i ¬ X mod T 0 π ¬ X mod T = 0 T *
936 767 rexri X mod T *
937 936 a1i ¬ X mod T 0 π ¬ X mod T = 0 X mod T *
938 120 a1i ¬ X mod T 0 π ¬ X mod T = 0 π
939 767 a1i ¬ X mod T 0 π ¬ X mod T = 0 X mod T
940 pm4.56 ¬ X mod T 0 π ¬ X mod T = 0 ¬ X mod T 0 π X mod T = 0
941 940 biimpi ¬ X mod T 0 π ¬ X mod T = 0 ¬ X mod T 0 π X mod T = 0
942 olc X mod T = 0 X mod T 0 π X mod T = 0
943 942 adantl X mod T < π X mod T = 0 X mod T 0 π X mod T = 0
944 153 a1i X mod T < π X mod T 0 0 *
945 155 a1i X mod T < π X mod T 0 π *
946 767 a1i X mod T < π X mod T 0 X mod T
947 0red X mod T 0 0
948 767 a1i X mod T 0 X mod T
949 modge0 X T + 0 X mod T
950 3 135 949 mp2an 0 X mod T
951 950 a1i X mod T 0 0 X mod T
952 id X mod T 0 X mod T 0
953 947 948 951 952 leneltd X mod T 0 0 < X mod T
954 953 adantl X mod T < π X mod T 0 0 < X mod T
955 simpl X mod T < π X mod T 0 X mod T < π
956 944 945 946 954 955 eliood X mod T < π X mod T 0 X mod T 0 π
957 956 orcd X mod T < π X mod T 0 X mod T 0 π X mod T = 0
958 943 957 pm2.61dane X mod T < π X mod T 0 π X mod T = 0
959 941 958 nsyl ¬ X mod T 0 π ¬ X mod T = 0 ¬ X mod T < π
960 938 939 959 nltled ¬ X mod T 0 π ¬ X mod T = 0 π X mod T
961 modlt X T + X mod T < T
962 3 135 961 mp2an X mod T < T
963 962 a1i ¬ X mod T 0 π ¬ X mod T = 0 X mod T < T
964 933 935 937 960 963 elicod ¬ X mod T 0 π ¬ X mod T = 0 X mod T π T
965 eqid x X π X 1 = x X π X 1
966 965 818 204 819 constlimc 1 x X π X 1 lim X
967 966 mptru 1 x X π X 1 lim X
968 967 a1i X mod T = π 1 x X π X 1 lim X
969 id X mod T = π X mod T = π
970 ubioc1 0 * π * 0 < π π 0 π
971 153 155 72 970 mp3an π 0 π
972 969 971 eqeltrdi X mod T = π X mod T 0 π
973 972 iftrued X mod T = π if X mod T 0 π 1 1 = 1
974 363 817 feqresmpt F X π X = x X π X F x
975 974 mptru F X π X = x X π X F x
976 840 110 147 sylancl x X π X F x = if x mod T < π 1 1
977 976 adantl X mod T = π x X π X F x = if x mod T < π 1 1
978 simpr X mod T = π x X π X x X π X
979 969 eqcomd X mod T = π π = X mod T
980 979 oveq2d X mod T = π X π = X X mod T
981 980 oveq1d X mod T = π X π X = X X mod T X
982 981 adantr X mod T = π x X π X X π X = X X mod T X
983 978 982 eleqtrd X mod T = π x X π X x X X mod T X
984 983 803 syl X mod T = π x X π X x mod T < X mod T
985 simpl X mod T = π x X π X X mod T = π
986 984 985 breqtrd X mod T = π x X π X x mod T < π
987 986 iftrued X mod T = π x X π X if x mod T < π 1 1 = 1
988 977 987 eqtrd X mod T = π x X π X F x = 1
989 988 mpteq2dva X mod T = π x X π X F x = x X π X 1
990 975 989 eqtr2id X mod T = π x X π X 1 = F X π X
991 990 oveq1d X mod T = π x X π X 1 lim X = F X π X lim X
992 991 929 eqtr2di X mod T = π F −∞ X lim X = x X π X 1 lim X
993 968 973 992 3eltr4d X mod T = π if X mod T 0 π 1 1 F −∞ X lim X
994 993 adantl X mod T π T X mod T = π if X mod T 0 π 1 1 F −∞ X lim X
995 155 a1i X mod T π T ¬ X mod T = π π *
996 934 a1i X mod T π T ¬ X mod T = π T *
997 767 a1i X mod T π T ¬ X mod T = π X mod T
998 120 a1i X mod T π T ¬ X mod T = π π
999 icogelb π * T * X mod T π T π X mod T
1000 155 934 999 mp3an12 X mod T π T π X mod T
1001 1000 adantr X mod T π T ¬ X mod T = π π X mod T
1002 neqne ¬ X mod T = π X mod T π
1003 1002 adantl X mod T π T ¬ X mod T = π X mod T π
1004 998 997 1001 1003 leneltd X mod T π T ¬ X mod T = π π < X mod T
1005 962 a1i X mod T π T ¬ X mod T = π X mod T < T
1006 995 996 997 1004 1005 eliood X mod T π T ¬ X mod T = π X mod T π T
1007 eqid x X + π - X mod T X 1 = x X + π - X mod T X 1
1008 ioossre X + π - X mod T X
1009 1008 a1i X mod T π T X + π - X mod T X
1010 1009 208 sstrdi X mod T π T X + π - X mod T X
1011 neg1cn 1
1012 1011 a1i X mod T π T 1
1013 27 a1i X mod T π T X
1014 1007 1010 1012 1013 constlimc X mod T π T 1 x X + π - X mod T X 1 lim X
1015 153 a1i X mod T π T 0 *
1016 120 a1i X mod T π T π
1017 936 a1i X mod T π T X mod T *
1018 ioogtlb π * T * X mod T π T π < X mod T
1019 155 934 1018 mp3an12 X mod T π T π < X mod T
1020 1015 1016 1017 1019 gtnelioc X mod T π T ¬ X mod T 0 π
1021 1020 iffalsed X mod T π T if X mod T 0 π 1 1 = 1
1022 1008 a1i X + π - X mod T X
1023 363 1022 feqresmpt F X + π - X mod T X = x X + π - X mod T X F x
1024 1023 mptru F X + π - X mod T X = x X + π - X mod T X F x
1025 elioore x X + π - X mod T X x
1026 1025 110 147 sylancl x X + π - X mod T X F x = if x mod T < π 1 1
1027 1026 adantl X mod T π T x X + π - X mod T X F x = if x mod T < π 1 1
1028 120 a1i X mod T π T x X + π - X mod T X π
1029 135 a1i x X + π - X mod T X T +
1030 1025 1029 modcld x X + π - X mod T X x mod T
1031 1030 adantl X mod T π T x X + π - X mod T X x mod T
1032 3 120 readdcli X + π
1033 1032 recni X + π
1034 1033 a1i x X + π - X mod T X X + π
1035 27 a1i x X + π - X mod T X X
1036 767 recni X mod T
1037 1036 a1i x X + π - X mod T X X mod T
1038 1034 1035 1037 nnncan2d x X + π - X mod T X X + π - X mod T - X X mod T = X + π - X
1039 1038 861 eqtr2di x X + π - X mod T X π = X + π - X mod T - X X mod T
1040 1032 767 resubcli X + π - X mod T
1041 1040 a1i x X + π - X mod T X X + π - X mod T
1042 768 a1i x X + π - X mod T X X X mod T
1043 1040 rexri X + π - X mod T *
1044 1043 a1i x X + π - X mod T X X + π - X mod T *
1045 3 a1i x X + π - X mod T X X
1046 1045 rexrd x X + π - X mod T X X *
1047 id x X + π - X mod T X x X + π - X mod T X
1048 ioogtlb X + π - X mod T * X * x X + π - X mod T X X + π - X mod T < x
1049 1044 1046 1047 1048 syl3anc x X + π - X mod T X X + π - X mod T < x
1050 1041 1025 1042 1049 ltsub1dd x X + π - X mod T X X + π - X mod T - X X mod T < x X X mod T
1051 1039 1050 eqbrtrd x X + π - X mod T X π < x X X mod T
1052 1025 recnd x X + π - X mod T X x
1053 sub31 x X X mod T x X X mod T = X mod T X x
1054 1052 1035 1037 1053 syl3anc x X + π - X mod T X x X X mod T = X mod T X x
1055 1051 1054 breqtrd x X + π - X mod T X π < X mod T X x
1056 1055 adantl π < X mod T x X + π - X mod T X π < X mod T X x
1057 1045 1025 resubcld x X + π - X mod T X X x
1058 0red x X + π - X mod T X 0
1059 iooltub X + π - X mod T * X * x X + π - X mod T X x < X
1060 1044 1046 1047 1059 syl3anc x X + π - X mod T X x < X
1061 1025 1045 posdifd x X + π - X mod T X x < X 0 < X x
1062 1060 1061 mpbid x X + π - X mod T X 0 < X x
1063 1058 1057 1062 ltled x X + π - X mod T X 0 X x
1064 1045 1041 resubcld x X + π - X mod T X X X + π - X mod T
1065 122 a1i x X + π - X mod T X T
1066 1041 1025 1045 1049 ltsub2dd x X + π - X mod T X X x < X X + π - X mod T
1067 sub31 X X + π X mod T X X + π - X mod T = X mod T X + π - X
1068 27 1033 1036 1067 mp3an X X + π - X mod T = X mod T X + π - X
1069 861 oveq2i X mod T X + π - X = X mod T π
1070 1068 1069 eqtri X X + π - X mod T = X mod T π
1071 ltsubrp X mod T π + X mod T π < X mod T
1072 767 184 1071 mp2an X mod T π < X mod T
1073 767 120 resubcli X mod T π
1074 1073 767 122 lttri X mod T π < X mod T X mod T < T X mod T π < T
1075 1072 962 1074 mp2an X mod T π < T
1076 1070 1075 eqbrtri X X + π - X mod T < T
1077 1076 a1i x X + π - X mod T X X X + π - X mod T < T
1078 1057 1064 1065 1066 1077 lttrd x X + π - X mod T X X x < T
1079 modid X x T + 0 X x X x < T X x mod T = X x
1080 1057 1029 1063 1078 1079 syl22anc x X + π - X mod T X X x mod T = X x
1081 1080 oveq2d x X + π - X mod T X X mod T X x mod T = X mod T X x
1082 1081 oveq1d x X + π - X mod T X X mod T X x mod T mod T = X mod T X x mod T
1083 767 a1i x X + π - X mod T X X mod T
1084 1083 1057 resubcld x X + π - X mod T X X mod T X x
1085 120 a1i x X + π - X mod T X π
1086 1054 1084 eqeltrd x X + π - X mod T X x X X mod T
1087 72 a1i x X + π - X mod T X 0 < π
1088 1058 1085 1086 1087 1051 lttrd x X + π - X mod T X 0 < x X X mod T
1089 1088 1054 breqtrd x X + π - X mod T X 0 < X mod T X x
1090 1058 1084 1089 ltled x X + π - X mod T X 0 X mod T X x
1091 1045 1042 resubcld x X + π - X mod T X X X X mod T
1092 1025 1045 1042 1060 ltsub1dd x X + π - X mod T X x X X mod T < X X X mod T
1093 nncan X X mod T X X X mod T = X mod T
1094 27 1036 1093 mp2an X X X mod T = X mod T
1095 1094 962 eqbrtri X X X mod T < T
1096 1095 a1i x X + π - X mod T X X X X mod T < T
1097 1086 1091 1065 1092 1096 lttrd x X + π - X mod T X x X X mod T < T
1098 1054 1097 eqbrtrrd x X + π - X mod T X X mod T X x < T
1099 modid X mod T X x T + 0 X mod T X x X mod T X x < T X mod T X x mod T = X mod T X x
1100 1084 1029 1090 1098 1099 syl22anc x X + π - X mod T X X mod T X x mod T = X mod T X x
1101 1082 1100 eqtr2d x X + π - X mod T X X mod T X x = X mod T X x mod T mod T
1102 modsubmodmod X X x T + X mod T X x mod T mod T = X X x mod T
1103 1045 1057 1029 1102 syl3anc x X + π - X mod T X X mod T X x mod T mod T = X X x mod T
1104 1035 1052 nncand x X + π - X mod T X X X x = x
1105 1104 oveq1d x X + π - X mod T X X X x mod T = x mod T
1106 1101 1103 1105 3eqtrd x X + π - X mod T X X mod T X x = x mod T
1107 1106 adantl π < X mod T x X + π - X mod T X X mod T X x = x mod T
1108 1056 1107 breqtrd π < X mod T x X + π - X mod T X π < x mod T
1109 1019 1108 sylan X mod T π T x X + π - X mod T X π < x mod T
1110 1028 1031 1109 ltled X mod T π T x X + π - X mod T X π x mod T
1111 1028 1031 1110 lensymd X mod T π T x X + π - X mod T X ¬ x mod T < π
1112 1111 iffalsed X mod T π T x X + π - X mod T X if x mod T < π 1 1 = 1
1113 1027 1112 eqtrd X mod T π T x X + π - X mod T X F x = 1
1114 1113 mpteq2dva X mod T π T x X + π - X mod T X F x = x X + π - X mod T X 1
1115 1024 1114 eqtr2id X mod T π T x X + π - X mod T X 1 = F X + π - X mod T X
1116 1115 oveq1d X mod T π T x X + π - X mod T X 1 lim X = F X + π - X mod T X lim X
1117 210 a1i X mod T π T F :
1118 1043 a1i X mod T π T X + π - X mod T *
1119 3 a1i X mod T π T X
1120 elioore X mod T π T X mod T
1121 ltaddsublt X π X mod T π < X mod T X + π - X mod T < X
1122 1119 1016 1120 1121 syl3anc X mod T π T π < X mod T X + π - X mod T < X
1123 1019 1122 mpbid X mod T π T X + π - X mod T < X
1124 365 a1i X mod T π T −∞ *
1125 mnflt X + π - X mod T −∞ < X + π - X mod T
1126 xrltle −∞ * X + π - X mod T * −∞ < X + π - X mod T −∞ X + π - X mod T
1127 365 1043 1126 mp2an −∞ < X + π - X mod T −∞ X + π - X mod T
1128 1040 1125 1127 mp2b −∞ X + π - X mod T
1129 1128 a1i X mod T π T −∞ X + π - X mod T
1130 1117 1118 1119 1123 1009 1124 1129 limcresiooub X mod T π T F X + π - X mod T X lim X = F −∞ X lim X
1131 1116 1130 eqtr2d X mod T π T F −∞ X lim X = x X + π - X mod T X 1 lim X
1132 1014 1021 1131 3eltr4d X mod T π T if X mod T 0 π 1 1 F −∞ X lim X
1133 1006 1132 syl X mod T π T ¬ X mod T = π if X mod T 0 π 1 1 F −∞ X lim X
1134 994 1133 pm2.61dan X mod T π T if X mod T 0 π 1 1 F −∞ X lim X
1135 964 1134 syl ¬ X mod T 0 π ¬ X mod T = 0 if X mod T 0 π 1 1 F −∞ X lim X
1136 932 1135 pm2.61dan ¬ X mod T 0 π if X mod T 0 π 1 1 F −∞ X lim X
1137 814 1136 pm2.61i if X mod T 0 π 1 1 F −∞ X lim X
1138 eqid x X X + π - X mod T 1 = x X X + π - X mod T 1
1139 ioossre X X + π - X mod T
1140 1139 a1i X X + π - X mod T
1141 1140 208 sstrdi X X + π - X mod T
1142 1138 1141 204 819 constlimc 1 x X X + π - X mod T 1 lim X
1143 1142 mptru 1 x X X + π - X mod T 1 lim X
1144 1143 a1i X mod T 0 π 1 x X X + π - X mod T 1 lim X
1145 2 a1i X mod T 0 π F = x if x mod T < π 1 1
1146 oveq1 x = X x mod T = X mod T
1147 1146 breq1d x = X x mod T < π X mod T < π
1148 1147 ifbid x = X if x mod T < π 1 1 = if X mod T < π 1 1
1149 1148 adantl X mod T 0 π x = X if x mod T < π 1 1 = if X mod T < π 1 1
1150 3 a1i X mod T 0 π X
1151 108 109 ifcli if X mod T < π 1 1
1152 1151 a1i X mod T 0 π if X mod T < π 1 1
1153 1145 1149 1150 1152 fvmptd X mod T 0 π F X = if X mod T < π 1 1
1154 icoltub 0 * π * X mod T 0 π X mod T < π
1155 153 155 1154 mp3an12 X mod T 0 π X mod T < π
1156 1155 iftrued X mod T 0 π if X mod T < π 1 1 = 1
1157 1153 1156 eqtrd X mod T 0 π F X = 1
1158 363 1140 feqresmpt F X X + π - X mod T = x X X + π - X mod T F x
1159 1158 mptru F X X + π - X mod T = x X X + π - X mod T F x
1160 elioore x X X + π - X mod T x
1161 1160 110 147 sylancl x X X + π - X mod T F x = if x mod T < π 1 1
1162 1161 adantl X mod T 0 π x X X + π - X mod T F x = if x mod T < π 1 1
1163 3 a1i x X X + π - X mod T X
1164 1160 1163 resubcld x X X + π - X mod T x X
1165 135 a1i x X X + π - X mod T T +
1166 0red x X X + π - X mod T 0
1167 1163 rexrd x X X + π - X mod T X *
1168 120 767 resubcli π X mod T
1169 3 1168 readdcli X + π - X mod T
1170 1169 rexri X + π - X mod T *
1171 1170 a1i x X X + π - X mod T X + π - X mod T *
1172 id x X X + π - X mod T x X X + π - X mod T
1173 ioogtlb X * X + π - X mod T * x X X + π - X mod T X < x
1174 1167 1171 1172 1173 syl3anc x X X + π - X mod T X < x
1175 1163 1160 posdifd x X X + π - X mod T X < x 0 < x X
1176 1174 1175 mpbid x X X + π - X mod T 0 < x X
1177 1166 1164 1176 ltled x X X + π - X mod T 0 x X
1178 120 a1i x X X + π - X mod T π
1179 122 a1i x X X + π - X mod T T
1180 1169 a1i x X X + π - X mod T X + π - X mod T
1181 1180 1163 resubcld x X X + π - X mod T X + π X mod T - X
1182 iooltub X * X + π - X mod T * x X X + π - X mod T x < X + π - X mod T
1183 1167 1171 1172 1182 syl3anc x X X + π - X mod T x < X + π - X mod T
1184 1160 1180 1163 1183 ltsub1dd x X X + π - X mod T x X < X + π X mod T - X
1185 1168 recni π X mod T
1186 pncan2 X π X mod T X + π X mod T - X = π X mod T
1187 27 1185 1186 mp2an X + π X mod T - X = π X mod T
1188 subge02 π X mod T 0 X mod T π X mod T π
1189 120 767 1188 mp2an 0 X mod T π X mod T π
1190 950 1189 mpbi π X mod T π
1191 1187 1190 eqbrtri X + π X mod T - X π
1192 1191 a1i x X X + π - X mod T X + π X mod T - X π
1193 1164 1181 1178 1184 1192 ltletrd x X X + π - X mod T x X < π
1194 187 a1i x X X + π - X mod T π < T
1195 1164 1178 1179 1193 1194 lttrd x X X + π - X mod T x X < T
1196 modid x X T + 0 x X x X < T x X mod T = x X
1197 1164 1165 1177 1195 1196 syl22anc x X X + π - X mod T x X mod T = x X
1198 1197 oveq2d x X X + π - X mod T X mod T + x X mod T = X mod T + x - X
1199 1198 oveq1d x X X + π - X mod T X mod T + x X mod T mod T = X mod T + x - X mod T
1200 767 a1i x X X + π - X mod T X mod T
1201 1200 1164 readdcld x X X + π - X mod T X mod T + x - X
1202 1163 1163 resubcld x X X + π - X mod T X X
1203 1200 1202 readdcld x X X + π - X mod T X mod T + X - X
1204 27 subidi X X = 0
1205 1204 oveq2i X mod T + X - X = X mod T + 0
1206 1036 addid1i X mod T + 0 = X mod T
1207 1205 1206 eqtr2i X mod T = X mod T + X - X
1208 950 1207 breqtri 0 X mod T + X - X
1209 1208 a1i x X X + π - X mod T 0 X mod T + X - X
1210 1163 1160 1163 1174 ltsub1dd x X X + π - X mod T X X < x X
1211 1202 1164 1200 1210 ltadd2dd x X X + π - X mod T X mod T + X - X < X mod T + x - X
1212 1166 1203 1201 1209 1211 lelttrd x X X + π - X mod T 0 < X mod T + x - X
1213 1166 1201 1212 ltled x X X + π - X mod T 0 X mod T + x - X
1214 1164 1181 1200 1184 ltadd2dd x X X + π - X mod T X mod T + x - X < X mod T + X + π - X mod T - X
1215 1187 oveq2i X mod T + X + π - X mod T - X = X mod T + π - X mod T
1216 1036 56 pncan3i X mod T + π - X mod T = π
1217 1215 1216 eqtri X mod T + X + π - X mod T - X = π
1218 1214 1217 breqtrdi x X X + π - X mod T X mod T + x - X < π
1219 1201 1178 1179 1218 1194 lttrd x X X + π - X mod T X mod T + x - X < T
1220 modid X mod T + x - X T + 0 X mod T + x - X X mod T + x - X < T X mod T + x - X mod T = X mod T + x - X
1221 1201 1165 1213 1219 1220 syl22anc x X X + π - X mod T X mod T + x - X mod T = X mod T + x - X
1222 1199 1221 eqtr2d x X X + π - X mod T X mod T + x - X = X mod T + x X mod T mod T
1223 modaddabs X x X T + X mod T + x X mod T mod T = X + x - X mod T
1224 1163 1164 1165 1223 syl3anc x X X + π - X mod T X mod T + x X mod T mod T = X + x - X mod T
1225 27 a1i x X X + π - X mod T X
1226 1160 recnd x X X + π - X mod T x
1227 1225 1226 pncan3d x X X + π - X mod T X + x - X = x
1228 1227 oveq1d x X X + π - X mod T X + x - X mod T = x mod T
1229 1222 1224 1228 3eqtrrd x X X + π - X mod T x mod T = X mod T + x - X
1230 1229 adantl X mod T < π x X X + π - X mod T x mod T = X mod T + x - X
1231 1218 adantl X mod T < π x X X + π - X mod T X mod T + x - X < π
1232 1230 1231 eqbrtrd X mod T < π x X X + π - X mod T x mod T < π
1233 1155 1232 sylan X mod T 0 π x X X + π - X mod T x mod T < π
1234 1233 iftrued X mod T 0 π x X X + π - X mod T if x mod T < π 1 1 = 1
1235 1162 1234 eqtrd X mod T 0 π x X X + π - X mod T F x = 1
1236 1235 mpteq2dva X mod T 0 π x X X + π - X mod T F x = x X X + π - X mod T 1
1237 1159 1236 eqtr2id X mod T 0 π x X X + π - X mod T 1 = F X X + π - X mod T
1238 1237 oveq1d X mod T 0 π x X X + π - X mod T 1 lim X = F X X + π - X mod T lim X
1239 210 a1i X mod T 0 π F :
1240 1170 a1i X mod T 0 π X + π - X mod T *
1241 1168 a1i X mod T 0 π π X mod T
1242 767 a1i X mod T 0 π X mod T
1243 120 a1i X mod T 0 π π
1244 1242 1243 posdifd X mod T 0 π X mod T < π 0 < π X mod T
1245 1155 1244 mpbid X mod T 0 π 0 < π X mod T
1246 1241 1245 elrpd X mod T 0 π π X mod T +
1247 1150 1246 ltaddrpd X mod T 0 π X < X + π - X mod T
1248 1139 a1i X mod T 0 π X X + π - X mod T
1249 376 a1i X mod T 0 π +∞ *
1250 ltpnf X + π - X mod T X + π - X mod T < +∞
1251 xrltle X + π - X mod T * +∞ * X + π - X mod T < +∞ X + π - X mod T +∞
1252 1170 376 1251 mp2an X + π - X mod T < +∞ X + π - X mod T +∞
1253 1169 1250 1252 mp2b X + π - X mod T +∞
1254 1253 a1i X mod T 0 π X + π - X mod T +∞
1255 1239 1150 1240 1247 1248 1249 1254 limcresioolb X mod T 0 π F X X + π - X mod T lim X = F X +∞ lim X
1256 1238 1255 eqtr2d X mod T 0 π F X +∞ lim X = x X X + π - X mod T 1 lim X
1257 1144 1157 1256 3eltr4d X mod T 0 π F X F X +∞ lim X
1258 155 a1i ¬ X mod T 0 π π *
1259 934 a1i ¬ X mod T 0 π T *
1260 936 a1i ¬ X mod T 0 π X mod T *
1261 153 a1i ¬ X mod T 0 π ¬ π X mod T 0 *
1262 155 a1i ¬ X mod T 0 π ¬ π X mod T π *
1263 936 a1i ¬ X mod T 0 π ¬ π X mod T X mod T *
1264 950 a1i ¬ X mod T 0 π ¬ π X mod T 0 X mod T
1265 767 a1i ¬ π X mod T X mod T
1266 120 a1i ¬ π X mod T π
1267 1265 1266 ltnled ¬ π X mod T X mod T < π ¬ π X mod T
1268 1267 ibir ¬ π X mod T X mod T < π
1269 1268 adantl ¬ X mod T 0 π ¬ π X mod T X mod T < π
1270 1261 1262 1263 1264 1269 elicod ¬ X mod T 0 π ¬ π X mod T X mod T 0 π
1271 simpl ¬ X mod T 0 π ¬ π X mod T ¬ X mod T 0 π
1272 1270 1271 condan ¬ X mod T 0 π π X mod T
1273 962 a1i ¬ X mod T 0 π X mod T < T
1274 1258 1259 1260 1272 1273 elicod ¬ X mod T 0 π X mod T π T
1275 eqid x X X + T - X mod T 1 = x X X + T - X mod T 1
1276 ioossre X X + T - X mod T
1277 1276 a1i X X + T - X mod T
1278 1277 208 sstrdi X X + T - X mod T
1279 1275 1278 306 819 constlimc 1 x X X + T - X mod T 1 lim X
1280 1279 mptru 1 x X X + T - X mod T 1 lim X
1281 1280 a1i X mod T π T 1 x X X + T - X mod T 1 lim X
1282 1ex 1 V
1283 109 elexi 1 V
1284 1282 1283 ifex if X mod T < π 1 1 V
1285 1148 2 1284 fvmpt X F X = if X mod T < π 1 1
1286 3 1285 ax-mp F X = if X mod T < π 1 1
1287 1286 a1i X mod T π T F X = if X mod T < π 1 1
1288 120 a1i X mod T π T π
1289 767 a1i X mod T π T X mod T
1290 1288 1289 1000 lensymd X mod T π T ¬ X mod T < π
1291 1290 iffalsed X mod T π T if X mod T < π 1 1 = 1
1292 1287 1291 eqtrd X mod T π T F X = 1
1293 363 1277 feqresmpt F X X + T - X mod T = x X X + T - X mod T F x
1294 1293 mptru F X X + T - X mod T = x X X + T - X mod T F x
1295 elioore x X X + T - X mod T x
1296 1295 110 147 sylancl x X X + T - X mod T F x = if x mod T < π 1 1
1297 1296 adantl X mod T π T x X X + T - X mod T F x = if x mod T < π 1 1
1298 120 a1i X mod T π T x X X + T - X mod T π
1299 3 a1i x X X + T - X mod T X
1300 1295 1299 resubcld x X X + T - X mod T x X
1301 135 a1i x X X + T - X mod T T +
1302 0red x X X + T - X mod T 0
1303 1299 rexrd x X X + T - X mod T X *
1304 122 767 resubcli T X mod T
1305 3 1304 readdcli X + T - X mod T
1306 1305 rexri X + T - X mod T *
1307 1306 a1i x X X + T - X mod T X + T - X mod T *
1308 id x X X + T - X mod T x X X + T - X mod T
1309 ioogtlb X * X + T - X mod T * x X X + T - X mod T X < x
1310 1303 1307 1308 1309 syl3anc x X X + T - X mod T X < x
1311 1299 1295 posdifd x X X + T - X mod T X < x 0 < x X
1312 1310 1311 mpbid x X X + T - X mod T 0 < x X
1313 1302 1300 1312 ltled x X X + T - X mod T 0 x X
1314 1305 a1i x X X + T - X mod T X + T - X mod T
1315 1314 1299 resubcld x X X + T - X mod T X + T X mod T - X
1316 122 a1i x X X + T - X mod T T
1317 iooltub X * X + T - X mod T * x X X + T - X mod T x < X + T - X mod T
1318 1303 1307 1308 1317 syl3anc x X X + T - X mod T x < X + T - X mod T
1319 1295 1314 1299 1318 ltsub1dd x X X + T - X mod T x X < X + T X mod T - X
1320 1304 recni T X mod T
1321 pncan2 X T X mod T X + T X mod T - X = T X mod T
1322 27 1320 1321 mp2an X + T X mod T - X = T X mod T
1323 subge02 T X mod T 0 X mod T T X mod T T
1324 122 767 1323 mp2an 0 X mod T T X mod T T
1325 950 1324 mpbi T X mod T T
1326 1322 1325 eqbrtri X + T X mod T - X T
1327 1326 a1i x X X + T - X mod T X + T X mod T - X T
1328 1300 1315 1316 1319 1327 ltletrd x X X + T - X mod T x X < T
1329 1300 1301 1313 1328 1196 syl22anc x X X + T - X mod T x X mod T = x X
1330 1329 oveq2d x X X + T - X mod T X mod T + x X mod T = X mod T + x - X
1331 1330 oveq1d x X X + T - X mod T X mod T + x X mod T mod T = X mod T + x - X mod T
1332 readdcl X mod T x X X mod T + x - X
1333 767 1300 1332 sylancr x X X + T - X mod T X mod T + x - X
1334 767 a1i x X X + T - X mod T X mod T
1335 950 a1i x X X + T - X mod T 0 X mod T
1336 1334 1300 1335 1312 addgegt0d x X X + T - X mod T 0 < X mod T + x - X
1337 1302 1333 1336 ltled x X X + T - X mod T 0 X mod T + x - X
1338 1300 1315 1334 1319 ltadd2dd x X X + T - X mod T X mod T + x - X < X mod T + X + T - X mod T - X
1339 1322 oveq2i X mod T + X + T - X mod T - X = X mod T + T - X mod T
1340 1036 123 pncan3i X mod T + T - X mod T = T
1341 1339 1340 eqtri X mod T + X + T - X mod T - X = T
1342 1338 1341 breqtrdi x X X + T - X mod T X mod T + x - X < T
1343 1333 1301 1337 1342 1220 syl22anc x X X + T - X mod T X mod T + x - X mod T = X mod T + x - X
1344 1331 1343 eqtr2d x X X + T - X mod T X mod T + x - X = X mod T + x X mod T mod T
1345 1299 1300 1301 1223 syl3anc x X X + T - X mod T X mod T + x X mod T mod T = X + x - X mod T
1346 27 a1i x X X + T - X mod T X
1347 1295 recnd x X X + T - X mod T x
1348 1346 1347 pncan3d x X X + T - X mod T X + x - X = x
1349 1348 oveq1d x X X + T - X mod T X + x - X mod T = x mod T
1350 1344 1345 1349 3eqtrd x X X + T - X mod T X mod T + x - X = x mod T
1351 1350 adantl X mod T π T x X X + T - X mod T X mod T + x - X = x mod T
1352 1333 adantl X mod T π T x X X + T - X mod T X mod T + x - X
1353 1351 1352 eqeltrrd X mod T π T x X X + T - X mod T x mod T
1354 767 a1i X mod T π T x X X + T - X mod T X mod T
1355 1000 adantr X mod T π T x X X + T - X mod T π X mod T
1356 1300 1312 elrpd x X X + T - X mod T x X +
1357 1334 1356 ltaddrpd x X X + T - X mod T X mod T < X mod T + x - X
1358 1357 adantl X mod T π T x X X + T - X mod T X mod T < X mod T + x - X
1359 1298 1354 1352 1355 1358 lelttrd X mod T π T x X X + T - X mod T π < X mod T + x - X
1360 1298 1352 1359 ltled X mod T π T x X X + T - X mod T π X mod T + x - X
1361 1360 1351 breqtrd X mod T π T x X X + T - X mod T π x mod T
1362 1298 1353 1361 lensymd X mod T π T x X X + T - X mod T ¬ x mod T < π
1363 1362 iffalsed X mod T π T x X X + T - X mod T if x mod T < π 1 1 = 1
1364 1297 1363 eqtrd X mod T π T x X X + T - X mod T F x = 1
1365 1364 mpteq2dva X mod T π T x X X + T - X mod T F x = x X X + T - X mod T 1
1366 1294 1365 eqtr2id X mod T π T x X X + T - X mod T 1 = F X X + T - X mod T
1367 1366 oveq1d X mod T π T x X X + T - X mod T 1 lim X = F X X + T - X mod T lim X
1368 210 a1i X mod T π T F :
1369 3 a1i X mod T π T X
1370 1306 a1i X mod T π T X + T - X mod T *
1371 1304 a1i X mod T π T T X mod T
1372 962 a1i X mod T π T X mod T < T
1373 122 a1i X mod T π T T
1374 1289 1373 posdifd X mod T π T X mod T < T 0 < T X mod T
1375 1372 1374 mpbid X mod T π T 0 < T X mod T
1376 1371 1375 elrpd X mod T π T T X mod T +
1377 1369 1376 ltaddrpd X mod T π T X < X + T - X mod T
1378 1276 a1i X mod T π T X X + T - X mod T
1379 376 a1i X mod T π T +∞ *
1380 ltpnf X + T - X mod T X + T - X mod T < +∞
1381 xrltle X + T - X mod T * +∞ * X + T - X mod T < +∞ X + T - X mod T +∞
1382 1306 376 1381 mp2an X + T - X mod T < +∞ X + T - X mod T +∞
1383 1305 1380 1382 mp2b X + T - X mod T +∞
1384 1383 a1i X mod T π T X + T - X mod T +∞
1385 1368 1369 1370 1377 1378 1379 1384 limcresioolb X mod T π T F X X + T - X mod T lim X = F X +∞ lim X
1386 1367 1385 eqtr2d X mod T π T F X +∞ lim X = x X X + T - X mod T 1 lim X
1387 1281 1292 1386 3eltr4d X mod T π T F X F X +∞ lim X
1388 1274 1387 syl ¬ X mod T 0 π F X F X +∞ lim X
1389 1257 1388 pm2.61i F X F X +∞ lim X
1390 id n 0 n 0
1391 1 2 1390 sqwvfoura n 0 π π F x cos n x dx π = 0
1392 1391 eqcomd n 0 0 = π π F x cos n x dx π
1393 1392 mpteq2ia n 0 0 = n 0 π π F x cos n x dx π
1394 id n n
1395 1 2 1394 sqwvfourb n π π F x sin n x dx π = if 2 n 0 4 n π
1396 1395 eqcomd n if 2 n 0 4 n π = π π F x sin n x dx π
1397 1396 mpteq2ia n if 2 n 0 4 n π = n π π F x sin n x dx π
1398 nnnn0 n n 0
1399 0red n 0
1400 eqid n 0 0 = n 0 0
1401 1400 fvmpt2 n 0 0 n 0 0 n = 0
1402 1398 1399 1401 syl2anc n n 0 0 n = 0
1403 1402 oveq1d n n 0 0 n cos n X = 0 cos n X
1404 78 coscld n cos n X
1405 1404 mul02d n 0 cos n X = 0
1406 1403 1405 eqtrd n n 0 0 n cos n X = 0
1407 ovex 4 n π V
1408 93 1407 ifex if 2 n 0 4 n π V
1409 eqid n if 2 n 0 4 n π = n if 2 n 0 4 n π
1410 1409 fvmpt2 n if 2 n 0 4 n π V n if 2 n 0 4 n π n = if 2 n 0 4 n π
1411 1408 1410 mpan2 n n if 2 n 0 4 n π n = if 2 n 0 4 n π
1412 1411 oveq1d n n if 2 n 0 4 n π n sin n X = if 2 n 0 4 n π sin n X
1413 1406 1412 oveq12d n n 0 0 n cos n X + n if 2 n 0 4 n π n sin n X = 0 + if 2 n 0 4 n π sin n X
1414 64 76 ifcld n if 2 n 0 4 n π
1415 1414 79 mulcld n if 2 n 0 4 n π sin n X
1416 1415 addid2d n 0 + if 2 n 0 4 n π sin n X = if 2 n 0 4 n π sin n X
1417 iftrue 2 n if 2 n 0 4 n π = 0
1418 1417 oveq1d 2 n if 2 n 0 4 n π sin n X = 0 sin n X
1419 79 mul02d n 0 sin n X = 0
1420 1418 1419 sylan9eqr n 2 n if 2 n 0 4 n π sin n X = 0
1421 iftrue 2 n if 2 n 0 4 n π sin n X = 0
1422 1421 eqcomd 2 n 0 = if 2 n 0 4 n π sin n X
1423 1422 adantl n 2 n 0 = if 2 n 0 4 n π sin n X
1424 1420 1423 eqtrd n 2 n if 2 n 0 4 n π sin n X = if 2 n 0 4 n π sin n X
1425 iffalse ¬ 2 n if 2 n 0 4 n π = 4 n π
1426 1425 oveq1d ¬ 2 n if 2 n 0 4 n π sin n X = 4 n π sin n X
1427 1426 adantl n ¬ 2 n if 2 n 0 4 n π sin n X = 4 n π sin n X
1428 iffalse ¬ 2 n if 2 n 0 4 n π sin n X = 4 n π sin n X
1429 1428 eqcomd ¬ 2 n 4 n π sin n X = if 2 n 0 4 n π sin n X
1430 1429 adantl n ¬ 2 n 4 n π sin n X = if 2 n 0 4 n π sin n X
1431 1427 1430 eqtrd n ¬ 2 n if 2 n 0 4 n π sin n X = if 2 n 0 4 n π sin n X
1432 1424 1431 pm2.61dan n if 2 n 0 4 n π sin n X = if 2 n 0 4 n π sin n X
1433 1413 1416 1432 3eqtrrd n if 2 n 0 4 n π sin n X = n 0 0 n cos n X + n if 2 n 0 4 n π n sin n X
1434 1433 mpteq2ia n if 2 n 0 4 n π sin n X = n n 0 0 n cos n X + n if 2 n 0 4 n π n sin n X
1435 112 1 149 150 331 605 676 755 3 1137 1389 1393 1397 1434 fourierclim seq 1 + n if 2 n 0 4 n π sin n X if X mod T 0 π 1 1 + F X 2 n 0 0 0 2
1436 0nn0 0 0
1437 eqidd n = 0 0 = 0
1438 1437 1400 93 fvmpt 0 0 n 0 0 0 = 0
1439 1436 1438 ax-mp n 0 0 0 = 0
1440 1439 oveq1i n 0 0 0 2 = 0 2
1441 32 recni 2
1442 71 131 gtneii 2 0
1443 1441 1442 div0i 0 2 = 0
1444 1440 1443 eqtri n 0 0 0 2 = 0
1445 1444 oveq2i if X mod T 0 π 1 1 + F X 2 n 0 0 0 2 = if X mod T 0 π 1 1 + F X 2 0
1446 204 mptru 1
1447 1446 1011 ifcli if X mod T 0 π 1 1
1448 1151 recni if X mod T < π 1 1
1449 1286 1448 eqeltri F X
1450 1447 1449 addcli if X mod T 0 π 1 1 + F X
1451 1450 1441 1442 divcli if X mod T 0 π 1 1 + F X 2
1452 1451 subid1i if X mod T 0 π 1 1 + F X 2 0 = if X mod T 0 π 1 1 + F X 2
1453 1445 1452 eqtri if X mod T 0 π 1 1 + F X 2 n 0 0 0 2 = if X mod T 0 π 1 1 + F X 2
1454 1435 1453 breqtri seq 1 + n if 2 n 0 4 n π sin n X if X mod T 0 π 1 1 + F X 2
1455 1454 a1i seq 1 + n if 2 n 0 4 n π sin n X if X mod T 0 π 1 1 + F X 2
1456 83 107 1455 sumnnodd seq 1 + k n if 2 n 0 4 n π sin n X 2 k 1 if X mod T 0 π 1 1 + F X 2 k n if 2 n 0 4 n π sin n X k = k n if 2 n 0 4 n π sin n X 2 k 1
1457 1456 mptru seq 1 + k n if 2 n 0 4 n π sin n X 2 k 1 if X mod T 0 π 1 1 + F X 2 k n if 2 n 0 4 n π sin n X k = k n if 2 n 0 4 n π sin n X 2 k 1
1458 1457 simpli seq 1 + k n if 2 n 0 4 n π sin n X 2 k 1 if X mod T 0 π 1 1 + F X 2
1459 breq2 n = 2 k 1 2 n 2 2 k 1
1460 oveq1 n = 2 k 1 n π = 2 k 1 π
1461 1460 oveq2d n = 2 k 1 4 n π = 4 2 k 1 π
1462 oveq1 n = 2 k 1 n X = 2 k 1 X
1463 1462 fveq2d n = 2 k 1 sin n X = sin 2 k 1 X
1464 1461 1463 oveq12d n = 2 k 1 4 n π sin n X = 4 2 k 1 π sin 2 k 1 X
1465 1459 1464 ifbieq2d n = 2 k 1 if 2 n 0 4 n π sin n X = if 2 2 k 1 0 4 2 k 1 π sin 2 k 1 X
1466 1465 adantl k n = 2 k 1 if 2 n 0 4 n π sin n X = if 2 2 k 1 0 4 2 k 1 π sin 2 k 1 X
1467 elnnz 2 k 1 2 k 1 0 < 2 k 1
1468 25 52 1467 sylanbrc k 2 k 1
1469 ovex 4 2 k 1 π sin 2 k 1 X V
1470 93 1469 ifex if 2 2 k 1 0 4 2 k 1 π sin 2 k 1 X V
1471 1470 a1i k if 2 2 k 1 0 4 2 k 1 π sin 2 k 1 X V
1472 84 1466 1468 1471 fvmptd k n if 2 n 0 4 n π sin n X 2 k 1 = if 2 2 k 1 0 4 2 k 1 π sin 2 k 1 X
1473 dvdsmul1 2 k 2 2 k
1474 20 22 1473 sylancr k 2 2 k
1475 23 zcnd k 2 k
1476 1cnd k 1
1477 1475 1476 npcand k 2 k - 1 + 1 = 2 k
1478 1477 eqcomd k 2 k = 2 k - 1 + 1
1479 1474 1478 breqtrd k 2 2 k - 1 + 1
1480 oddp1even 2 k 1 ¬ 2 2 k 1 2 2 k - 1 + 1
1481 25 1480 syl k ¬ 2 2 k 1 2 2 k - 1 + 1
1482 1479 1481 mpbird k ¬ 2 2 k 1
1483 1482 iffalsed k if 2 2 k 1 0 4 2 k 1 π sin 2 k 1 X = 4 2 k 1 π sin 2 k 1 X
1484 56 a1i k π
1485 26 1484 mulcomd k 2 k 1 π = π 2 k 1
1486 1485 oveq2d k 4 2 k 1 π = 4 π 2 k 1
1487 58 a1i k 4
1488 73 a1i k π 0
1489 1487 1484 26 1488 53 divdiv1d k 4 π 2 k 1 = 4 π 2 k 1
1490 1486 1489 eqtr4d k 4 2 k 1 π = 4 π 2 k 1
1491 1490 oveq1d k 4 2 k 1 π sin 2 k 1 X = 4 π 2 k 1 sin 2 k 1 X
1492 1487 1484 1488 divcld k 4 π
1493 1492 26 30 53 div32d k 4 π 2 k 1 sin 2 k 1 X = 4 π sin 2 k 1 X 2 k 1
1494 1491 1493 eqtrd k 4 2 k 1 π sin 2 k 1 X = 4 π sin 2 k 1 X 2 k 1
1495 1472 1483 1494 3eqtrd k n if 2 n 0 4 n π sin n X 2 k 1 = 4 π sin 2 k 1 X 2 k 1
1496 1495 mpteq2ia k n if 2 n 0 4 n π sin n X 2 k 1 = k 4 π sin 2 k 1 X 2 k 1
1497 oveq2 k = n 2 k = 2 n
1498 1497 oveq1d k = n 2 k 1 = 2 n 1
1499 1498 oveq1d k = n 2 k 1 X = 2 n 1 X
1500 1499 fveq2d k = n sin 2 k 1 X = sin 2 n 1 X
1501 1500 1498 oveq12d k = n sin 2 k 1 X 2 k 1 = sin 2 n 1 X 2 n 1
1502 1501 oveq2d k = n 4 π sin 2 k 1 X 2 k 1 = 4 π sin 2 n 1 X 2 n 1
1503 1502 cbvmptv k 4 π sin 2 k 1 X 2 k 1 = n 4 π sin 2 n 1 X 2 n 1
1504 1496 1503 eqtri k n if 2 n 0 4 n π sin n X 2 k 1 = n 4 π sin 2 n 1 X 2 n 1
1505 seqeq3 k n if 2 n 0 4 n π sin n X 2 k 1 = n 4 π sin 2 n 1 X 2 n 1 seq 1 + k n if 2 n 0 4 n π sin n X 2 k 1 = seq 1 + n 4 π sin 2 n 1 X 2 n 1
1506 1504 1505 ax-mp seq 1 + k n if 2 n 0 4 n π sin n X 2 k 1 = seq 1 + n 4 π sin 2 n 1 X 2 n 1
1507 1 2 3 5 fourierswlem Y = if X mod T 0 π 1 1 + F X 2
1508 1507 eqcomi if X mod T 0 π 1 1 + F X 2 = Y
1509 1458 1506 1508 3brtr3i seq 1 + n 4 π sin 2 n 1 X 2 n 1 Y
1510 1509 a1i seq 1 + n 4 π sin 2 n 1 X 2 n 1 Y
1511 eqid n 4 π sin 2 n 1 X 2 n 1 = n 4 π sin 2 n 1 X 2 n 1
1512 65 69 74 divcld n 4 π
1513 1441 a1i n 2
1514 1513 66 mulcld n 2 n
1515 id 2 n 2 n
1516 1cnd 2 n 1
1517 1515 1516 subcld 2 n 2 n 1
1518 1514 1517 syl n 2 n 1
1519 1518 77 mulcld n 2 n 1 X
1520 1519 sincld n sin 2 n 1 X
1521 32 a1i n 2
1522 nnre n n
1523 1521 1522 remulcld n 2 n
1524 1523 recnd n 2 n
1525 1cnd n 1
1526 1524 1525 subcld n 2 n 1
1527 1red n 1
1528 39 1521 eqeltrid n 2 1
1529 1lt2 1 < 2
1530 1529 a1i n 1 < 2
1531 1530 39 breqtrrdi n 1 < 2 1
1532 47 a1i n 0 2
1533 nnge1 n 1 n
1534 1527 1522 1521 1532 1533 lemul2ad n 2 1 2 n
1535 1527 1528 1523 1531 1534 ltletrd n 1 < 2 n
1536 1527 1535 gtned n 2 n 1
1537 1524 1525 1536 subne0d n 2 n 1 0
1538 1520 1526 1537 divcld n sin 2 n 1 X 2 n 1
1539 1512 1538 mulcld n 4 π sin 2 n 1 X 2 n 1
1540 1511 1539 fmpti n 4 π sin 2 n 1 X 2 n 1 :
1541 1540 a1i n 4 π sin 2 n 1 X 2 n 1 :
1542 1541 ffvelrnda k n 4 π sin 2 n 1 X 2 n 1 k
1543 divcan6 π π 0 4 4 0 π 4 4 π = 1
1544 56 73 58 60 1543 mp4an π 4 4 π = 1
1545 1544 eqcomi 1 = π 4 4 π
1546 1545 oveq1i 1 sin 2 k 1 X 2 k 1 = π 4 4 π sin 2 k 1 X 2 k 1
1547 54 mulid2d k 1 sin 2 k 1 X 2 k 1 = sin 2 k 1 X 2 k 1
1548 60 a1i k 4 0
1549 1484 1487 1548 divcld k π 4
1550 1549 1492 54 mulassd k π 4 4 π sin 2 k 1 X 2 k 1 = π 4 4 π sin 2 k 1 X 2 k 1
1551 1546 1547 1550 3eqtr3a k sin 2 k 1 X 2 k 1 = π 4 4 π sin 2 k 1 X 2 k 1
1552 eqidd k n 4 π sin 2 n 1 X 2 n 1 = n 4 π sin 2 n 1 X 2 n 1
1553 13 oveq2d n = k 4 π sin 2 n 1 X 2 n 1 = 4 π sin 2 k 1 X 2 k 1
1554 1553 adantl k n = k 4 π sin 2 n 1 X 2 n 1 = 4 π sin 2 k 1 X 2 k 1
1555 1494 1469 eqeltrrdi k 4 π sin 2 k 1 X 2 k 1 V
1556 1552 1554 15 1555 fvmptd k n 4 π sin 2 n 1 X 2 n 1 k = 4 π sin 2 k 1 X 2 k 1
1557 1556 oveq2d k π 4 n 4 π sin 2 n 1 X 2 n 1 k = π 4 4 π sin 2 k 1 X 2 k 1
1558 1557 eqcomd k π 4 4 π sin 2 k 1 X 2 k 1 = π 4 n 4 π sin 2 n 1 X 2 n 1 k
1559 18 1551 1558 3eqtrd k n sin 2 n 1 X 2 n 1 k = π 4 n 4 π sin 2 n 1 X 2 n 1 k
1560 1559 adantl k n sin 2 n 1 X 2 n 1 k = π 4 n 4 π sin 2 n 1 X 2 n 1 k
1561 6 7 62 1510 1542 1560 isermulc2 seq 1 + n sin 2 n 1 X 2 n 1 π 4 Y
1562 climrel Rel
1563 1562 releldmi seq 1 + n sin 2 n 1 X 2 n 1 π 4 Y seq 1 + n sin 2 n 1 X 2 n 1 dom
1564 1561 1563 syl seq 1 + n sin 2 n 1 X 2 n 1 dom
1565 6 7 19 55 1564 isumclim2 seq 1 + n sin 2 n 1 X 2 n 1 k sin 2 k 1 X 2 k 1
1566 1565 mptru seq 1 + n sin 2 n 1 X 2 n 1 k sin 2 k 1 X 2 k 1
1567 1561 mptru seq 1 + n sin 2 n 1 X 2 n 1 π 4 Y
1568 climuni seq 1 + n sin 2 n 1 X 2 n 1 k sin 2 k 1 X 2 k 1 seq 1 + n sin 2 n 1 X 2 n 1 π 4 Y k sin 2 k 1 X 2 k 1 = π 4 Y
1569 1566 1567 1568 mp2an k sin 2 k 1 X 2 k 1 = π 4 Y
1570 1569 oveq2i 4 π k sin 2 k 1 X 2 k 1 = 4 π π 4 Y
1571 58 56 73 divcli 4 π
1572 56 58 60 divcli π 4
1573 1286 1151 eqeltri F X
1574 71 1573 ifcli if X mod π = 0 0 F X
1575 5 1574 eqeltri Y
1576 1575 recni Y
1577 1571 1572 1576 mulassi 4 π π 4 Y = 4 π π 4 Y
1578 1572 1571 1544 mulcomli 4 π π 4 = 1
1579 1578 oveq1i 4 π π 4 Y = 1 Y
1580 1576 mulid2i 1 Y = Y
1581 1579 1580 eqtri 4 π π 4 Y = Y
1582 1570 1577 1581 3eqtr2i 4 π k sin 2 k 1 X 2 k 1 = Y
1583 seqeq3 S = n sin 2 n 1 X 2 n 1 seq 1 + S = seq 1 + n sin 2 n 1 X 2 n 1
1584 4 1583 ax-mp seq 1 + S = seq 1 + n sin 2 n 1 X 2 n 1
1585 1584 1567 eqbrtri seq 1 + S π 4 Y
1586 1582 1585 pm3.2i 4 π k sin 2 k 1 X 2 k 1 = Y seq 1 + S π 4 Y