Metamath Proof Explorer


Theorem fourierdlem104

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

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

Proof

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