Metamath Proof Explorer


Theorem fourierdlem103

Description: The half lower part of the integral equal to the fourier partial sum, converges to half the left limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem103.f φ F :
fourierdlem103.xre φ X
fourierdlem103.p P = m p 0 m | p 0 = - π + X p m = π + X i 0 ..^ m p i < p i + 1
fourierdlem103.m φ M
fourierdlem103.v φ V P M
fourierdlem103.x φ X ran V
fourierdlem103.fcn φ i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
fourierdlem103.fbdioo φ i 0 ..^ M w t V i V i + 1 F t w
fourierdlem103.fdvcn φ i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
fourierdlem103.fdvbd φ i 0 ..^ M z t V i V i + 1 F t z
fourierdlem103.r φ i 0 ..^ M R F V i V i + 1 lim V i
fourierdlem103.l φ i 0 ..^ M L F V i V i + 1 lim V i + 1
fourierdlem103.h H = s π π if s = 0 0 F X + s if 0 < s Y W s
fourierdlem103.k K = s π π if s = 0 1 s 2 sin s 2
fourierdlem103.u U = s π π H s K s
fourierdlem103.s S = s π π sin n + 1 2 s
fourierdlem103.g G = s π π U s S s
fourierdlem103.z Z = m π 0 F X + s D m s ds
fourierdlem103.e E = n π 0 G s ds π
fourierdlem103.y φ Y F X +∞ lim X
fourierdlem103.w φ W F −∞ X lim X
fourierdlem103.a φ A F −∞ X lim X
fourierdlem103.b φ B F X +∞ lim X
fourierdlem103.d D = n s if s mod 2 π = 0 2 n + 1 2 π sin n + 1 2 s 2 π sin s 2
fourierdlem103.o O = U π d
fourierdlem103.t T = π d ran Q π d
fourierdlem103.n N = T 1
fourierdlem103.j J = ι f | f Isom < , < 0 N T
fourierdlem103.q Q = i 0 M V i X
fourierdlem103.1 C = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1
fourierdlem103.ch χ φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2
Assertion fourierdlem103 φ Z W 2

Proof

