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 sseldi φ 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 syl6eq φ 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 &ApplyFunctio