Step Hyp Ref Expression
1 fourierdlem103.f φ F :
2 fourierdlem103.xre φ X
3 fourierdlem103.p P = m p 0 m | p 0 = - π + X p m = π + X i 0 ..^ m p i < p i + 1
4 fourierdlem103.m φ M
5 fourierdlem103.v φ V P M
6 fourierdlem103.x φ X ran V
7 fourierdlem103.fcn φ i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
8 fourierdlem103.fbdioo φ i 0 ..^ M w t V i V i + 1 F t w
9 fourierdlem103.fdvcn φ i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
10 fourierdlem103.fdvbd φ i 0 ..^ M z t V i V i + 1 F t z
11 fourierdlem103.r φ i 0 ..^ M R F V i V i + 1 lim V i
12 fourierdlem103.l φ i 0 ..^ M L F V i V i + 1 lim V i + 1
13 fourierdlem103.h H = s π π if s = 0 0 F X + s if 0 < s Y W s
14 fourierdlem103.k K = s π π if s = 0 1 s 2 sin s 2
15 fourierdlem103.u U = s π π H s K s
16 fourierdlem103.s S = s π π sin n + 1 2 s
17 fourierdlem103.g G = s π π U s S s
18 fourierdlem103.z Z = m π 0 F X + s D m s ds
19 fourierdlem103.e E = n π 0 G s ds π
20 fourierdlem103.y φ Y F X +∞ lim X
21 fourierdlem103.w φ W F −∞ X lim X
22 fourierdlem103.a φ A F −∞ X lim X
23 fourierdlem103.b φ B F X +∞ lim X
24 fourierdlem103.d D = n s if s mod 2 π = 0 2 n + 1 2 π sin n + 1 2 s 2 π sin s 2
25 fourierdlem103.o O = U π d
26 fourierdlem103.t T = π d ran Q π d
27 fourierdlem103.n N = T 1
28 fourierdlem103.j J = ι f | f Isom < , < 0 N T
29 fourierdlem103.q Q = i 0 M V i X
30 fourierdlem103.1 C = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1
31 fourierdlem103.ch χ φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2
32 eqid 1 = 1
33 1zzd φ 1
34 nfv n φ
35 nfmpt1 _ n n π 0 G s ds
36 nfmpt1 _ n n π
37 nfmpt1 _ n n π 0 G s ds π
38 19 37 nfcxfr _ n E
39 nnuz = 1
40 pire π
41 40 renegcli π
42 41 a1i φ d π 0 π
43 elioore d π 0 d
44 43 adantl φ d π 0 d
45 ioossre X +∞
46 45 a1i φ X +∞
47 1 46 fssresd φ F X +∞ : X +∞
48 ioosscn X +∞
49 48 a1i φ X +∞
50 eqid TopOpen fld = TopOpen fld
51 pnfxr +∞ *
52 51 a1i φ +∞ *
53 2 ltpnfd φ X < +∞
54 50 52 2 53 lptioo1cn φ X limPt TopOpen fld X +∞
55 47 49 54 20 limcrecl φ Y
56 ioossre −∞ X
57 56 a1i φ −∞ X
58 1 57 fssresd φ F −∞ X : −∞ X
59 ioosscn −∞ X
60 59 a1i φ −∞ X
61 mnfxr −∞ *
62 61 a1i φ −∞ *
63 2 mnfltd φ −∞ < X
64 50 62 2 63 lptioo2cn φ X limPt TopOpen fld −∞ X
65 58 60 64 21 limcrecl φ W
66 1 2 55 65 13 14 15 fourierdlem55 φ U : π π
67 ax-resscn
68 67 a1i φ
69 66 68 fssd φ U : π π
70 69 adantr φ d π 0 U : π π
71 41 a1i d π 0 π
72 40 a1i d π 0 π
73 71 leidd d π 0 π π
74 0red d π 0 0
75 41 rexri π *
76 0xr 0 *
77 iooltub π * 0 * d π 0 d < 0
78 75 76 77 mp3an12 d π 0 d < 0
79 pipos 0 < π
80 79 a1i d π 0 0 < π
81 43 74 72 78 80 lttrd d π 0 d < π
82 43 72 81 ltled d π 0 d π
83 iccss π π π π d π π d π π
84 71 72 73 82 83 syl22anc d π 0 π d π π
85 84 adantl φ d π 0 π d π π
86 70 85 fssresd φ d π 0 U π d : π d
87 25 a1i φ d π 0 O = U π d
88 87 feq1d φ d π 0 O : π d U π d : π d
89 86 88 mpbird φ d π 0 O : π d
90 41 elexi π V
91 90 prid1 π π d
92 elun1 π π d π π d ran Q π d
93 91 92 ax-mp π π d ran Q π d
94 93 26 eleqtrri π T
95 94 ne0ii T
96 95 a1i φ T
97 prfi π d Fin
98 97 a1i φ π d Fin
99 fzfi 0 M Fin
100 29 rnmptfi 0 M Fin ran Q Fin
101 99 100 ax-mp ran Q Fin
102 101 a1i φ ran Q Fin
103 infi ran Q Fin ran Q π d Fin
104 102 103 syl φ ran Q π d Fin
105 unfi π d Fin ran Q π d Fin π d ran Q π d Fin
106 98 104 105 syl2anc φ π d ran Q π d Fin
107 26 106 eqeltrid φ T Fin
108 hashnncl T Fin T T
109 107 108 syl φ T T
110 96 109 mpbird φ T
111 nnm1nn0 T T 1 0
112 110 111 syl φ T 1 0
113 27 112 eqeltrid φ N 0
114 113 adantr φ d π 0 N 0
115 0red φ d π 0 0
116 1red φ d π 0 1
117 114 nn0red φ d π 0 N
118 0lt1 0 < 1
119 118 a1i φ d π 0 0 < 1
120 2re 2
121 120 a1i φ d π 0 2
122 110 nnred φ T
123 122 adantr φ d π 0 T
124 ioogtlb π * 0 * d π 0 π < d
125 75 76 124 mp3an12 d π 0 π < d
126 71 125 ltned d π 0 π d
127 126 adantl φ d π 0 π d
128 hashprg π d π d π d = 2
129 42 44 128 syl2anc φ d π 0 π d π d = 2
130 127 129 mpbid φ d π 0 π d = 2
131 130 eqcomd φ d π 0 2 = π d
132 107 adantr φ d π 0 T Fin
133 ssun1 π d π d ran Q π d
134 133 26 sseqtrri π d T
135 hashssle T Fin π d T π d T
136 132 134 135 sylancl φ d π 0 π d T
137 131 136 eqbrtrd φ d π 0 2 T
138 121 123 116 137 lesub1dd φ d π 0 2 1 T 1
139 1e2m1 1 = 2 1
140 138 139 27 3brtr4g φ d π 0 1 N
141 115 116 117 119 140 ltletrd φ d π 0 0 < N
142 141 gt0ne0d φ d π 0 N 0
143 114 142 jca φ d π 0 N 0 N 0
144 elnnne0 N N 0 N 0
145 143 144 sylibr φ d π 0 N
146 73 adantl φ d π 0 π π
147 71 43 125 ltled d π 0 π d
148 147 adantl φ d π 0 π d
149 42 44 42 146 148 eliccd φ d π 0 π π d
150 44 leidd φ d π 0 d d
151 42 44 44 148 150 eliccd φ d π 0 d π d
152 149 151 jca φ d π 0 π π d d π d
153 vex d V
154 90 153 prss π π d d π d π d π d
155 152 154 sylib φ d π 0 π d π d
156 inss2 ran Q π d π d
157 156 a1i φ d π 0 ran Q π d π d
158 ioossicc π d π d
159 157 158 sstrdi φ d π 0 ran Q π d π d
160 155 159 unssd φ d π 0 π d ran Q π d π d
161 26 160 eqsstrid φ d π 0 T π d
162 94 a1i φ d π 0 π T
163 153 prid2 d π d
164 elun1 d π d d π d ran Q π d
165 163 164 ax-mp d π d ran Q π d
166 165 26 eleqtrri d T
167 166 a1i φ d π 0 d T
168 132 27 28 42 44 161 162 167 fourierdlem52 φ d π 0 J : 0 N π d J 0 = π J N = d
169 168 simpld φ d π 0 J : 0 N π d J 0 = π
170 169 simpld φ d π 0 J : 0 N π d
171 169 simprd φ d π 0 J 0 = π
172 168 simprd φ d π 0 J N = d
173 elfzoelz k 0 ..^ N k
174 173 zred k 0 ..^ N k
175 174 adantl φ d π 0 k 0 ..^ N k
176 175 ltp1d φ d π 0 k 0 ..^ N k < k + 1
177 71 43 jca d π 0 π d
178 90 153 prss π d π d
179 177 178 sylib d π 0 π d
180 179 adantl φ d π 0 π d
181 ioossre π d
182 156 181 sstri ran Q π d
183 182 a1i φ d π 0 ran Q π d
184 180 183 unssd φ d π 0 π d ran Q π d
185 26 184 eqsstrid φ d π 0 T
186 132 185 28 27 fourierdlem36 φ d π 0 J Isom < , < 0 N T
187 186 adantr φ d π 0 k 0 ..^ N J Isom < , < 0 N T
188 elfzofz k 0 ..^ N k 0 N
189 188 adantl φ d π 0 k 0 ..^ N k 0 N
190 fzofzp1 k 0 ..^ N k + 1 0 N
191 190 adantl φ d π 0 k 0 ..^ N k + 1 0 N
192 isorel J Isom < , < 0 N T k 0 N k + 1 0 N k < k + 1 J k < J k + 1
193 187 189 191 192 syl12anc φ d π 0 k 0 ..^ N k < k + 1 J k < J k + 1
194 176 193 mpbid φ d π 0 k 0 ..^ N J k < J k + 1
195 66 adantr φ d π 0 U : π π
196 195 85 feqresmpt φ d π 0 U π d = s π d U s
197 85 sselda φ d π 0 s π d s π π
198 1 2 55 65 13 fourierdlem9 φ H : π π
199 198 ad2antrr φ d π 0 s π d H : π π
200 199 197 ffvelrnd φ d π 0 s π d H s
201 14 fourierdlem43 K : π π
202 201 a1i φ d π 0 s π d K : π π
203 202 197 ffvelrnd φ d π 0 s π d K s
204 200 203 remulcld φ d π 0 s π d H s K s
205 15 fvmpt2 s π π H s K s U s = H s K s
206 197 204 205 syl2anc φ d π 0 s π d U s = H s K s
207 41 a1i d π 0 s π d π
208 43 adantr d π 0 s π d d
209 simpr d π 0 s π d s π d
210 eliccre π d s π d s
211 207 208 209 210 syl3anc d π 0 s π d s
212 0red d π 0 s π d 0
213 75 a1i d π 0 s π d π *
214 208 rexrd d π 0 s π d d *
215 iccleub π * d * s π d s d
216 213 214 209 215 syl3anc d π 0 s π d s d
217 78 adantr d π 0 s π d d < 0
218 211 208 212 216 217 lelttrd d π 0 s π d s < 0
219 211 218 ltned d π 0 s π d s 0
220 219 adantll φ d π 0 s π d s 0
221 220 neneqd φ d π 0 s π d ¬ s = 0
222 221 iffalsed φ d π 0 s π d if s = 0 0 F X + s if 0 < s Y W s = F X + s if 0 < s Y W s
223 211 212 218 ltnsymd d π 0 s π d ¬ 0 < s
224 223 adantll φ d π 0 s π d ¬ 0 < s
225 224 iffalsed φ d π 0 s π d if 0 < s Y W = W
226 225 oveq2d φ d π 0 s π d F X + s if 0 < s Y W = F X + s W
227 226 oveq1d φ d π 0 s π d F X + s if 0 < s Y W s = F X + s W s
228 222 227 eqtrd φ d π 0 s π d if s = 0 0 F X + s if 0 < s Y W s = F X + s W s
229 1 ad2antrr φ d π 0 s π d F :
230 2 ad2antrr φ d π 0 s π d X
231 iccssre π π π π
232 41 40 231 mp2an π π
233 232 197 sseldi φ d π 0 s π d s
234 230 233 readdcld φ d π 0 s π d X + s
235 229 234 ffvelrnd φ d π 0 s π d F X + s
236 65 ad2antrr φ d π 0 s π d W
237 235 236 resubcld φ d π 0 s π d F X + s W
238 237 233 220 redivcld φ d π 0 s π d F X + s W s
239 228 238 eqeltrd φ d π 0 s π d if s = 0 0 F X + s if 0 < s Y W s
240 13 fvmpt2 s π π if s = 0 0 F X + s if 0 < s Y W s H s = if s = 0 0 F X + s if 0 < s Y W s
241 197 239 240 syl2anc φ d π 0 s π d H s = if s = 0 0 F X + s if 0 < s Y W s
242 241 222 227 3eqtrd φ d π 0 s π d H s = F X + s W s
243 40 a1i d π 0 s π d π
244 243 renegcld d π 0 s π d π
245 iccgelb π * d * s π d π s
246 213 214 209 245 syl3anc d π 0 s π d π s
247 81 adantr d π 0 s π d d < π
248 211 208 243 216 247 lelttrd d π 0 s π d s < π
249 211 243 248 ltled d π 0 s π d s π
250 244 243 211 246 249 eliccd d π 0 s π d s π π
251 219 neneqd d π 0 s π d ¬ s = 0
252 251 iffalsed d π 0 s π d if s = 0 1 s 2 sin s 2 = s 2 sin s 2
253 120 a1i d π 0 s π d 2
254 211 rehalfcld d π 0 s π d s 2
255 254 resincld d π 0 s π d sin s 2
256 253 255 remulcld d π 0 s π d 2 sin s 2
257 2cn 2
258 257 a1i d π 0 s π d 2
259 211 recnd d π 0 s π d s
260 259 halfcld d π 0 s π d s 2
261 260 sincld d π 0 s π d sin s 2
262 2ne0 2 0
263 262 a1i d π 0 s π d 2 0
264 fourierdlem44 s π π s 0 sin s 2 0
265 250 219 264 syl2anc d π 0 s π d sin s 2 0
266 258 261 263 265 mulne0d d π 0 s π d 2 sin s 2 0
267 211 256 266 redivcld d π 0 s π d s 2 sin s 2
268 252 267 eqeltrd d π 0 s π d if s = 0 1 s 2 sin s 2
269 14 fvmpt2 s π π if s = 0 1 s 2 sin s 2 K s = if s = 0 1 s 2 sin s 2
270 250 268 269 syl2anc d π 0 s π d K s = if s = 0 1 s 2 sin s 2
271 270 adantll φ d π 0 s π d K s = if s = 0 1 s 2 sin s 2
272 242 271 oveq12d φ d π 0 s π d H s K s = F X + s W s if s = 0 1 s 2 sin s 2
273 221 iffalsed φ d π 0 s π d if s = 0 1 s 2 sin s 2 = s 2 sin s 2
274 273 oveq2d φ d π 0 s π d F X + s W s if s = 0 1 s 2 sin s 2 = F X + s W s s 2 sin s 2
275 206 272 274 3eqtrd φ d π 0 s π d U s = F X + s W s s 2 sin s 2
276 275 mpteq2dva φ d π 0 s π d U s = s π d F X + s W s s 2 sin s 2
277 87 196 276 3eqtrd φ d π 0 O = s π d F X + s W s s 2 sin s 2
278 277 adantr φ d π 0 k 0 ..^ N O = s π d F X + s W s s 2 sin s 2
279 278 reseq1d φ d π 0 k 0 ..^ N O J k J k + 1 = s π d F X + s W s s 2 sin s 2 J k J k + 1
280 1 adantr φ d π 0 F :
281 2 adantr φ d π 0 X
282 4 adantr φ d π 0 M
283 5 adantr φ d π 0 V P M
284 7 adantlr φ d π 0 i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
285 11 adantlr φ d π 0 i 0 ..^ M R F V i V i + 1 lim V i
286 12 adantlr φ d π 0 i 0 ..^ M L F V i V i + 1 lim V i + 1
287 125 adantl φ d π 0 π < d
288 75 a1i φ d π 0 π *
289 76 a1i φ d π 0 0 *
290 78 adantl φ d π 0 d < 0
291 288 44 289 290 gtnelicc φ d π 0 ¬ 0 π d
292 65 adantr φ d π 0 W
293 eqid s π d F X + s W s s 2 sin s 2 = s π d F X + s W s s 2 sin s 2
294 eqid if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 = if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2
295 eqid if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2 = if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2
296 fveq2 l = i Q l = Q i
297 oveq1 l = i l + 1 = i + 1
298 297 fveq2d l = i Q l + 1 = Q i + 1
299 296 298 oveq12d l = i Q l Q l + 1 = Q i Q i + 1
300 299 sseq2d l = i J k J k + 1 Q l Q l + 1 J k J k + 1 Q i Q i + 1
301 300 cbvriotavw ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 = ι i 0 ..^ M | J k J k + 1 Q i Q i + 1
302 280 281 3 282 283 284 285 286 42 44 287 85 291 292 293 29 26 27 28 294 295 301 fourierdlem86 φ d π 0 k 0 ..^ N if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 s π d F X + s W s s 2 sin s 2 J k J k + 1 lim J k + 1 if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2 s π d F X + s W s s 2 sin s 2 J k J k + 1 lim J k s π d F X + s W s s 2 sin s 2 J k J k + 1 : J k J k + 1 cn
303 302 simprd φ d π 0 k 0 ..^ N s π d F X + s W s s 2 sin s 2 J k J k + 1 : J k J k + 1 cn
304 279 303 eqeltrd φ d π 0 k 0 ..^ N O J k J k + 1 : J k J k + 1 cn
305 302 simpld φ d π 0 k 0 ..^ N if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 s π d F X + s W s s 2 sin s 2 J k J k + 1 lim J k + 1 if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2 s π d F X + s W s s 2 sin s 2 J k J k + 1 lim J k
306 305 simpld φ d π 0 k 0 ..^ N if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 s π d F X + s W s s 2 sin s 2 J k J k + 1 lim J k + 1
307 278 eqcomd φ d π 0 k 0 ..^ N s π d F X + s W s s 2 sin s 2 = O
308 307 reseq1d φ d π 0 k 0 ..^ N s π d F X + s W s s 2 sin s 2 J k J k + 1 = O J k J k + 1
309 308 oveq1d φ d π 0 k 0 ..^ N s π d F X + s W s s 2 sin s 2 J k J k + 1 lim J k + 1 = O J k J k + 1 lim J k + 1
310 306 309 eleqtrd φ d π 0 k 0 ..^ N if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 O J k J k + 1 lim J k + 1
311 305 simprd φ d π 0 k 0 ..^ N if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2 s π d F X + s W s s 2 sin s 2 J k J k + 1 lim J k
312 308 oveq1d φ d π 0 k 0 ..^ N s π d F X + s W s s 2 sin s 2 J k J k + 1 lim J k = O J k J k + 1 lim J k
313 311 312 eleqtrd φ d π 0 k 0 ..^ N if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2 O J k J k + 1 lim J k
314 eqid D O = D O
315 89 adantr φ d π 0 k 0 ..^ N O : π d
316 41 a1i φ d π 0 k 0 ..^ N s J k J k + 1 π
317 44 ad2antrr φ d π 0 k 0 ..^ N s J k J k + 1 d
318 elioore s J k J k + 1 s
319 318 adantl φ d π 0 k 0 ..^ N s J k J k + 1 s
320 85 232 sstrdi φ d π 0 π d
321 320 adantr φ d π 0 k 0 ..^ N π d
322 170 adantr φ d π 0 k 0 ..^ N J : 0 N π d
323 322 189 ffvelrnd φ d π 0 k 0 ..^ N J k π d
324 321 323 sseldd φ d π 0 k 0 ..^ N J k
325 324 adantr φ d π 0 k 0 ..^ N s J k J k + 1 J k
326 75 a1i φ d π 0 k 0 ..^ N π *
327 44 adantr φ d π 0 k 0 ..^ N d
328 327 rexrd φ d π 0 k 0 ..^ N d *
329 iccgelb π * d * J k π d π J k
330 326 328 323 329 syl3anc φ d π 0 k 0 ..^ N π J k
331 330 adantr φ d π 0 k 0 ..^ N s J k J k + 1 π J k
332 325 rexrd φ d π 0 k 0 ..^ N s J k J k + 1 J k *
333 322 191 ffvelrnd φ d π 0 k 0 ..^ N J k + 1 π d
334 321 333 sseldd φ d π 0 k 0 ..^ N J k + 1
335 334 rexrd φ d π 0 k 0 ..^ N J k + 1 *
336 335 adantr φ d π 0 k 0 ..^ N s J k J k + 1 J k + 1 *
337 simpr φ d π 0 k 0 ..^ N s J k J k + 1 s J k J k + 1
338 ioogtlb J k * J k + 1 * s J k J k + 1 J k < s
339 332 336 337 338 syl3anc φ d π 0 k 0 ..^ N s J k J k + 1 J k < s
340 316 325 319 331 339 lelttrd φ d π 0 k 0 ..^ N s J k J k + 1 π < s
341 316 319 340 ltled φ d π 0 k 0 ..^ N s J k J k + 1 π s
342 334 adantr φ d π 0 k 0 ..^ N s J k J k + 1 J k + 1
343 iooltub J k * J k + 1 * s J k J k + 1 s < J k + 1
344 332 336 337 343 syl3anc φ d π 0 k 0 ..^ N s J k J k + 1 s < J k + 1
345 iccleub π * d * J k + 1 π d J k + 1 d
346 326 328 333 345 syl3anc φ d π 0 k 0 ..^ N J k + 1 d
347 346 adantr φ d π 0 k 0 ..^ N s J k J k + 1 J k + 1 d
348 319 342 317 344 347 ltletrd φ d π 0 k 0 ..^ N s J k J k + 1 s < d
349 319 317 348 ltled φ d π 0 k 0 ..^ N s J k J k + 1 s d
350 316 317 319 341 349 eliccd φ d π 0 k 0 ..^ N s J k J k + 1 s π d
351 350 ralrimiva φ d π 0 k 0 ..^ N s J k J k + 1 s π d
352 dfss3 J k J k + 1 π d s J k J k + 1 s π d
353 351 352 sylibr φ d π 0 k 0 ..^ N J k J k + 1 π d
354 315 353 feqresmpt φ d π 0 k 0 ..^ N O J k J k + 1 = s J k J k + 1 O s
355 simplll φ d π 0 k 0 ..^ N s J k J k + 1 φ
356 simpllr φ d π 0 k 0 ..^ N s J k J k + 1 d π 0
357 25 fveq1i O s = U π d s
358 357 a1i φ d π 0 s π d O s = U π d s
359 fvres s π d U π d s = U s
360 359 adantl φ d π 0 s π d U π d s = U s
361 271 273 eqtrd φ d π 0 s π d K s = s 2 sin s 2
362 242 361 oveq12d φ d π 0 s π d H s K s = F X + s W s s 2 sin s 2
363 237 recnd φ d π 0 s π d F X + s W
364 259 adantll φ d π 0 s π d s
365 257 a1i φ d π 0 s π d 2
366 364 halfcld φ d π 0 s π d s 2
367 366 sincld φ d π 0 s π d sin s 2
368 365 367 mulcld φ d π 0 s π d 2 sin s 2
369 266 adantll φ d π 0 s π d 2 sin s 2 0
370 363 364 368 220 369 dmdcan2d φ d π 0 s π d F X + s W s s 2 sin s 2 = F X + s W 2 sin s 2
371 206 362 370 3eqtrd φ d π 0 s π d U s = F X + s W 2 sin s 2
372 358 360 371 3eqtrd φ d π 0 s π d O s = F X + s W 2 sin s 2
373 355 356 350 372 syl21anc φ d π 0 k 0 ..^ N s J k J k + 1 O s = F X + s W 2 sin s 2
374 355 356 350 370 syl21anc φ d π 0 k 0 ..^ N s J k J k + 1 F X + s W s s 2 sin s 2 = F X + s W 2 sin s 2
375 374 eqcomd φ d π 0 k 0 ..^ N s J k J k + 1 F X + s W 2 sin s 2 = F X + s W s s 2 sin s 2
376 eqidd φ k 0 ..^ N s J k J k + 1 t J k J k + 1 F X + t W t = t J k J k + 1 F X + t W t
377 oveq2 t = s X + t = X + s
378 377 fveq2d t = s F X + t = F X + s
379 378 oveq1d t = s F X + t W = F X + s W
380 id t = s t = s
381 379 380 oveq12d t = s F X + t W t = F X + s W s
382 381 adantl φ k 0 ..^ N s J k J k + 1 t = s F X + t W t = F X + s W s
383 simpr φ k 0 ..^ N s J k J k + 1 s J k J k + 1
384 ovex F X + s W s V
385 384 a1i φ k 0 ..^ N s J k J k + 1 F X + s W s V
386 376 382 383 385 fvmptd φ k 0 ..^ N s J k J k + 1 t J k J k + 1 F X + t W t s = F X + s W s
387 eqidd φ k 0 ..^ N s J k J k + 1 t J k J k + 1 t 2 sin t 2 = t J k J k + 1 t 2 sin t 2
388 oveq1 t = s t 2 = s 2
389 388 fveq2d t = s sin t 2 = sin s 2
390 389 oveq2d t = s 2 sin t 2 = 2 sin s 2
391 380 390 oveq12d t = s t 2 sin t 2 = s 2 sin s 2
392 391 adantl φ k 0 ..^ N s J k J k + 1 t = s t 2 sin t 2 = s 2 sin s 2
393 ovex s 2 sin s 2 V
394 393 a1i φ k 0 ..^ N s J k J k + 1 s 2 sin s 2 V
395 387 392 383 394 fvmptd φ k 0 ..^ N s J k J k + 1 t J k J k + 1 t 2 sin t 2 s = s 2 sin s 2
396 386 395 oveq12d φ k 0 ..^ N s J k J k + 1 t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s = F X + s W s s 2 sin s 2
397 396 eqcomd φ k 0 ..^ N s J k J k + 1 F X + s W s s 2 sin s 2 = t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s
398 397 adantllr φ d π 0 k 0 ..^ N s J k J k + 1 F X + s W s s 2 sin s 2 = t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s
399 373 375 398 3eqtrd φ d π 0 k 0 ..^ N s J k J k + 1 O s = t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s
400 399 mpteq2dva φ d π 0 k 0 ..^ N s J k J k + 1 O s = s J k J k + 1 t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s
401 354 400 eqtr2d φ d π 0 k 0 ..^ N s J k J k + 1 t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s = O J k J k + 1
402 401 oveq2d φ d π 0 k 0 ..^ N ds J k J k + 1 t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s d s = D O J k J k + 1
403 67 a1i φ d π 0 k 0 ..^ N
404 353 321 sstrd φ d π 0 k 0 ..^ N J k J k + 1
405 50 tgioo2 topGen ran . = TopOpen fld 𝑡
406 50 405 dvres O : π d π d J k J k + 1 D O J k J k + 1 = O int topGen ran . J k J k + 1
407 403 315 321 404 406 syl22anc φ d π 0 k 0 ..^ N D O J k J k + 1 = O int topGen ran . J k J k + 1
408 ioontr int topGen ran . J k J k + 1 = J k J k + 1
409 408 a1i φ d π 0 k 0 ..^ N int topGen ran . J k J k + 1 = J k J k + 1
410 409 reseq2d φ d π 0 k 0 ..^ N O int topGen ran . J k J k + 1 = O J k J k + 1
411 402 407 410 3eqtrrd φ d π 0 k 0 ..^ N O J k J k + 1 = ds J k J k + 1 t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s d s
412 1 ad2antrr φ d π 0 k 0 ..^ N F :
413 2 ad2antrr φ d π 0 k 0 ..^ N X
414 4 ad2antrr φ d π 0 k 0 ..^ N M
415 5 ad2antrr φ d π 0 k 0 ..^ N V P M
416 9 ad4ant14 φ d π 0 k 0 ..^ N i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
417 85 adantr φ d π 0 k 0 ..^ N π d π π
418 353 417 sstrd φ d π 0 k 0 ..^ N J k J k + 1 π π
419 324 rexrd φ d π 0 k 0 ..^ N J k *
420 76 a1i φ d π 0 k 0 ..^ N 0 *
421 0red φ d π 0 k 0 ..^ N 0
422 78 ad2antlr φ d π 0 k 0 ..^ N d < 0
423 334 327 421 346 422 lelttrd φ d π 0 k 0 ..^ N J k + 1 < 0
424 419 334 420 423 gtnelicc φ d π 0 k 0 ..^ N ¬ 0 J k J k + 1
425 65 ad2antrr φ d π 0 k 0 ..^ N W
426 41 a1i φ d π 0 k 0 ..^ N π
427 125 ad2antlr φ d π 0 k 0 ..^ N π < d
428 simpr φ d π 0 k 0 ..^ N k 0 ..^ N
429 biid φ d π 0 k 0 ..^ N i 0 ..^ M J k J k + 1 Q i Q i + 1 v 0 ..^ M J k J k + 1 Q v Q v + 1 φ d π 0 k 0 ..^ N i 0 ..^ M J k J k + 1 Q i Q i + 1 v 0 ..^ M J k J k + 1 Q v Q v + 1
430 413 3 414 415 426 327 427 417 29 26 27 28 428 301 429 fourierdlem50 φ d π 0 k 0 ..^ N ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 0 ..^ M J k J k + 1 Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1
431 430 simpld φ d π 0 k 0 ..^ N ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 0 ..^ M
432 430 simprd φ d π 0 k 0 ..^ N J k J k + 1 Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1
433 381 cbvmptv t J k J k + 1 F X + t W t = s J k J k + 1 F X + s W s
434 391 cbvmptv t J k J k + 1 t 2 sin t 2 = s J k J k + 1 s 2 sin s 2
435 eqid s J k J k + 1 t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s = s J k J k + 1 t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s
436 412 413 3 414 415 416 324 334 194 418 424 425 29 431 432 433 434 435 fourierdlem72 φ d π 0 k 0 ..^ N ds J k J k + 1 t J k J k + 1 F X + t W t s t J k J k + 1 t 2 sin t 2 s d s : J k J k + 1 cn
437 411 436 eqeltrd φ d π 0 k 0 ..^ N O J k J k + 1 : J k J k + 1 cn
438 eqid s π d F X + s W 2 sin s 2 = s π d F X + s W 2 sin s 2
439 eqid X + J k X + J k + 1 = X + J k X + J k + 1
440 30 431 eqeltrid φ d π 0 k 0 ..^ N C 0 ..^ M
441 simpll φ d π 0 k 0 ..^ N φ
442 441 440 jca φ d π 0 k 0 ..^ N φ C 0 ..^ M
443 eleq1 i = C i 0 ..^ M C 0 ..^ M
444 443 anbi2d i = C φ i 0 ..^ M φ C 0 ..^ M
445 fveq2 i = C V i = V C
446 oveq1 i = C i + 1 = C + 1
447 446 fveq2d i = C V i + 1 = V C + 1
448 445 447 oveq12d i = C V i V i + 1 = V C V C + 1
449 raleq V i V i + 1 = V C V C + 1 t V i V i + 1 F t w t V C V C + 1 F t w
450 448 449 syl i = C t V i V i + 1 F t w t V C V C + 1 F t w
451 450 rexbidv i = C w t V i V i + 1 F t w w t V C V C + 1 F t w
452 444 451 imbi12d i = C φ i 0 ..^ M w t V i V i + 1 F t w φ C 0 ..^ M w t V C V C + 1 F t w
453 452 8 vtoclg C 0 ..^ M φ C 0 ..^ M w t V C V C + 1 F t w
454 440 442 453 sylc φ d π 0 k 0 ..^ N w t V C V C + 1 F t w
455 nfv t φ d π 0 k 0 ..^ N
456 nfra1 t t V C V C + 1 F t w
457 455 456 nfan t φ d π 0 k 0 ..^ N t V C V C + 1 F t w
458 simplr φ d π 0 k 0 ..^ N t V C V C + 1 F t w t X + J k X + J k + 1 t V C V C + 1 F t w
459 41 a1i φ π
460 459 2 readdcld φ - π + X
461 40 a1i φ π
462 461 2 readdcld φ π + X
463 460 462 iccssred φ - π + X π + X
464 ressxr *
465 463 464 sstrdi φ - π + X π + X *
466 465 ad2antrr φ d π 0 k 0 ..^ N - π + X π + X *
467 3 414 415 fourierdlem15 φ d π 0 k 0 ..^ N V : 0 M - π + X π + X
468 elfzofz C 0 ..^ M C 0 M
469 440 468 syl φ d π 0 k 0 ..^ N C 0 M
470 467 469 ffvelrnd φ d π 0 k 0 ..^ N V C - π + X π + X
471 466 470 sseldd φ d π 0 k 0 ..^ N V C *
472 471 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 V C *
473 fzofzp1 C 0 ..^ M C + 1 0 M
474 440 473 syl φ d π 0 k 0 ..^ N C + 1 0 M
475 467 474 ffvelrnd φ d π 0 k 0 ..^ N V C + 1 - π + X π + X
476 466 475 sseldd φ d π 0 k 0 ..^ N V C + 1 *
477 476 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 V C + 1 *
478 elioore t X + J k X + J k + 1 t
479 478 adantl φ d π 0 k 0 ..^ N t X + J k X + J k + 1 t
480 40 a1i φ d π 0 k 0 ..^ N π
481 426 480 413 3 414 415 469 29 fourierdlem13 φ d π 0 k 0 ..^ N Q C = V C X V C = X + Q C
482 481 simprd φ d π 0 k 0 ..^ N V C = X + Q C
483 482 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 V C = X + Q C
484 463 ad2antrr φ d π 0 k 0 ..^ N - π + X π + X
485 484 470 sseldd φ d π 0 k 0 ..^ N V C
486 485 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 V C
487 483 486 eqeltrrd φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + Q C
488 413 324 readdcld φ d π 0 k 0 ..^ N X + J k
489 488 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + J k
490 481 simpld φ d π 0 k 0 ..^ N Q C = V C X
491 485 413 resubcld φ d π 0 k 0 ..^ N V C X
492 490 491 eqeltrd φ d π 0 k 0 ..^ N Q C
493 426 480 413 3 414 415 474 29 fourierdlem13 φ d π 0 k 0 ..^ N Q C + 1 = V C + 1 X V C + 1 = X + Q C + 1
494 493 simpld φ d π 0 k 0 ..^ N Q C + 1 = V C + 1 X
495 484 475 sseldd φ d π 0 k 0 ..^ N V C + 1
496 495 413 resubcld φ d π 0 k 0 ..^ N V C + 1 X
497 494 496 eqeltrd φ d π 0 k 0 ..^ N Q C + 1
498 30 eqcomi ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 = C
499 498 fveq2i Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 = Q C
500 498 oveq1i ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 = C + 1
501 500 fveq2i Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 = Q C + 1
502 499 501 oveq12i Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 = Q C Q C + 1
503 432 502 sseqtrdi φ d π 0 k 0 ..^ N J k J k + 1 Q C Q C + 1
504 492 497 324 334 194 503 fourierdlem10 φ d π 0 k 0 ..^ N Q C J k J k + 1 Q C + 1
505 504 simpld φ d π 0 k 0 ..^ N Q C J k
506 492 324 413 505 leadd2dd φ d π 0 k 0 ..^ N X + Q C X + J k
507 506 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + Q C X + J k
508 489 rexrd φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + J k *
509 413 334 readdcld φ d π 0 k 0 ..^ N X + J k + 1
510 509 rexrd φ d π 0 k 0 ..^ N X + J k + 1 *
511 510 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + J k + 1 *
512 simpr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 t X + J k X + J k + 1
513 ioogtlb X + J k * X + J k + 1 * t X + J k X + J k + 1 X + J k < t
514 508 511 512 513 syl3anc φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + J k < t
515 487 489 479 507 514 lelttrd φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + Q C < t
516 483 515 eqbrtrd φ d π 0 k 0 ..^ N t X + J k X + J k + 1 V C < t
517 509 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + J k + 1
518 493 simprd φ d π 0 k 0 ..^ N V C + 1 = X + Q C + 1
519 518 495 eqeltrrd φ d π 0 k 0 ..^ N X + Q C + 1
520 519 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + Q C + 1
521 iooltub X + J k * X + J k + 1 * t X + J k X + J k + 1 t < X + J k + 1
522 508 511 512 521 syl3anc φ d π 0 k 0 ..^ N t X + J k X + J k + 1 t < X + J k + 1
523 504 simprd φ d π 0 k 0 ..^ N J k + 1 Q C + 1
524 334 497 413 523 leadd2dd φ d π 0 k 0 ..^ N X + J k + 1 X + Q C + 1
525 524 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + J k + 1 X + Q C + 1
526 479 517 520 522 525 ltletrd φ d π 0 k 0 ..^ N t X + J k X + J k + 1 t < X + Q C + 1
527 518 eqcomd φ d π 0 k 0 ..^ N X + Q C + 1 = V C + 1
528 527 adantr φ d π 0 k 0 ..^ N t X + J k X + J k + 1 X + Q C + 1 = V C + 1
529 526 528 breqtrd φ d π 0 k 0 ..^ N t X + J k X + J k + 1 t < V C + 1
530 472 477 479 516 529 eliood φ d π 0 k 0 ..^ N t X + J k X + J k + 1 t V C V C + 1
531 530 adantlr φ d π 0 k 0 ..^ N t V C V C + 1 F t w t X + J k X + J k + 1 t V C V C + 1
532 rspa t V C V C + 1 F t w t V C V C + 1 F t w
533 458 531 532 syl2anc φ d π 0 k 0 ..^ N t V C V C + 1 F t w t X + J k X + J k + 1 F t w
534 533 ex φ d π 0 k 0 ..^ N t V C V C + 1 F t w t X + J k X + J k + 1 F t w
535 457 534 ralrimi φ d π 0 k 0 ..^ N t V C V C + 1 F t w t X + J k X + J k + 1 F t w
536 535 ex φ d π 0 k 0 ..^ N t V C V C + 1 F t w t X + J k X + J k + 1 F t w
537 536 reximdv φ d π 0 k 0 ..^ N w t V C V C + 1 F t w w t X + J k X + J k + 1 F t w
538 454 537 mpd φ d π 0 k 0 ..^ N w t X + J k X + J k + 1 F t w
539 448 raleqdv i = C t V i V i + 1 F t z t V C V C + 1 F t z
540 539 rexbidv i = C z t V i V i + 1 F t z z t V C V C + 1 F t z
541 444 540 imbi12d i = C φ i 0 ..^ M z t V i V i + 1 F t z φ C 0 ..^ M z t V C V C + 1 F t z
542 541 10 vtoclg C 0 ..^ M φ C 0 ..^ M z t V C V C + 1 F t z
543 440 442 542 sylc φ d π 0 k 0 ..^ N z t V C V C + 1 F t z
544 nfra1 t t V C V C + 1 F t z
545 455 544 nfan t φ d π 0 k 0 ..^ N t V C V C + 1 F t z
546 1 68 fssd φ F :
547 ssid
548 547 a1i φ
549 ioossre X + J k X + J k + 1
550 549 a1i φ X + J k X + J k + 1
551 50 405 dvres F : X + J k X + J k + 1 D F X + J k X + J k + 1 = F int topGen ran . X + J k X + J k + 1
552 68 546 548 550 551 syl22anc φ D F X + J k X + J k + 1 = F int topGen ran . X + J k X + J k + 1
553 ioontr int topGen ran . X + J k X + J k + 1 = X + J k X + J k + 1
554 553 reseq2i F int topGen ran . X + J k X + J k + 1 = F X + J k X + J k + 1
555 554 a1i φ F int topGen ran . X + J k X + J k + 1 = F X + J k X + J k + 1
556 552 555 eqtrd φ D F X + J k X + J k + 1 = F X + J k X + J k + 1
557 556 fveq1d φ F X + J k X + J k + 1 t = F X + J k X + J k + 1 t
558 fvres t X + J k X + J k + 1 F X + J k X + J k + 1 t = F t
559 557 558 sylan9eq φ t X + J k X + J k + 1 F X + J k X + J k + 1 t = F t
560 559 ad4ant14 φ d π 0 k 0 ..^ N t X + J k X + J k + 1 F X + J k X + J k + 1 t = F t
561 560 fveq2d φ d π 0 k 0 ..^ N t X + J k X + J k + 1 F X + J k X + J k + 1 t = F t
562 561 adantlr φ d π 0 k 0 ..^ N t V C V C + 1 F t z t X + J k X + J k + 1 F X + J k X + J k + 1 t = F t
563 simplr φ d π 0 k 0 ..^ N t V C V C + 1 F t z t X + J k X + J k + 1 t V C V C + 1 F t z
564 530 adantlr φ d π 0 k 0 ..^ N t V C V C + 1 F t z t X + J k X + J k + 1 t V C V C + 1
565 rspa t V C V C + 1 F t z t V C V C + 1 F t z
566 563 564 565 syl2anc φ d π 0 k 0 ..^ N t V C V C + 1 F t z t X + J k X + J k + 1 F t z
567 562 566 eqbrtrd φ d π 0 k 0 ..^ N t V C V C + 1 F t z t X + J k X + J k + 1 F X + J k X + J k + 1 t z
568 567 ex φ d π 0 k 0 ..^ N t V C V C + 1 F t z t X + J k X + J k + 1 F X + J k X + J k + 1 t z
569 545 568 ralrimi φ d π 0 k 0 ..^ N t V C V C + 1 F t z t X + J k X + J k + 1 F X + J k X + J k + 1 t z
570 569 ex φ d π 0 k 0 ..^ N t V C V C + 1 F t z t X + J k X + J k + 1 F X + J k X + J k + 1 t z
571 570 reximdv φ d π 0 k 0 ..^ N z t V C V C + 1 F t z z t X + J k X + J k + 1 F X + J k X + J k + 1 t z
572 543 571 mpd φ d π 0 k 0 ..^ N z t X + J k X + J k + 1 F X + J k X + J k + 1 t z
573 426 rexrd φ d π 0 k 0 ..^ N π *
574 573 328 322 428 fourierdlem8 φ d π 0 k 0 ..^ N J k J k + 1 π d
575 145 ad2antrr φ d π 0 r π d ¬ r ran J N
576 170 320 fssd φ d π 0 J : 0 N
577 576 ad2antrr φ d π 0 r π d ¬ r ran J J : 0 N
578 simpr φ d π 0 r π d r π d
579 171 eqcomd φ d π 0 π = J 0
580 172 eqcomd φ d π 0 d = J N
581 579 580 oveq12d φ d π 0 π d = J 0 J N
582 581 adantr φ d π 0 r π d π d = J 0 J N
583 578 582 eleqtrd φ d π 0 r π d r J 0 J N
584 583 adantr φ d π 0 r π d ¬ r ran J r J 0 J N
585 simpr φ d π 0 r π d ¬ r ran J ¬ r ran J
586 fveq2 j = k J j = J k
587 586 breq1d j = k J j < r J k < r
588 587 cbvrabv j 0 ..^ N | J j < r = k 0 ..^ N | J k < r
589 588 supeq1i sup j 0 ..^ N | J j < r < = sup k 0 ..^ N | J k < r <
590 575 577 584 585 589 fourierdlem25 φ d π 0 r π d ¬ r ran J m 0 ..^ N r J m J m + 1
591 554 a1i φ d π 0 k 0 ..^ N F int topGen ran . X + J k X + J k + 1 = F X + J k X + J k + 1
592 546 ad2antrr φ d π 0 k 0 ..^ N F :
593 547 a1i φ d π 0 k 0 ..^ N
594 549 a1i φ d π 0 k 0 ..^ N X + J k X + J k + 1
595 403 592 593 594 551 syl22anc φ d π 0 k 0 ..^ N D F X + J k X + J k + 1 = F int topGen ran . X + J k X + J k + 1
596 530 ralrimiva φ d π 0 k 0 ..^ N t X + J k X + J k + 1 t V C V C + 1
597 dfss3 X + J k X + J k + 1 V C V C + 1 t X + J k X + J k + 1 t V C V C + 1
598 596 597 sylibr φ d π 0 k 0 ..^ N X + J k X + J k + 1 V C V C + 1
599 598 resabs1d φ d π 0 k 0 ..^ N F V C V C + 1 X + J k X + J k + 1 = F X + J k X + J k + 1
600 591 595 599 3eqtr4rd φ d π 0 k 0 ..^ N F V C V C + 1 X + J k X + J k + 1 = D F X + J k X + J k + 1
601 simpr φ C 0 ..^ M C 0 ..^ M
602 id φ C 0 ..^ M φ C 0 ..^ M
603 448 reseq2d i = C F V i V i + 1 = F V C V C + 1
604 603 448 feq12d i = C F V i V i + 1 : V i V i + 1 F V C V C + 1 : V C V C + 1
605 444 604 imbi12d i = C φ i 0 ..^ M F V i V i + 1 : V i V i + 1 φ C 0 ..^ M F V C V C + 1 : V C V C + 1
606 cncff F V i V i + 1 : V i V i + 1 cn F V i V i + 1 : V i V i + 1
607 9 606 syl φ i 0 ..^ M F V i V i + 1 : V i V i + 1
608 605 607 vtoclg C 0 ..^ M φ C 0 ..^ M F V C V C + 1 : V C V C + 1
609 601 602 608 sylc φ C 0 ..^ M F V C V C + 1 : V C V C + 1
610 442 609 syl φ d π 0 k 0 ..^ N F V C V C + 1 : V C V C + 1
611 610 598 fssresd φ d π 0 k 0 ..^ N F V C V C + 1 X + J k X + J k + 1 : X + J k X + J k + 1
612 600 611 feq1dd φ d π 0 k 0 ..^ N F X + J k X + J k + 1 : X + J k X + J k + 1
613 379 390 oveq12d t = s F X + t W 2 sin t 2 = F X + s W 2 sin s 2
614 613 cbvmptv t J k J k + 1 F X + t W 2 sin t 2 = s J k J k + 1 F X + s W 2 sin s 2
615 biid φ d π 0 k 0 ..^ N w z φ d π 0 k 0 ..^ N w z
616 fveq2 r = t F r = F t
617 616 fveq2d r = t F r = F t
618 617 breq1d r = t F r w F t w
619 618 cbvralvw r X + J k X + J k + 1 F r w t X + J k X + J k + 1 F t w
620 615 619 anbi12i φ d π 0 k 0 ..^ N w z r X + J k X + J k + 1 F r w φ d π 0 k 0 ..^ N w z t X + J k X + J k + 1 F t w
621 fveq2 r = t F X + J k X + J k + 1 r = F X + J k X + J k + 1 t
622 621 fveq2d r = t F X + J k X + J k + 1 r = F X + J k X + J k + 1 t
623 622 breq1d r = t F X + J k X + J k + 1 r z F X + J k X + J k + 1 t z
624 623 cbvralvw r X + J k X + J k + 1 F X + J k X + J k + 1 r z t X + J k X + J k + 1 F X + J k X + J k + 1 t z
625 620 624 anbi12i φ d π 0 k 0 ..^ N w z r X + J k X + J k + 1 F r w r X + J k X + J k + 1 F X + J k X + J k + 1 r z φ d π 0 k 0 ..^ N w z t X + J k X + J k + 1 F t w t X + J k X + J k + 1 F X + J k X + J k + 1 t z
626 280 281 42 44 85 291 292 438 439 538 572 170 194 574 590 612 614 625 fourierdlem80 φ d π 0 b s dom ds π d F X + s W 2 sin s 2 d s ds π d F X + s W 2 sin s 2 d s s b
627 370 mpteq2dva φ d π 0 s π d F X + s W s s 2 sin s 2 = s π d F X + s W 2 sin s 2
628 277 627 eqtrd φ d π 0 O = s π d F X + s W 2 sin s 2
629 628 oveq2d φ d π 0 D O = ds π d F X + s W 2 sin s 2 d s
630 629 dmeqd φ d π 0 dom O = dom ds π d F X + s W 2 sin s 2 d s
631 nfcv _ s dom O
632 nfcv _ s
633 nfcv _ s D
634 nfmpt1 _ s s π d F X + s W 2 sin s 2
635 632 633 634 nfov _ s ds π d F X + s W 2 sin s 2 d s
636 635 nfdm _ s dom ds π d F X + s W 2 sin s 2 d s
637 631 636 raleqf dom O = dom ds π d F X + s W 2 sin s 2 d s s dom O O s b s dom ds π d F X + s W 2 sin s 2 d s O s b
638 630 637 syl φ d π 0 s dom O O s b s dom ds π d F X + s W 2 sin s 2 d s O s b
639 629 fveq1d φ d π 0 O s = ds π d F X + s W 2 sin s 2 d s s
640 639 fveq2d φ d π 0 O s = ds π d F X + s W 2 sin s 2 d s s
641 640 breq1d φ d π 0 O s b ds π d F X + s W 2 sin s 2 d s s b
642 641 ralbidv φ d π 0 s dom ds π d F X + s W 2 sin s 2 d s O s b s dom ds π d F X + s W 2 sin s 2 d s ds π d F X + s W 2 sin s 2 d s s b
643 638 642 bitrd φ d π 0 s dom O O s b s dom ds π d F X + s W 2 sin s 2 d s ds π d F X + s W 2 sin s 2 d s s b
644 643 rexbidv φ d π 0 b s dom O O s b b s dom ds π d F X + s W 2 sin s 2 d s ds π d F X + s W 2 sin s 2 d s s b
645 626 644 mpbird φ d π 0 b s dom O O s b
646 eqid l + π d O s sin l s ds = l + π d O s sin l s ds
647 eqeq1 t = s t = J k s = J k
648 fveq2 h = l Q h = Q l
649 oveq1 h = l h + 1 = l + 1
650 649 fveq2d h = l Q h + 1 = Q l + 1
651 648 650 oveq12d h = l Q h Q h + 1 = Q l Q l + 1
652 651 sseq2d h = l J k J k + 1 Q h Q h + 1 J k J k + 1 Q l Q l + 1
653 652 cbvriotavw ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1
654 653 fveq2i Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1
655 654 eqeq2i J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1
656 655 a1i J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1
657 csbeq1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R
658 653 657 ax-mp ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R
659 658 a1i ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R
660 656 659 ifbieq1d if J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R F X + J k = if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k
661 660 mptru if J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R F X + J k = if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k
662 661 oveq1i if J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R F X + J k W = if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W
663 662 oveq1i if J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R F X + J k W J k = if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k
664 663 oveq1i if J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R F X + J k W J k J k 2 sin J k 2 = if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2
665 664 a1i t = s if J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R F X + J k W J k J k 2 sin J k 2 = if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2
666 eqeq1 t = s t = J k + 1 s = J k + 1
667 653 oveq1i ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1
668 667 fveq2i Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1
669 668 eqeq2i J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1
670 669 a1i J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1
671 csbeq1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L
672 653 671 ax-mp ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L
673 672 a1i ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L = ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L
674 670 673 ifbieq1d if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 = if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1
675 674 mptru if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 = if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1
676 675 oveq1i if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 W = if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W
677 676 oveq1i if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 W J k + 1 = if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1
678 677 oveq1i if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 = if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2
679 678 a1i t = s if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 = if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2
680 fveq2 t = s O t = O s
681 666 679 680 ifbieq12d t = s if t = J k + 1 if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 O t = if s = J k + 1 if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 O s
682 647 665 681 ifbieq12d t = s if t = J k if J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R F X + J k W J k J k 2 sin J k 2 if t = J k + 1 if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 O t = if s = J k if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2 if s = J k + 1 if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 O s
683 682 cbvmptv t J k J k + 1 if t = J k if J k = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i R F X + J k W J k J k 2 sin J k 2 if t = J k + 1 if J k + 1 = Q ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 + 1 ι h 0 ..^ M | J k J k + 1 Q h Q h + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 O t = s J k J k + 1 if s = J k if J k = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i R F X + J k W J k J k 2 sin J k 2 if s = J k + 1 if J k + 1 = Q ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 + 1 ι l 0 ..^ M | J k J k + 1 Q l Q l + 1 / i L F X + J k + 1 W J k + 1 J k + 1 2 sin J k + 1 2 O s
684 42 44 89 145 170 171 172 194 304 310 313 314 437 645 646 683 fourierdlem73 φ d π 0 e + j l j +∞ π d O s sin l s ds < e
685 breq2 e = a π d O s sin l s ds < e π d O s sin l s ds < a
686 685 rexralbidv e = a j l j +∞ π d O s sin l s ds < e j l j +∞ π d O s sin l s ds < a
687 686 cbvralvw e + j l j +∞ π d O s sin l s ds < e a + j l j +∞ π d O s sin l s ds < a
688 684 687 sylib φ d π 0 a + j l j +∞ π d O s sin l s ds < a
689 688 adantlr φ e + d π 0 a + j l j +∞ π d O s sin l s ds < a
690 rphalfcl e + e 2 +
691 690 ad2antlr φ e + d π 0 e 2 +
692 breq2 a = e 2 π d O s sin l s ds < a π d O s sin l s ds < e 2
693 692 rexralbidv a = e 2 j l j +∞ π d O s sin l s ds < a j l j +∞ π d O s sin l s ds < e 2
694 693 rspccva a + j l j +∞ π d O s sin l s ds < a e 2 + j l j +∞ π d O s sin l s ds < e 2
695 689 691 694 syl2anc φ e + d π 0 j l j +∞ π d O s sin l s ds < e 2
696 357 a1i φ d π 0 s π d O s = U π d s
697 158 a1i φ d π 0 π d π d
698 697 sselda φ d π 0 s π d s π d
699 698 359 syl φ d π 0 s π d U π d s = U s
700 696 699 eqtr2d φ d π 0 s π d U s = O s
701 700 oveq1d φ d π 0 s π d U s sin l s = O s sin l s
702 701 itgeq2dv φ d π 0 π d U s sin l s ds = π d O s sin l s ds
703 702 adantr φ d π 0 π d O s sin l s ds < e 2 π d U s sin l s ds = π d O s sin l s ds
704 703 fveq2d φ d π 0 π d O s sin l s ds < e 2 π d U s sin l s ds = π d O s sin l s ds
705 simpr φ d π 0 π d O s sin l s ds < e 2 π d O s sin l s ds < e 2
706 704 705 eqbrtrd φ d π 0 π d O s sin l s ds < e 2 π d U s sin l s ds < e 2
707 706 ex φ d π 0 π d O s sin l s ds < e 2 π d U s sin l s ds < e 2
708 707 adantlr φ e + d π 0 π d O s sin l s ds < e 2 π d U s sin l s ds < e 2
709 708 ralimdv φ e + d π 0 l j +∞ π d O s sin l s ds < e 2 l j +∞ π d U s sin l s ds < e 2
710 709 reximdv φ e + d π 0 j l j +∞ π d O s sin l s ds < e 2 j l j +∞ π d U s sin l s ds < e 2
711 695 710 mpd φ e + d π 0 j l j +∞ π d U s sin l s ds < e 2
712 711 adantr φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2
713 nfv k φ e + d π 0
714 nfra1 k k d 0 U s sin k + 1 2 s ds < e 2
715 713 714 nfan k φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2
716 nfv k j
717 715 716 nfan k φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j
718 nfv k l j +∞ π d U s sin l s ds < e 2
719 717 718 nfan k φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2
720 simpll φ e + d π 0 j k j φ e + d π 0
721 eluznn j k j k
722 721 adantll φ e + d π 0 j k j k
723 720 722 jca φ e + d π 0 j k j φ e + d π 0 k
724 723 adantllr φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j k j φ e + d π 0 k
725 simpllr φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j k j k d 0 U s sin k + 1 2 s ds < e 2
726 721 adantll φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j k j k
727 rspa k d 0 U s sin k + 1 2 s ds < e 2 k d 0 U s sin k + 1 2 s ds < e 2
728 725 726 727 syl2anc φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j k j d 0 U s sin k + 1 2 s ds < e 2
729 724 728 jca φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j k j φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2
730 729 adantlr φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 k j φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2
731 nnre j j
732 731 rexrd j j *
733 732 adantr j k j j *
734 51 a1i j k j +∞ *
735 eluzelre k j k
736 1re 1
737 736 rehalfcli 1 2
738 737 a1i k j 1 2
739 735 738 readdcld k j k + 1 2
740 739 adantl j k j k + 1 2
741 731 adantr j k j j
742 735 adantl j k j k
743 eluzle k j j k
744 743 adantl j k j j k
745 halfgt0 0 < 1 2
746 745 a1i j k j 0 < 1 2
747 737 a1i j k j 1 2
748 747 742 ltaddposd j k j 0 < 1 2 k < k + 1 2
749 746 748 mpbid j k j k < k + 1 2
750 741 742 740 744 749 lelttrd j k j j < k + 1 2
751 740 ltpnfd j k j k + 1 2 < +∞
752 733 734 740 750 751 eliood j k j k + 1 2 j +∞
753 752 adantlr j l j +∞ π d U s sin l s ds < e 2 k j k + 1 2 j +∞
754 simplr j l j +∞ π d U s sin l s ds < e 2 k j l j +∞ π d U s sin l s ds < e 2
755 oveq1 l = k + 1 2 l s = k + 1 2 s
756 755 fveq2d l = k + 1 2 sin l s = sin k + 1 2 s
757 756 oveq2d l = k + 1 2 U s sin l s = U s sin k + 1 2 s
758 757 adantr l = k + 1 2 s π d U s sin l s = U s sin k + 1 2 s
759 758 itgeq2dv l = k + 1 2 π d U s sin l s ds = π d U s sin k + 1 2 s ds
760 759 fveq2d l = k + 1 2 π d U s sin l s ds = π d U s sin k + 1 2 s ds
761 760 breq1d l = k + 1 2 π d U s sin l s ds < e 2 π d U s sin k + 1 2 s ds < e 2
762 761 rspcv k + 1 2 j +∞ l j +∞ π d U s sin l s ds < e 2 π d U s sin k + 1 2 s ds < e 2
763 753 754 762 sylc j l j +∞ π d U s sin l s ds < e 2 k j π d U s sin k + 1 2 s ds < e 2
764 763 adantlll φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 k j π d U s sin k + 1 2 s ds < e 2
765 730 764 jca φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 k j φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2
766 765 31 sylibr φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 k j χ
767 41 a1i χ π
768 0red χ 0
769 ioossicc π 0 π 0
770 31 biimpi χ φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2
771 simp-4r φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2 d π 0
772 770 771 syl χ d π 0
773 769 772 sseldi χ d π 0
774 simp-5l φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2 φ
775 770 774 syl χ φ
776 66 adantr φ s π 0 U : π π
777 40 rexri π *
778 0re 0
779 778 40 79 ltleii 0 π
780 iooss2 π * 0 π π 0 π π
781 777 779 780 mp2an π 0 π π
782 ioossicc π π π π
783 781 782 sstri π 0 π π
784 783 sseli s π 0 s π π
785 784 adantl φ s π 0 s π π
786 776 785 ffvelrnd φ s π 0 U s
787 775 786 sylan χ s π 0 U s
788 simpllr φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2 k
789 770 788 syl χ k
790 789 nnred χ k
791 737 a1i χ 1 2
792 790 791 readdcld χ k + 1 2
793 792 adantr χ s π 0 k + 1 2
794 elioore s π 0 s
795 794 adantl χ s π 0 s
796 793 795 remulcld χ s π 0 k + 1 2 s
797 796 resincld χ s π 0 sin k + 1 2 s
798 787 797 remulcld χ s π 0 U s sin k + 1 2 s
799 798 recnd χ s π 0 U s sin k + 1 2 s
800 75 a1i χ π *
801 76 a1i χ 0 *
802 767 leidd χ π π
803 ioossre π 0
804 803 772 sseldi χ d
805 800 801 772 77 syl3anc χ d < 0
806 804 768 805 ltled χ d 0
807 ioossioo π * 0 * π π d 0 π d π 0
808 800 801 802 806 807 syl22anc χ π d π 0
809 ioombl π d dom vol
810 809 a1i χ π d dom vol
811 eleq1 n = k n k
812 811 anbi2d n = k φ n φ k
813 simpl n = k s π 0 n = k
814 813 oveq1d n = k s π 0 n + 1 2 = k + 1 2
815 814 oveq1d n = k s π 0 n + 1 2 s = k + 1 2 s
816 815 fveq2d n = k s π 0 sin n + 1 2 s = sin k + 1 2 s
817 816 oveq2d n = k s π 0 U s sin n + 1 2 s = U s sin k + 1 2 s
818 817 mpteq2dva n = k s π 0 U s sin n + 1 2 s = s π 0 U s sin k + 1 2 s
819 818 eleq1d n = k s π 0 U s sin n + 1 2 s 𝐿 1 s π 0 U s sin k + 1 2 s 𝐿 1
820 812 819 imbi12d n = k φ n s π 0 U s sin n + 1 2 s 𝐿 1 φ k s π 0 U s sin k + 1 2 s 𝐿 1
821 783 a1i φ n π 0 π π
822 ioombl π 0 dom vol
823 822 a1i φ n π 0 dom vol
824 66 ffvelrnda φ s π π U s
825 824 adantlr φ n s π π U s
826 nnre n n
827 readdcl n 1 2 n + 1 2
828 826 737 827 sylancl n n + 1 2
829 828 adantr n s π π n + 1 2
830 simpr n s π π s π π
831 232 830 sseldi n s π π s
832 829 831 remulcld n s π π n + 1 2 s
833 832 resincld n s π π sin n + 1 2 s
834 833 adantll φ n s π π sin n + 1 2 s
835 825 834 remulcld φ n s π π U s sin n + 1 2 s
836 17 a1i φ n G = s π π U s S s
837 16 fvmpt2 s π π sin n + 1 2 s S s = sin n + 1 2 s
838 830 833 837 syl2anc n s π π S s = sin n + 1 2 s
839 838 adantll φ n s π π S s = sin n + 1 2 s
840 839 oveq2d φ n s π π U s S s = U s sin n + 1 2 s
841 840 mpteq2dva φ n s π π U s S s = s π π U s sin n + 1 2 s
842 836 841 eqtr2d φ n s π π U s sin n + 1 2 s = G
843 1 adantr φ n F :
844 6 adantr φ n X ran V
845 20 adantr φ n Y F X +∞ lim X
846 21 adantr φ n W F −∞ X lim X
847 826 adantl φ n n
848 4 adantr φ n M
849 5 adantr φ n V P M
850 7 adantlr φ n i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
851 11 adantlr φ n i 0 ..^ M R F V i V i + 1 lim V i
852 12 adantlr φ n i 0 ..^ M L F V i V i + 1 lim V i + 1
853 eqid m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1 = m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1
854 eqid D F = D F
855 607 adantlr φ n i 0 ..^ M F V i V i + 1 : V i V i + 1
856 22 adantr φ n A F −∞ X lim X
857 23 adantr φ n B F X +∞ lim X
858 3 843 844 845 846 13 14 15 847 16 17 848 849 850 851 852 29 853 854 855 856 857 fourierdlem88 φ n G 𝐿 1
859 842 858 eqeltrd φ n s π π U s sin n + 1 2 s 𝐿 1
860 821 823 835 859 iblss φ n s π 0 U s sin n + 1 2 s 𝐿 1
861 820 860 chvarvv φ k s π 0 U s sin k + 1 2 s 𝐿 1
862 775 789 861 syl2anc χ s π 0 U s sin k + 1 2 s 𝐿 1
863 808 810 798 862 iblss χ s π d U s sin k + 1 2 s 𝐿 1
864 772 125 syl χ π < d
865 767 804 864 ltled χ π d
866 768 leidd χ 0 0
867 ioossioo π * 0 * π d 0 0 d 0 π 0
868 800 801 865 866 867 syl22anc χ d 0 π 0
869 ioombl d 0 dom vol
870 869 a1i χ d 0 dom vol
871 868 870 798 862 iblss χ s d 0 U s sin k + 1 2 s 𝐿 1
872 767 768 773 799 863 871 itgsplitioo χ π 0 U s sin k + 1 2 s ds = π d U s sin k + 1 2 s ds + d 0 U s sin k + 1 2 s ds
873 808 sselda χ s π d s π 0
874 873 798 syldan χ s π d U s sin k + 1 2 s
875 874 863 itgcl χ π d U s sin k + 1 2 s ds
876 868 sselda χ s d 0 s π 0
877 876 798 syldan χ s d 0 U s sin k + 1 2 s
878 877 871 itgcl χ d 0 U s sin k + 1 2 s ds
879 875 878 addcomd χ π d U s sin k + 1 2 s ds + d 0 U s sin k + 1 2 s ds = d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds
880 872 879 eqtrd χ π 0 U s sin k + 1 2 s ds = d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds
881 880 fveq2d χ π 0 U s sin k + 1 2 s ds = d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds
882 878 875 addcld χ d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds
883 882 abscld χ d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds
884 878 abscld χ d 0 U s sin k + 1 2 s ds
885 875 abscld χ π d U s sin k + 1 2 s ds
886 884 885 readdcld χ d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds
887 simp-5r φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2 e +
888 770 887 syl χ e +
889 888 rpred χ e
890 878 875 abstrid χ d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds
891 simplr φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 π d U s sin k + 1 2 s ds < e 2 d 0 U s sin k + 1 2 s ds < e 2
892 770 891 syl χ d 0 U s sin k + 1 2 s ds < e 2
893 770 simprd χ π d U s sin k + 1 2 s ds < e 2
894 884 885 889 892 893 lt2halvesd χ d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds < e
895 883 886 889 890 894 lelttrd χ d 0 U s sin k + 1 2 s ds + π d U s sin k + 1 2 s ds < e
896 881 895 eqbrtrd χ π 0 U s sin k + 1 2 s ds < e
897 766 896 syl φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 k j π 0 U s sin k + 1 2 s ds < e
898 897 ex φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 k j π 0 U s sin k + 1 2 s ds < e
899 719 898 ralrimi φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 k j π 0 U s sin k + 1 2 s ds < e
900 899 ex φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 k j π 0 U s sin k + 1 2 s ds < e
901 900 reximdva φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j l j +∞ π d U s sin l s ds < e 2 j k j π 0 U s sin k + 1 2 s ds < e
902 712 901 mpd φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2 j k j π 0 U s sin k + 1 2 s ds < e
903 negpilt0 π < 0
904 41 778 40 lttri π < 0 0 < π π < π
905 903 79 904 mp2an π < π
906 41 40 905 ltleii π π
907 906 a1i φ π π
908 3 fourierdlem2 M V P M V 0 M V 0 = - π + X V M = π + X i 0 ..^ M V i < V i + 1
909 4 908 syl φ V P M V 0 M V 0 = - π + X V M = π + X i 0 ..^ M V i < V i + 1
910 5 909 mpbid φ V 0 M V 0 = - π + X V M = π + X i 0 ..^ M V i < V i + 1
911 910 simpld φ V 0 M
912 elmapi V 0 M V : 0 M
913 911 912 syl φ V : 0 M
914 913 ffvelrnda φ i 0 M V i
915 2 adantr φ i 0 M X
916 914 915 resubcld φ i 0 M V i X
917 916 29 fmptd φ Q : 0 M
918 29 a1i φ Q = i 0 M V i X
919 fveq2 i = 0 V i = V 0
920 919 oveq1d i = 0 V i X = V 0 X
921 920 adantl φ i = 0 V i X = V 0 X
922 4 nnnn0d φ M 0
923 nn0uz 0 = 0
924 922 923 eleqtrdi φ M 0
925 eluzfz1 M 0 0 0 M
926 924 925 syl φ 0 0 M
927 913 926 ffvelrnd φ V 0
928 927 2 resubcld φ V 0 X
929 918 921 926 928 fvmptd φ Q 0 = V 0 X
930 910 simprd φ V 0 = - π + X V M = π + X i 0 ..^ M V i < V i + 1
931 930 simpld φ V 0 = - π + X V M = π + X
932 931 simpld φ V 0 = - π + X
933 932 oveq1d φ V 0 X = π + X - X
934 459 recnd φ π
935 2 recnd φ X
936 934 935 pncand φ π + X - X = π
937 929 933 936 3eqtrd φ Q 0 = π
938 459 461 2 3 853 4 5 29 fourierdlem14 φ Q m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1 M
939 853 fourierdlem2 M Q m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1 M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
940 4 939 syl φ Q m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1 M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
941 938 940 mpbid φ Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
942 941 simprd φ Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
943 942 simpld φ Q 0 = π Q M = π
944 943 simprd φ Q M = π
945 942 simprd φ i 0 ..^ M Q i < Q i + 1
946 945 r19.21bi φ i 0 ..^ M Q i < Q i + 1
947 1 adantr φ i 0 ..^ M F :
948 853 4 938 fourierdlem15 φ Q : 0 M π π
949 948 adantr φ i 0 ..^ M Q : 0 M π π
950 elfzofz i 0 ..^ M i 0 M
951 950 adantl φ i 0 ..^ M i 0 M
952 949 951 ffvelrnd φ i 0 ..^ M Q i π π
953 fzofzp1 i 0 ..^ M i + 1 0 M
954 953 adantl φ i 0 ..^ M i + 1 0 M
955 949 954 ffvelrnd φ i 0 ..^ M Q i + 1 π π
956 2 adantr φ i 0 ..^ M X
957 ffn V : 0 M V Fn 0 M
958 911 912 957 3syl φ V Fn 0 M
959 fvelrnb V Fn 0 M X ran V i 0 M V i = X
960 958 959 syl φ X ran V i 0 M V i = X
961 6 960 mpbid φ i 0 M V i = X
962 oveq1 V i = X V i X = X X
963 962 adantl φ i 0 M V i = X V i X = X X
964 935 subidd φ X X = 0
965 964 ad2antrr φ i 0 M V i = X X X = 0
966 963 965 eqtr2d φ i 0 M V i = X 0 = V i X
967 966 ex φ i 0 M V i = X 0 = V i X
968 967 reximdva φ i 0 M V i = X i 0 M 0 = V i X
969 961 968 mpd φ i 0 M 0 = V i X
970 29 elrnmpt 0 0 ran Q i 0 M 0 = V i X
971 778 970 ax-mp 0 ran Q i 0 M 0 = V i X
972 969 971 sylibr φ 0 ran Q
973 853 4 938 972 fourierdlem12 φ i 0 ..^ M ¬ 0 Q i Q i + 1
974 913 adantr φ i 0 ..^ M V : 0 M
975 974 951 ffvelrnd φ i 0 ..^ M V i
976 975 956 resubcld φ i 0 ..^ M V i X
977 29 fvmpt2 i 0 M V i X Q i = V i X
978 951 976 977 syl2anc φ i 0 ..^ M Q i = V i X
979 978 oveq1d φ i 0 ..^ M Q i + X = V i - X + X
980 975 recnd φ i 0 ..^ M V i
981 935 adantr φ i 0 ..^ M X
982 980 981 npcand φ i 0 ..^ M V i - X + X = V i
983 979 982 eqtrd φ i 0 ..^ M Q i + X = V i
984 fveq2 j = i V j = V i
985 984 oveq1d j = i V j X = V i X
986 985 cbvmptv j 0 M V j X = i 0 M V i X
987 29 986 eqtr4i Q = j 0 M V j X
988 987 a1i φ i 0 ..^ M Q = j 0 M V j X
989 fveq2 j = i + 1 V j = V i + 1
990 989 oveq1d j = i + 1 V j X = V i + 1 X
991 990 adantl φ i 0 ..^ M j = i + 1 V j X = V i + 1 X
992 974 954 ffvelrnd φ i 0 ..^ M V i + 1
993 992 956 resubcld φ i 0 ..^ M V i + 1 X
994 988 991 954 993 fvmptd φ i 0 ..^ M Q i + 1 = V i + 1 X
995 994 oveq1d φ i 0 ..^ M Q i + 1 + X = V i + 1 - X + X
996 992 recnd φ i 0 ..^ M V i + 1
997 996 981 npcand φ i 0 ..^ M V i + 1 - X + X = V i + 1
998 995 997 eqtrd φ i 0 ..^ M Q i + 1 + X = V i + 1
999 983 998 oveq12d φ i 0 ..^ M Q i + X Q i + 1 + X = V i V i + 1
1000 999 reseq2d φ i 0 ..^ M F Q i + X Q i + 1 + X = F V i V i + 1
1001 999 oveq1d φ i 0 ..^ M Q i + X Q i + 1 + X cn = V i V i + 1 cn
1002 7 1000 1001 3eltr4d φ i 0 ..^ M F Q i + X Q i + 1 + X : Q i + X Q i + 1 + X cn
1003 55 adantr φ i 0 ..^ M Y
1004 65 adantr φ i 0 ..^ M W
1005 947 952 955 956 973 1002 1003 1004 13 fourierdlem40 φ i 0 ..^ M H Q i Q i + 1 : Q i Q i + 1 cn
1006 id F V i V i + 1 : V i V i + 1 F V i V i + 1 : V i V i + 1
1007 67 a1i F V i V i + 1 : V i V i + 1
1008 1006 1007 fssd F V i V i + 1 : V i V i + 1 F V i V i + 1 : V i V i + 1
1009 9 606 1008 3syl φ i 0 ..^ M F V i V i + 1 : V i V i + 1
1010 eqid if V i = X B R if V i < X W Y Q i = if V i = X B R if V i < X W Y Q i
1011 2 3 1 6 20 65 13 4 5 11 29 853 854 1009 23 1010 fourierdlem75 φ i 0 ..^ M if V i = X B R if V i < X W Y Q i H Q i Q i + 1 lim Q i
1012 eqid if V i + 1 = X A L if V i + 1 < X W Y Q i + 1 = if V i + 1 = X A L if V i + 1 < X W Y Q i + 1
1013 2 3 1 6 55 21 13 4 5 12 29 853 854 607 22 1012 fourierdlem74 φ i 0 ..^ M if V i + 1 = X A L if V i + 1 < X W Y Q i + 1 H Q i Q i + 1 lim Q i + 1
1014 fveq2 j = i Q j = Q i
1015 oveq1 j = i j + 1 = i + 1
1016 1015 fveq2d j = i Q j + 1 = Q i + 1
1017 1014 1016 oveq12d j = i Q j Q j + 1 = Q i Q i + 1
1018 1017 cbvmptv j 0 ..^ M Q j Q j + 1 = i 0 ..^ M Q i Q i + 1
1019 459 461 907 198 4 917 937 944 946 1005 1011 1013 1018 fourierdlem70 φ x s π π H s x
1020 eqid e 3 y = e 3 y
1021 fveq2 t = s G t = G s
1022 1021 fveq2d t = s G t = G s
1023 1022 breq1d t = s G t y G s y
1024 1023 cbvralvw t π π G t y s π π G s y
1025 1024 ralbii n t π π G t y n s π π G s y
1026 1025 3anbi3i φ e + y + n t π π G t y φ e + y + n s π π G s y
1027 1026 anbi1i φ e + y + n t π π G t y u dom vol φ e + y + n s π π G s y u dom vol
1028 1027 anbi1i φ e + y + n t π π G t y u dom vol u π π vol u e 3 y φ e + y + n s π π G s y u dom vol u π π vol u e 3 y
1029 1028 anbi1i φ e + y + n t π π G t y u dom vol u π π vol u e 3 y n φ e + y + n s π π G s y u dom vol u π π vol u e 3 y n
1030 1 2 55 65 13 14 15 16 17 1019 858 1020 1029 fourierdlem87 φ e + c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2
1031 iftrue c π 2 if c π 2 c π 2 = c
1032 1031 negeqd c π 2 if c π 2 c π 2 = c
1033 1032 adantl c + c π 2 if c π 2 c π 2 = c
1034 75 a1i c + c π 2 π *
1035 76 a1i c + c π 2 0 *
1036 rpre c + c
1037 1036 renegcld c + c
1038 1037 adantr c + c π 2 c
1039 1036 adantr c + c π 2 c
1040 40 rehalfcli π 2
1041 1040 a1i c + c π 2 π 2
1042 40 a1i c + c π 2 π
1043 simpr c + c π 2 c π 2
1044 halfpos π 0 < π π 2 < π
1045 40 1044 ax-mp 0 < π π 2 < π
1046 79 1045 mpbi π 2 < π
1047 1046 a1i c + c π 2 π 2 < π
1048 1039 1041 1042 1043 1047 lelttrd c + c π 2 c < π
1049 1039 1042 ltnegd c + c π 2 c < π π < c
1050 1048 1049 mpbid c + c π 2 π < c
1051 rpgt0 c + 0 < c
1052 1036 lt0neg2d c + 0 < c c < 0
1053 1051 1052 mpbid c + c < 0
1054 1053 adantr c + c π 2 c < 0
1055 1034 1035 1038 1050 1054 eliood c + c π 2 c π 0
1056 1033 1055 eqeltrd c + c π 2 if c π 2 c π 2 π 0
1057 iffalse ¬ c π 2 if c π 2 c π 2 = π 2
1058 1057 negeqd ¬ c π 2 if c π 2 c π 2 = π 2
1059 1040 renegcli π 2
1060 1059 rexri π 2 *
1061 75 76 1060 3pm3.2i π * 0 * π 2 *
1062 1040 40 ltnegi π 2 < π π < π 2
1063 1046 1062 mpbi π < π 2
1064 2pos 0 < 2
1065 40 120 79 1064 divgt0ii 0 < π 2
1066 lt0neg2 π 2 0 < π 2 π 2 < 0
1067 1040 1066 ax-mp 0 < π 2 π 2 < 0
1068 1065 1067 mpbi π 2 < 0
1069 1063 1068 pm3.2i π < π 2 π 2 < 0
1070 elioo3g π 2 π 0 π * 0 * π 2 * π < π 2 π 2 < 0
1071 1061 1069 1070 mpbir2an π 2 π 0
1072 1071 a1i ¬ c π 2 π 2 π 0
1073 1058 1072 eqeltrd ¬ c π 2 if c π 2 c π 2 π 0
1074 1073 adantl c + ¬ c π 2 if c π 2 c π 2 π 0
1075 1056 1074 pm2.61dan c + if c π 2 c π 2 π 0
1076 1075 3ad2ant2 φ e + c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 if c π 2 c π 2 π 0
1077 ioombl if c π 2 c π 2 0 dom vol
1078 1077 a1i c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 if c π 2 c π 2 0 dom vol
1079 simpr c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2
1080 1078 1079 jca c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 if c π 2 c π 2 0 dom vol u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2
1081 ioossicc if c π 2 c π 2 0 if c π 2 c π 2 0
1082 1081 a1i c + if c π 2 c π 2 0 if c π 2 c π 2 0
1083 41 a1i c + π
1084 40 a1i c + π
1085 1039 1042 1048 ltled c + c π 2 c π
1086 1039 1042 lenegd c + c π 2 c π π c
1087 1085 1086 mpbid c + c π 2 π c
1088 1032 eqcomd c π 2 c = if c π 2 c π 2
1089 1088 adantl c + c π 2 c = if c π 2 c π 2
1090 1087 1089 breqtrd c + c π 2 π if c π 2 c π 2
1091 41 1059 1063 ltleii π π 2
1092 1091 a1i c + ¬ c π 2 π π 2
1093 1058 eqcomd ¬ c π 2 π 2 = if c π 2 c π 2
1094 1093 adantl c + ¬ c π 2 π 2 = if c π 2 c π 2
1095 1092 1094 breqtrd c + ¬ c π 2 π if c π 2 c π 2
1096 1090 1095 pm2.61dan c + π if c π 2 c π 2
1097 779 a1i c + 0 π
1098 iccss π π π if c π 2 c π 2 0 π if c π 2 c π 2 0 π π
1099 1083 1084 1096 1097 1098 syl22anc c + if c π 2 c π 2 0 π π
1100 1082 1099 sstrd c + if c π 2 c π 2 0 π π
1101 803 1075 sseldi c + if c π 2 c π 2
1102 0red c + 0
1103 rpge0 c + 0 c
1104 1103 adantr c + c π 2 0 c
1105 1043 iftrued c + c π 2 if c π 2 c π 2 = c
1106 1104 1105 breqtrrd c + c π 2 0 if c π 2 c π 2
1107 778 1040 1065 ltleii 0 π 2
1108 simpr c + ¬ c π 2 ¬ c π 2
1109 1108 iffalsed c + ¬ c π 2 if c π 2 c π 2 = π 2
1110 1107 1109 breqtrrid c + ¬ c π 2 0 if c π 2 c π 2
1111 1106 1110 pm2.61dan c + 0 if c π 2 c π 2
1112 1040 a1i c + π 2
1113 1036 1112 ifcld c + if c π 2 c π 2
1114 1113 le0neg2d c + 0 if c π 2 c π 2 if c π 2 c π 2 0
1115 1111 1114 mpbid c + if c π 2 c π 2 0
1116 volioo if c π 2 c π 2 0 if c π 2 c π 2 0 vol if c π 2 c π 2 0 = 0 if c π 2 c π 2
1117 1101 1102 1115 1116 syl3anc c + vol if c π 2 c π 2 0 = 0 if c π 2 c π 2
1118 0cn 0
1119 1118 a1i c + 0
1120 1113 recnd c + if c π 2 c π 2
1121 1119 1120 subnegd c + 0 if c π 2 c π 2 = 0 + if c π 2 c π 2
1122 1120 addid2d c + 0 + if c π 2 c π 2 = if c π 2 c π 2
1123 1117 1121 1122 3eqtrd c + vol if c π 2 c π 2 0 = if c π 2 c π 2
1124 min1 c π 2 if c π 2 c π 2 c
1125 1036 1040 1124 sylancl c + if c π 2 c π 2 c
1126 1123 1125 eqbrtrd c + vol if c π 2 c π 2 0 c
1127 1100 1126 jca c + if c π 2 c π 2 0 π π vol if c π 2 c π 2 0 c
1128 1127 adantr c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 if c π 2 c π 2 0 π π vol if c π 2 c π 2 0 c
1129 sseq1 u = if c π 2 c π 2 0 u π π if c π 2 c π 2 0 π π
1130 fveq2 u = if c π 2 c π 2 0 vol u = vol if c π 2 c π 2 0
1131 1130 breq1d u = if c π 2 c π 2 0 vol u c vol if c π 2 c π 2 0 c
1132 1129 1131 anbi12d u = if c π 2 c π 2 0 u π π vol u c if c π 2 c π 2 0 π π vol if c π 2 c π 2 0 c
1133 itgeq1 u = if c π 2 c π 2 0 u U s sin k + 1 2 s ds = if c π 2 c π 2 0 U s sin k + 1 2 s ds
1134 1133 fveq2d u = if c π 2 c π 2 0 u U s sin k + 1 2 s ds = if c π 2 c π 2 0 U s sin k + 1 2 s ds
1135 1134 breq1d u = if c π 2 c π 2 0 u U s sin k + 1 2 s ds < e 2 if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2
1136 1135 ralbidv u = if c π 2 c π 2 0 k u U s sin k + 1 2 s ds < e 2 k if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2
1137 1132 1136 imbi12d u = if c π 2 c π 2 0 u π π vol u c k u U s sin k + 1 2 s ds < e 2 if c π 2 c π 2 0 π π vol if c π 2 c π 2 0 c k if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2
1138 1137 rspcva if c π 2 c π 2 0 dom vol u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 if c π 2 c π 2 0 π π vol if c π 2 c π 2 0 c k if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2
1139 1080 1128 1138 sylc c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 k if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2
1140 1139 3adant1 φ e + c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 k if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2
1141 oveq1 d = if c π 2 c π 2 d 0 = if c π 2 c π 2 0
1142 1141 itgeq1d d = if c π 2 c π 2 d 0 U s sin k + 1 2 s ds = if c π 2 c π 2 0 U s sin k + 1 2 s ds
1143 1142 fveq2d d = if c π 2 c π 2 d 0 U s sin k + 1 2 s ds = if c π 2 c π 2 0 U s sin k + 1 2 s ds
1144 1143 breq1d d = if c π 2 c π 2 d 0 U s sin k + 1 2 s ds < e 2 if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2
1145 1144 ralbidv d = if c π 2 c π 2 k d 0 U s sin k + 1 2 s ds < e 2 k if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2
1146 1145 rspcev if c π 2 c π 2 π 0 k if c π 2 c π 2 0 U s sin k + 1 2 s ds < e 2 d π 0 k d 0 U s sin k + 1 2 s ds < e 2
1147 1076 1140 1146 syl2anc φ e + c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 d π 0 k d 0 U s sin k + 1 2 s ds < e 2
1148 1147 rexlimdv3a φ e + c + u dom vol u π π vol u c k u U s sin k + 1 2 s ds < e 2 d π 0 k d 0 U s sin k + 1 2 s ds < e 2
1149 1030 1148 mpd φ e + d π 0 k d 0 U s sin k + 1 2 s ds < e 2
1150 902 1149 r19.29a φ e + j k j π 0 U s sin k + 1 2 s ds < e
1151 1150 ralrimiva φ e + j k j π 0 U s sin k + 1 2 s ds < e
1152 nnex V
1153 1152 mptex n π 0 G s ds V
1154 1153 a1i φ n π 0 G s ds V
1155 eqidd φ k n π 0 G s ds = n π 0 G s ds
1156 784 adantl φ k n = k s π 0 s π π
1157 786 ad4ant14 φ k n = k s π 0 U s
1158 784 adantl k n = k s π 0 s π π
1159 simpr k n = k n = k
1160 simpl k n = k k
1161 1159 1160 eqeltrd k n = k n
1162 1161 nnred k n = k n
1163 737 a1i k n = k 1 2
1164 1162 1163 readdcld k n = k n + 1 2
1165 1164 adantr k n = k s π 0 n + 1 2
1166 232 1158 sseldi k n = k s π 0 s
1167 1165 1166 remulcld k n = k s π 0 n + 1 2 s
1168 1167 resincld k n = k s π 0 sin n + 1 2 s
1169 1158 1168 837 syl2anc k n = k s π 0 S s = sin n + 1 2 s
1170 1169 adantlll φ k n = k s π 0 S s = sin n + 1 2 s
1171 1162 adantll φ k n = k n
1172 1171 adantr φ k n = k s π 0 n
1173 1red φ k n = k s π 0 1
1174 1173 rehalfcld φ k n = k s π 0 1 2
1175 1172 1174 readdcld φ k n = k s π 0 n + 1 2
1176 232 1156 sseldi φ k n = k s π 0 s
1177 1175 1176 remulcld φ k n = k s π 0 n + 1 2 s
1178 1177 resincld φ k n = k s π 0 sin n + 1 2 s
1179 1170 1178 eqeltrd φ k n = k s π 0 S s
1180 1157 1179 remulcld φ k n = k s π 0 U s S s
1181 17 fvmpt2 s π π U s S s G s = U s S s
1182 1156 1180 1181 syl2anc φ k n = k s π 0 G s = U s S s
1183 oveq1 n = k n + 1 2 = k + 1 2
1184 1183 oveq1d n = k n + 1 2 s = k + 1 2 s
1185 1184 fveq2d n = k sin n + 1 2 s = sin k + 1 2 s
1186 1185 ad2antlr φ k n = k s π 0 sin n + 1 2 s = sin k + 1 2 s
1187 1170 1186 eqtrd φ k n = k s π 0 S s = sin k + 1 2 s
1188 1187 oveq2d φ k n = k s π 0 U s S s = U s sin k + 1 2 s
1189 1182 1188 eqtrd φ k n = k s π 0 G s = U s sin k + 1 2 s
1190 1189 itgeq2dv φ k n = k π 0 G s ds = π 0 U s sin k + 1 2 s ds
1191 simpr φ k k
1192 817 itgeq2dv n = k π 0 U s sin n + 1 2 s ds = π 0 U s sin k + 1 2 s ds
1193 1192 eleq1d n = k π 0 U s sin n + 1 2 s ds π 0 U s sin k + 1 2 s ds
1194 812 1193 imbi12d n = k φ n π 0 U s sin n + 1 2 s ds φ k π 0 U s sin k + 1 2 s ds
1195 786 adantlr φ n s π 0 U s
1196 simpr φ n n
1197 1196 784 833 syl2an φ n s π 0 sin n + 1 2 s
1198 1195 1197 remulcld φ n s π 0 U s sin n + 1 2 s
1199 1198 860 itgcl φ n π 0 U s sin n + 1 2 s ds
1200 1194 1199 chvarvv φ k π 0 U s sin k + 1 2 s ds
1201 1155 1190 1191 1200 fvmptd φ k n π 0 G s ds k = π 0 U s sin k + 1 2 s ds
1202 39 33 1154 1201 1200 clim0c φ n π 0 G s ds 0 e + j k j π 0 U s sin k + 1 2 s ds < e
1203 1151 1202 mpbird φ n π 0 G s ds 0
1204 1152 mptex n π 0 G s ds π V
1205 19 1204 eqeltri E V
1206 1205 a1i φ E V
1207 1152 mptex n π V
1208 1207 a1i φ n π V
1209 picn π
1210 1209 a1i φ π
1211 eqidd m n π = n π
1212 eqidd m n = m π = π
1213 id m m
1214 40 a1i m π
1215 1211 1212 1213 1214 fvmptd m n π m = π
1216 1215 adantl φ m n π m = π
1217 39 33 1208 1210 1216 climconst φ n π π
1218 778 79 gtneii π 0
1219 1218 a1i φ π 0
1220 2 adantr φ n X
1221 55 adantr φ n Y
1222 65 adantr φ n W
1223 843 1220 1221 1222 13 14 15 847 16 17 fourierdlem67 φ n G : π π
1224 1223 adantr φ n s π 0 G : π π
1225 821 sselda φ n s π 0 s π π
1226 1224 1225 ffvelrnd φ n s π 0 G s
1227 1223 ffvelrnda φ n s π π G s
1228 1223 feqmptd φ n G = s π π G s
1229 1228 858 eqeltrrd φ n s π π G s 𝐿 1
1230 821 823 1227 1229 iblss φ n s π 0 G s 𝐿 1
1231 1226 1230 itgcl φ n π 0 G s ds
1232 eqid n π 0 G s ds = n π 0 G s ds
1233 1232 fvmpt2 n π 0 G s ds n π 0 G s ds n = π 0 G s ds
1234 1196 1231 1233 syl2anc φ n n π 0 G s ds n = π 0 G s ds
1235 1234 1231 eqeltrd φ n n π 0 G s ds n
1236 id n n
1237 eqid n π = n π
1238 1237 fvmpt2 n π n π n = π
1239 1236 40 1238 sylancl n n π n = π
1240 1209 a1i n π
1241 1218 a1i n π 0
1242 1240 1241 jca n π π 0
1243 eldifsn π 0 π π 0
1244 1242 1243 sylibr n π 0
1245 1239 1244 eqeltrd n n π n 0
1246 1245 adantl φ n n π n 0
1247 1209 a1i φ n π
1248 1218 a1i φ n π 0
1249 1231 1247 1248 divcld φ n π 0 G s ds π
1250 19 fvmpt2 n π 0 G s ds π E n = π 0 G s ds π
1251 1196 1249 1250 syl2anc φ n E n = π 0 G s ds π
1252 1234 eqcomd φ n π 0 G s ds = n π 0 G s ds n
1253 1239 eqcomd n π = n π n
1254 1253 adantl φ n π = n π n
1255 1252 1254 oveq12d φ n π 0 G s ds π = n π 0 G s ds n n π n
1256 1251 1255 eqtrd φ n E n = n π 0 G s ds n n π n
1257 34 35 36 38 39 33 1203 1206 1217 1219 1235 1246 1256 climdivf φ E 0 π
1258 1209 1218 div0i 0 π = 0
1259 1258 a1i φ 0 π = 0
1260 1257 1259 breqtrd φ E 0
1261 1152 mptex m π 0 F X + s D m s ds V
1262 18 1261 eqeltri Z V
1263 1262 a1i φ Z V
1264 1152 mptex m W 2 V
1265 1264 a1i φ m W 2 V
1266 limccl F −∞ X lim X
1267 1266 21 sseldi φ W
1268 1267 halfcld φ W 2
1269 eqidd φ n 1 m W 2 = m W 2
1270 eqidd φ n 1 m = n W 2 = W 2
1271 39 eqcomi 1 =
1272 1271 eleq2i n 1 n
1273 1272 biimpi n 1 n
1274 1273 adantl φ n 1 n
1275 1268 adantr φ n 1 W 2
1276 1269 1270 1274 1275 fvmptd φ n 1 m W 2 n = W 2
1277 32 33 1265 1268 1276 climconst φ m W 2 W 2
1278 1249 19 fmptd φ E :
1279 1278 adantr φ n 1 E :
1280 1279 1274 ffvelrnd φ n 1 E n
1281 1276 1275 eqeltrd φ n 1 m W 2 n
1282 1276 oveq2d φ n 1 E n + m W 2 n = E n + W 2
1283 822 a1i φ π 0 dom vol
1284 75 a1i s π 0 π *
1285 0red s π 0 0
1286 1285 rexrd s π 0 0 *
1287 id s π 0 s π 0
1288 iooltub π * 0 * s π 0 s < 0
1289 1284 1286 1287 1288 syl3anc s π 0 s < 0
1290 794 1289 ltned s π 0 s 0
1291 1290 neneqd s π 0 ¬ s = 0
1292 velsn s 0 s = 0
1293 1291 1292 sylnibr s π 0 ¬ s 0
1294 784 1293 eldifd s π 0 s π π 0
1295 1294 ssriv π 0 π π 0
1296 1295 a1i φ π 0 π π 0
1297 794 adantl φ s π 0 s
1298 0red φ s π 0 0
1299 794 1285 1289 ltled s π 0 s 0
1300 1299 adantl φ s π 0 s 0
1301 1297 1298 1300 lensymd φ s π 0 ¬ 0 < s
1302 1301 iffalsed φ s π 0 if 0 < s Y W = W
1303 eqid D n = D n
1304 41 a1i φ n π
1305 0red φ n 0
1306 41 778 903 ltleii π 0
1307 1306 a1i φ n π 0
1308 eqid s π 0 s 2 + k = 1 n sin k s k π = s π 0 s 2 + k = 1 n sin k s k π
1309 24 1196 1303 1304 1305 1307 1308 dirkeritg φ n π 0 D n s ds = s π 0 s 2 + k = 1 n sin k s k π 0 s π 0 s 2 + k = 1 n sin k s k π π
1310 ubicc2 π * 0 * π 0 0 π 0
1311 75 76 1306 1310 mp3an 0 π 0
1312 oveq1 s = 0 s 2 = 0 2
1313 257 262 div0i 0 2 = 0
1314 1313 a1i s = 0 0 2 = 0
1315 1312 1314 eqtrd s = 0 s 2 = 0
1316 oveq2 s = 0 k s = k 0
1317 elfzelz k 1 n k
1318 1317 zcnd k 1 n k
1319 1318 mul01d k 1 n k 0 = 0
1320 1316 1319 sylan9eq s = 0 k 1 n k s = 0
1321 1320 fveq2d s = 0 k 1 n sin k s = sin 0
1322 sin0 sin 0 = 0
1323 1322 a1i s = 0 k 1 n sin 0 = 0
1324 1321 1323 eqtrd s = 0 k 1 n sin k s = 0
1325 1324 oveq1d s = 0 k 1 n sin k s k = 0 k
1326 0red k 1 n 0
1327 1red k 1 n 1
1328 1317 zred k 1 n k
1329 118 a1i k 1 n 0 < 1
1330 elfzle1 k 1 n 1 k
1331 1326 1327 1328 1329 1330 ltletrd k 1 n 0 < k
1332 1331 gt0ne0d k 1 n k 0
1333 1318 1332 div0d k 1 n 0 k = 0
1334 1333 adantl s = 0 k 1 n 0 k = 0
1335 1325 1334 eqtrd s = 0 k 1 n sin k s k = 0
1336 1335 sumeq2dv s = 0 k = 1 n sin k s k = k = 1 n 0
1337 fzfi 1 n Fin
1338 1337 olci 1 n ˙ 1 n Fin
1339 sumz 1 n ˙ 1 n Fin k = 1 n 0 = 0
1340 1338 1339 ax-mp k = 1 n 0 = 0
1341 1340 a1i s = 0 k = 1 n 0 = 0
1342 1336 1341 eqtrd s = 0 k = 1 n sin k s k = 0
1343 1315 1342 oveq12d s = 0 s 2 + k = 1 n sin k s k = 0 + 0
1344 00id 0 + 0 = 0
1345 1344 a1i s = 0 0 + 0 = 0
1346 1343 1345 eqtrd s = 0 s 2 + k = 1 n sin k s k = 0
1347 1346 oveq1d s = 0 s 2 + k = 1 n sin k s k π = 0 π
1348 1258 a1i s = 0 0 π = 0
1349 1347 1348 eqtrd s = 0 s 2 + k = 1 n sin k s k π = 0
1350 778 elexi 0 V
1351 1349 1308 1350 fvmpt 0 π 0 s π 0 s 2 + k = 1 n sin k s k π 0 = 0
1352 1311 1351 ax-mp s π 0 s 2 + k = 1 n sin k s k π 0 = 0
1353 lbicc2 π * 0 * π 0 π π 0
1354 75 76 1306 1353 mp3an π π 0
1355 oveq1 s = π s 2 = π 2
1356 oveq2 s = π k s = k π
1357 1356 fveq2d s = π sin k s = sin k π
1358 1357 oveq1d s = π sin k s k = sin k π k
1359 1358 sumeq2sdv s = π k = 1 n sin k s k = k = 1 n sin k π k
1360 1355 1359 oveq12d s = π s 2 + k = 1 n sin k s k = π 2 + k = 1 n sin k π k
1361 1360 oveq1d s = π s 2 + k = 1 n sin k s k π = π 2 + k = 1 n sin k π k π
1362 ovex π 2 + k = 1 n sin k π k π V
1363 1361 1308 1362 fvmpt π π 0 s π 0 s 2 + k = 1 n sin k s k π π = π 2 + k = 1 n sin k π k π
1364 1354 1363 ax-mp s π 0 s 2 + k = 1 n sin k s k π π = π 2 + k = 1 n sin k π k π
1365 mulneg12 k π k π = k π
1366 1318 1209 1365 sylancl k 1 n k π = k π
1367 1366 eqcomd k 1 n k π = k π
1368 1367 oveq1d k 1 n k π π = k π π
1369 1318 negcld k 1 n k
1370 1209 a1i k 1 n π
1371 1218 a1i k 1 n π 0
1372 1369 1370 1371 divcan4d k 1 n k π π = k
1373 1368 1372 eqtrd k 1 n k π π = k
1374 1317 znegcld k 1 n k
1375 1373 1374 eqeltrd k 1 n k π π
1376 negpicn π
1377 1376 a1i k 1 n π
1378 1318 1377 mulcld k 1 n k π
1379 sineq0 k π sin k π = 0 k π π
1380 1378 1379 syl k 1 n sin k π = 0 k π π
1381 1375 1380 mpbird k 1 n sin k π = 0
1382 1381 oveq1d k 1 n sin k π k = 0 k
1383 1382 1333 eqtrd k 1 n sin k π k = 0
1384 1383 sumeq2i k = 1 n sin k π k = k = 1 n 0
1385 1384 1340 eqtri k = 1 n sin k π k = 0
1386 1385 oveq2i π 2 + k = 1 n sin k π k = π 2 + 0
1387 1386 oveq1i π 2 + k = 1 n sin k π k π = π 2 + 0 π
1388 1376 257 262 divcli π 2
1389 1388 addid1i π 2 + 0 = π 2
1390 divneg π 2 2 0 π 2 = π 2
1391 1209 257 262 1390 mp3an π 2 = π 2
1392 1389 1391 eqtr4i π 2 + 0 = π 2
1393 1392 oveq1i π 2 + 0 π = π 2 π
1394 1040 recni π 2
1395 divneg π 2 π π 0 π 2 π = π 2 π
1396 1394 1209 1218 1395 mp3an π 2 π = π 2 π
1397 1396 eqcomi π 2 π = π 2 π
1398 1209 257 1209 262 1218 divdiv32i π 2 π = π π 2
1399 1209 1218 dividi π π = 1
1400 1399 oveq1i π π 2 = 1 2
1401 1398 1400 eqtri π 2 π = 1 2
1402 1401 negeqi π 2 π = 1 2
1403 1393 1397 1402 3eqtri π 2 + 0 π = 1 2
1404 1364 1387 1403 3eqtri s π 0 s 2 + k = 1 n sin k s k π π = 1 2
1405 1352 1404 oveq12i s π 0 s 2 + k = 1 n sin k s k π 0 s π 0 s 2 + k = 1 n sin k s k π π = 0 1 2
1406 1405 a1i φ n s π 0 s 2 + k = 1 n sin k s k π 0 s π 0 s 2 + k = 1 n sin k s k π π = 0 1 2
1407 halfcn 1 2
1408 1118 1407 subnegi 0 1 2 = 0 + 1 2
1409 1407 addid2i 0 + 1 2 = 1 2
1410 1408 1409 eqtri 0 1 2 = 1 2
1411 1410 a1i φ n 0 1 2 = 1 2
1412 1309 1406 1411 3eqtrd φ n π 0 D n s ds = 1 2
1413 1 2 3 4 5 6 7 11 12 13 14 15 16 17 854 607 22 23 20 21 1283 1296 19 24 65 1302 1412 fourierdlem95 φ n E n + W 2 = π 0 F X + s D n s ds
1414 1274 1413 syldan φ n 1 E n + W 2 = π 0 F X + s D n s ds
1415 18 a1i φ n Z = m π 0 F X + s D m s ds
1416 fveq2 m = n D m = D n
1417 1416 fveq1d m = n D m s = D n s
1418 1417 oveq2d m = n F X + s D m s = F X + s D n s
1419 1418 adantr m = n s π 0 F X + s D m s = F X + s D n s
1420 1419 itgeq2dv m = n π 0 F X + s D m s ds = π 0 F X + s D n s ds
1421 1420 adantl φ n m = n π 0 F X + s D m s ds = π 0 F X + s D n s ds
1422 1 adantr φ s π 0 F :
1423 2 adantr φ s π 0 X
1424 1423 1297 readdcld φ s π 0 X + s
1425 1422 1424 ffvelrnd φ s π 0 F X + s
1426 1425 adantlr φ n s π 0 F X + s
1427 24 dirkerf n D n :
1428 1427 ad2antlr φ n s π 0 D n :
1429 794 adantl φ n s π 0 s
1430 1428 1429 ffvelrnd φ n s π 0 D n s
1431 1426 1430 remulcld φ n s π 0 F X + s D n s
1432 1 adantr φ s π π F :
1433 2 adantr φ s π π X
1434 232 sseli s π π s
1435 1434 adantl φ s π π s
1436 1433 1435 readdcld φ s π π X + s
1437 1432 1436 ffvelrnd φ s π π F X + s
1438 1437 adantlr φ n s π π F X + s
1439 1427 ad2antlr φ n s π π D n :
1440 1434 adantl φ n s π π s
1441 1439 1440 ffvelrnd φ n s π π D n s
1442 1438 1441 remulcld φ n s π π F X + s D n s
1443 40 a1i φ n π
1444 24 dirkercncf n D n : cn
1445 1444 adantl φ n D n : cn
1446 eqid s π π F X + s D n s = s π π F X + s D n s
1447 1304 1443 843 1220 3 848 849 850 851 852 29 853 1445 1446 fourierdlem84 φ n s π π F X + s D n s 𝐿 1
1448 821 823 1442 1447 iblss φ n s π 0 F X + s D n s 𝐿 1
1449 1431 1448 itgrecl φ n π 0 F X + s D n s ds
1450 1415 1421 1196 1449 fvmptd φ n Z n = π 0 F X + s D n s ds
1451 1450 eqcomd φ n π 0 F X + s D n s ds = Z n
1452 1274 1451 syldan φ n 1 π 0 F X + s D n s ds = Z n
1453 1282 1414 1452 3eqtrrd φ n 1 Z n = E n + m W 2 n
1454 32 33 1260 1263 1277 1280 1281 1453 climadd φ Z 0 + W 2
1455 1268 addid2d φ 0 + W 2 = W 2
1456 1454 1455 breqtrd φ Z W 2