Metamath Proof Explorer


Theorem fourierdlem111

Description: The fourier partial sum for F is the sum of two integrals, with the same integrand involving F and the Dirichlet Kernel D , but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem111.a A = n 0 π π F t cos n t dt π
fourierdlem111.b B = n π π F t sin n t dt π
fourierdlem111.s S = m A 0 2 + n = 1 m A n cos n X + B n sin n X
fourierdlem111.d D = n y if y mod 2 π = 0 2 n + 1 2 π sin n + 1 2 y 2 π sin y 2
fourierdlem111.p P = m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1
fourierdlem111.m φ M
fourierdlem111.q φ Q P M
fourierdlem111.x φ X
fourierdlem111.6 φ F :
fourierdlem111.fper φ x F x + T = F x
fourierdlem111.g G = x F X + x D n x
fourierdlem111.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem111.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
fourierdlem111.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
fourierdlem111.t T = 2 π
fourierdlem111.o O = m p 0 m | p 0 = - π - X p m = π X i 0 ..^ m p i < p i + 1
fourierdlem111.14 W = i 0 M Q i X
Assertion fourierdlem111 φ n S n = π 0 F X + s D n s ds + 0 π F X + s D n s ds

Proof

Step Hyp Ref Expression
1 fourierdlem111.a A = n 0 π π F t cos n t dt π
2 fourierdlem111.b B = n π π F t sin n t dt π
3 fourierdlem111.s S = m A 0 2 + n = 1 m A n cos n X + B n sin n X
4 fourierdlem111.d D = n y if y mod 2 π = 0 2 n + 1 2 π sin n + 1 2 y 2 π sin y 2
5 fourierdlem111.p P = m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1
6 fourierdlem111.m φ M
7 fourierdlem111.q φ Q P M
8 fourierdlem111.x φ X
9 fourierdlem111.6 φ F :
10 fourierdlem111.fper φ x F x + T = F x
11 fourierdlem111.g G = x F X + x D n x
12 fourierdlem111.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
13 fourierdlem111.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
14 fourierdlem111.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
15 fourierdlem111.t T = 2 π
16 fourierdlem111.o O = m p 0 m | p 0 = - π - X p m = π X i 0 ..^ m p i < p i + 1
17 fourierdlem111.14 W = i 0 M Q i X
18 eleq1 k = n k n
19 18 anbi2d k = n φ k φ n
20 fveq2 k = n S k = S n
21 fveq2 k = n D k = D n
22 21 fveq1d k = n D k t X = D n t X
23 22 oveq2d k = n F t D k t X = F t D n t X
24 23 adantr k = n t π π F t D k t X = F t D n t X
25 24 itgeq2dv k = n π π F t D k t X dt = π π F t D n t X dt
26 20 25 eqeq12d k = n S k = π π F t D k t X dt S n = π π F t D n t X dt
27 19 26 imbi12d k = n φ k S k = π π F t D k t X dt φ n S n = π π F t D n t X dt
28 9 adantr φ k F :
29 eqid π π = π π
30 ioossre π π
31 30 a1i φ π π
32 9 31 feqresmpt φ F π π = x π π F x
33 ioossicc π π π π
34 33 a1i φ π π π π
35 ioombl π π dom vol
36 35 a1i φ π π dom vol
37 9 adantr φ x π π F :
38 pire π
39 38 renegcli π
40 39 38 elicc2i t π π t π t t π
41 40 simp1bi t π π t
42 41 ssriv π π
43 42 a1i φ π π
44 43 sselda φ x π π x
45 37 44 ffvelrnd φ x π π F x
46 9 43 feqresmpt φ F π π = x π π F x
47 ax-resscn
48 47 a1i φ
49 9 48 fssd φ F :
50 49 43 fssresd φ F π π : π π
51 ioossicc Q i Q i + 1 Q i Q i + 1
52 39 rexri π *
53 52 a1i φ i 0 ..^ M π *
54 38 rexri π *
55 54 a1i φ i 0 ..^ M π *
56 5 6 7 fourierdlem15 φ Q : 0 M π π
57 56 adantr φ i 0 ..^ M Q : 0 M π π
58 simpr φ i 0 ..^ M i 0 ..^ M
59 53 55 57 58 fourierdlem8 φ i 0 ..^ M Q i Q i + 1 π π
60 51 59 sstrid φ i 0 ..^ M Q i Q i + 1 π π
61 60 resabs1d φ i 0 ..^ M F π π Q i Q i + 1 = F Q i Q i + 1
62 61 12 eqeltrd φ i 0 ..^ M F π π Q i Q i + 1 : Q i Q i + 1 cn
63 61 oveq1d φ i 0 ..^ M F π π Q i Q i + 1 lim Q i = F Q i Q i + 1 lim Q i
64 13 63 eleqtrrd φ i 0 ..^ M R F π π Q i Q i + 1 lim Q i
65 61 oveq1d φ i 0 ..^ M F π π Q i Q i + 1 lim Q i + 1 = F Q i Q i + 1 lim Q i + 1
66 14 65 eleqtrrd φ i 0 ..^ M L F π π Q i Q i + 1 lim Q i + 1
67 5 6 7 50 62 64 66 fourierdlem69 φ F π π 𝐿 1
68 46 67 eqeltrrd φ x π π F x 𝐿 1
69 34 36 45 68 iblss φ x π π F x 𝐿 1
70 32 69 eqeltrd φ F π π 𝐿 1
71 70 adantr φ k F π π 𝐿 1
72 8 adantr φ k X
73 simpr φ k k
74 28 29 71 1 2 72 3 4 73 fourierdlem83 φ k S k = π π F t D k t X dt
75 27 74 chvarvv φ n S n = π π F t D n t X dt
76 39 a1i φ n π
77 38 a1i φ n π
78 49 adantr φ t π π F :
79 41 adantl φ t π π t
80 78 79 ffvelrnd φ t π π F t
81 80 adantlr φ n t π π F t
82 4 dirkerf n D n :
83 82 ad2antlr φ n t π π D n :
84 8 adantr φ t π π X
85 79 84 resubcld φ t π π t X
86 85 adantlr φ n t π π t X
87 83 86 ffvelrnd φ n t π π D n t X
88 87 recnd φ n t π π D n t X
89 81 88 mulcld φ n t π π F t D n t X
90 76 77 89 itgioo φ n π π F t D n t X dt = π π F t D n t X dt
91 fvres t π π F π π t = F t
92 91 eqcomd t π π F t = F π π t
93 92 oveq1d t π π F t D n t X = F π π t D n t X
94 93 adantl φ n t π π F t D n t X = F π π t D n t X
95 94 itgeq2dv φ n π π F t D n t X dt = π π F π π t D n t X dt
96 simpl n = m y n = m
97 96 oveq2d n = m y 2 n = 2 m
98 97 oveq1d n = m y 2 n + 1 = 2 m + 1
99 98 oveq1d n = m y 2 n + 1 2 π = 2 m + 1 2 π
100 96 oveq1d n = m y n + 1 2 = m + 1 2
101 100 oveq1d n = m y n + 1 2 y = m + 1 2 y
102 101 fveq2d n = m y sin n + 1 2 y = sin m + 1 2 y
103 102 oveq1d n = m y sin n + 1 2 y 2 π sin y 2 = sin m + 1 2 y 2 π sin y 2
104 99 103 ifeq12d n = m y if y mod 2 π = 0 2 n + 1 2 π sin n + 1 2 y 2 π sin y 2 = if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
105 104 mpteq2dva n = m y if y mod 2 π = 0 2 n + 1 2 π sin n + 1 2 y 2 π sin y 2 = y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
106 105 cbvmptv n y if y mod 2 π = 0 2 n + 1 2 π sin n + 1 2 y 2 π sin y 2 = m y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
107 4 106 eqtri D = m y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
108 fveq2 s = t F π π s = F π π t
109 oveq1 s = t s X = t X
110 109 fveq2d s = t D n s X = D n t X
111 108 110 oveq12d s = t F π π s D n s X = F π π t D n t X
112 111 cbvmptv s π π F π π s D n s X = t π π F π π t D n t X
113 7 adantr φ n Q P M
114 6 adantr φ n M
115 simpr φ n n
116 8 adantr φ n X
117 50 adantr φ n F π π : π π
118 62 adantlr φ n i 0 ..^ M F π π Q i Q i + 1 : Q i Q i + 1 cn
119 64 adantlr φ n i 0 ..^ M R F π π Q i Q i + 1 lim Q i
120 66 adantlr φ n i 0 ..^ M L F π π Q i Q i + 1 lim Q i + 1
121 107 5 112 113 114 115 116 117 118 119 120 fourierdlem101 φ n π π F π π t D n t X dt = - π - X π X F π π X + y D n y dy
122 oveq2 s = y X + s = X + y
123 122 fveq2d s = y F X + s = F X + y
124 fveq2 s = y D n s = D n y
125 123 124 oveq12d s = y F X + s D n s = F X + y D n y
126 125 cbvitgv - π - X π X F X + s D n s ds = - π - X π X F X + y D n y dy
127 126 a1i φ n - π - X π X F X + s D n s ds = - π - X π X F X + y D n y dy
128 39 a1i φ π
129 128 8 resubcld φ - π - X
130 129 adantr φ n - π - X
131 38 a1i φ π
132 131 8 resubcld φ π X
133 132 adantr φ n π X
134 49 adantr φ y - π - X π X F :
135 8 adantr φ y - π - X π X X
136 simpr φ y - π - X π X y - π - X π X
137 129 adantr φ y - π - X π X - π - X
138 132 adantr φ y - π - X π X π X
139 elicc2 - π - X π X y - π - X π X y - π - X y y π X
140 137 138 139 syl2anc φ y - π - X π X y - π - X π X y - π - X y y π X
141 136 140 mpbid φ y - π - X π X y - π - X y y π X
142 141 simp1d φ y - π - X π X y
143 135 142 readdcld φ y - π - X π X X + y
144 134 143 ffvelrnd φ y - π - X π X F X + y
145 144 adantlr φ n y - π - X π X F X + y
146 82 ad2antlr φ n y - π - X π X D n :
147 142 adantlr φ n y - π - X π X y
148 146 147 ffvelrnd φ n y - π - X π X D n y
149 148 recnd φ n y - π - X π X D n y
150 145 149 mulcld φ n y - π - X π X F X + y D n y
151 130 133 150 itgioo φ n - π - X π X F X + y D n y dy = - π - X π X F X + y D n y dy
152 39 a1i φ y - π - X π X π
153 38 a1i φ y - π - X π X π
154 8 recnd φ X
155 131 recnd φ π
156 155 negcld φ π
157 154 156 pncan3d φ X + π - X = π
158 157 eqcomd φ π = X + π - X
159 158 adantr φ y - π - X π X π = X + π - X
160 141 simp2d φ y - π - X π X - π - X y
161 137 142 135 160 leadd2dd φ y - π - X π X X + π - X X + y
162 159 161 eqbrtrd φ y - π - X π X π X + y
163 141 simp3d φ y - π - X π X y π X
164 142 138 135 163 leadd2dd φ y - π - X π X X + y X + π - X
165 154 adantr φ y - π - X π X X
166 155 adantr φ y - π - X π X π
167 165 166 pncan3d φ y - π - X π X X + π - X = π
168 164 167 breqtrd φ y - π - X π X X + y π
169 152 153 143 162 168 eliccd φ y - π - X π X X + y π π
170 fvres X + y π π F π π X + y = F X + y
171 169 170 syl φ y - π - X π X F π π X + y = F X + y
172 171 eqcomd φ y - π - X π X F X + y = F π π X + y
173 172 adantlr φ n y - π - X π X F X + y = F π π X + y
174 173 oveq1d φ n y - π - X π X F X + y D n y = F π π X + y D n y
175 174 itgeq2dv φ n - π - X π X F X + y D n y dy = - π - X π X F π π X + y D n y dy
176 127 151 175 3eqtrrd φ n - π - X π X F π π X + y D n y dy = - π - X π X F X + s D n s ds
177 121 176 eqtrd φ n π π F π π t D n t X dt = - π - X π X F X + s D n s ds
178 90 95 177 3eqtrd φ n π π F t D n t X dt = - π - X π X F X + s D n s ds
179 elioore s - π - X π X s
180 179 adantl φ n s - π - X π X s
181 49 adantr φ s - π - X π X F :
182 8 adantr φ s - π - X π X X
183 179 adantl φ s - π - X π X s
184 182 183 readdcld φ s - π - X π X X + s
185 181 184 ffvelrnd φ s - π - X π X F X + s
186 185 adantlr φ n s - π - X π X F X + s
187 82 ad2antlr φ n s - π - X π X D n :
188 187 180 ffvelrnd φ n s - π - X π X D n s
189 188 recnd φ n s - π - X π X D n s
190 186 189 mulcld φ n s - π - X π X F X + s D n s
191 oveq2 x = s X + x = X + s
192 191 fveq2d x = s F X + x = F X + s
193 fveq2 x = s D n x = D n s
194 192 193 oveq12d x = s F X + x D n x = F X + s D n s
195 194 cbvmptv x F X + x D n x = s F X + s D n s
196 11 195 eqtri G = s F X + s D n s
197 196 fvmpt2 s F X + s D n s G s = F X + s D n s
198 180 190 197 syl2anc φ n s - π - X π X G s = F X + s D n s
199 198 eqcomd φ n s - π - X π X F X + s D n s = G s
200 199 itgeq2dv φ n - π - X π X F X + s D n s ds = - π - X π X G s ds
201 49 adantr φ x F :
202 8 adantr φ x X
203 simpr φ x x
204 202 203 readdcld φ x X + x
205 201 204 ffvelrnd φ x F X + x
206 205 adantlr φ n x F X + x
207 82 adantl φ n D n :
208 207 ffvelrnda φ n x D n x
209 208 recnd φ n x D n x
210 206 209 mulcld φ n x F X + x D n x
211 210 11 fmptd φ n G :
212 211 adantr φ n s - π - X π X G :
213 129 adantr φ s - π - X π X - π - X
214 132 adantr φ s - π - X π X π X
215 simpr φ s - π - X π X s - π - X π X
216 eliccre - π - X π X s - π - X π X s
217 213 214 215 216 syl3anc φ s - π - X π X s
218 217 adantlr φ n s - π - X π X s
219 212 218 ffvelrnd φ n s - π - X π X G s
220 130 133 219 itgioo φ n - π - X π X G s ds = - π - X π X G s ds
221 fveq2 s = x G s = G x
222 221 cbvitgv - π - X π X G s ds = - π - X π X G x dx
223 220 222 syl6eq φ n - π - X π X G s ds = - π - X π X G x dx
224 200 223 eqtrd φ n - π - X π X F X + s D n s ds = - π - X π X G x dx
225 eqid π - X - - π - X = π - X - - π - X
226 116 renegcld φ n X
227 5 fourierdlem2 M Q P M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
228 6 227 syl φ Q P M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
229 7 228 mpbid φ Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
230 229 simpld φ Q 0 M
231 elmapi Q 0 M Q : 0 M
232 230 231 syl φ Q : 0 M
233 232 ffvelrnda φ i 0 M Q i
234 8 adantr φ i 0 M X
235 233 234 resubcld φ i 0 M Q i X
236 235 17 fmptd φ W : 0 M
237 reex V
238 ovex 0 M V
239 237 238 pm3.2i V 0 M V
240 elmapg V 0 M V W 0 M W : 0 M
241 239 240 mp1i φ W 0 M W : 0 M
242 236 241 mpbird φ W 0 M
243 17 a1i φ W = i 0 M Q i X
244 fveq2 i = 0 Q i = Q 0
245 229 simprd φ Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
246 245 simpld φ Q 0 = π Q M = π
247 246 simpld φ Q 0 = π
248 244 247 sylan9eqr φ i = 0 Q i = π
249 248 oveq1d φ i = 0 Q i X = - π - X
250 0zd φ 0
251 6 nnzd φ M
252 0red M 0
253 nnre M M
254 nngt0 M 0 < M
255 252 253 254 ltled M 0 M
256 6 255 syl φ 0 M
257 eluz2 M 0 0 M 0 M
258 250 251 256 257 syl3anbrc φ M 0
259 eluzfz1 M 0 0 0 M
260 258 259 syl φ 0 0 M
261 243 249 260 129 fvmptd φ W 0 = - π - X
262 fveq2 i = M Q i = Q M
263 246 simprd φ Q M = π
264 262 263 sylan9eqr φ i = M Q i = π
265 264 oveq1d φ i = M Q i X = π X
266 eluzfz2 M 0 M 0 M
267 258 266 syl φ M 0 M
268 243 265 267 132 fvmptd φ W M = π X
269 261 268 jca φ W 0 = - π - X W M = π X
270 232 adantr φ i 0 ..^ M Q : 0 M
271 elfzofz i 0 ..^ M i 0 M
272 271 adantl φ i 0 ..^ M i 0 M
273 270 272 ffvelrnd φ i 0 ..^ M Q i
274 fzofzp1 i 0 ..^ M i + 1 0 M
275 274 adantl φ i 0 ..^ M i + 1 0 M
276 270 275 ffvelrnd φ i 0 ..^ M Q i + 1
277 8 adantr φ i 0 ..^ M X
278 245 simprd φ i 0 ..^ M Q i < Q i + 1
279 278 r19.21bi φ i 0 ..^ M Q i < Q i + 1
280 273 276 277 279 ltsub1dd φ i 0 ..^ M Q i X < Q i + 1 X
281 272 235 syldan φ i 0 ..^ M Q i X
282 17 fvmpt2 i 0 M Q i X W i = Q i X
283 272 281 282 syl2anc φ i 0 ..^ M W i = Q i X
284 fveq2 i = j Q i = Q j
285 284 oveq1d i = j Q i X = Q j X
286 285 cbvmptv i 0 M Q i X = j 0 M Q j X
287 17 286 eqtri W = j 0 M Q j X
288 287 a1i φ i 0 ..^ M W = j 0 M Q j X
289 fveq2 j = i + 1 Q j = Q i + 1
290 289 oveq1d j = i + 1 Q j X = Q i + 1 X
291 290 adantl φ i 0 ..^ M j = i + 1 Q j X = Q i + 1 X
292 276 277 resubcld φ i 0 ..^ M Q i + 1 X
293 288 291 275 292 fvmptd φ i 0 ..^ M W i + 1 = Q i + 1 X
294 280 283 293 3brtr4d φ i 0 ..^ M W i < W i + 1
295 294 ralrimiva φ i 0 ..^ M W i < W i + 1
296 242 269 295 jca32 φ W 0 M W 0 = - π - X W M = π X i 0 ..^ M W i < W i + 1
297 16 fourierdlem2 M W O M W 0 M W 0 = - π - X W M = π X i 0 ..^ M W i < W i + 1
298 6 297 syl φ W O M W 0 M W 0 = - π - X W M = π X i 0 ..^ M W i < W i + 1
299 296 298 mpbird φ W O M
300 299 adantr φ n W O M
301 155 156 154 nnncan2d φ π - X - - π - X = π π
302 picn π
303 302 2timesi 2 π = π + π
304 302 302 subnegi π π = π + π
305 303 15 304 3eqtr4i T = π π
306 301 305 syl6eqr φ π - X - - π - X = T
307 306 oveq2d φ x + π X - - π - X = x + T
308 307 fveq2d φ G x + π X - - π - X = G x + T
309 308 ad2antrr φ n x G x + π X - - π - X = G x + T
310 simpr φ n x x
311 11 fvmpt2 x F X + x D n x G x = F X + x D n x
312 310 210 311 syl2anc φ n x G x = F X + x D n x
313 154 adantr φ x X
314 203 recnd φ x x
315 2re 2
316 315 38 remulcli 2 π
317 15 316 eqeltri T
318 317 a1i φ T
319 318 recnd φ T
320 319 adantr φ x T
321 313 314 320 addassd φ x X + x + T = X + x + T
322 321 eqcomd φ x X + x + T = X + x + T
323 322 fveq2d φ x F X + x + T = F X + x + T
324 simpl φ x φ
325 324 204 jca φ x φ X + x
326 eleq1 s = X + x s X + x
327 326 anbi2d s = X + x φ s φ X + x
328 oveq1 s = X + x s + T = X + x + T
329 328 fveq2d s = X + x F s + T = F X + x + T
330 fveq2 s = X + x F s = F X + x
331 329 330 eqeq12d s = X + x F s + T = F s F X + x + T = F X + x
332 327 331 imbi12d s = X + x φ s F s + T = F s φ X + x F X + x + T = F X + x
333 eleq1 x = s x s
334 333 anbi2d x = s φ x φ s
335 oveq1 x = s x + T = s + T
336 335 fveq2d x = s F x + T = F s + T
337 fveq2 x = s F x = F s
338 336 337 eqeq12d x = s F x + T = F x F s + T = F s
339 334 338 imbi12d x = s φ x F x + T = F x φ s F s + T = F s
340 339 10 chvarvv φ s F s + T = F s
341 332 340 vtoclg X + x φ X + x F X + x + T = F X + x
342 204 325 341 sylc φ x F X + x + T = F X + x
343 323 342 eqtr2d φ x F X + x = F X + x + T
344 343 adantlr φ n x F X + x = F X + x + T
345 4 15 dirkerper n x D n x + T = D n x
346 345 eqcomd n x D n x = D n x + T
347 346 adantll φ n x D n x = D n x + T
348 344 347 oveq12d φ n x F X + x D n x = F X + x + T D n x + T
349 196 a1i φ n x G = s F X + s D n s
350 oveq2 s = x + T X + s = X + x + T
351 350 fveq2d s = x + T F X + s = F X + x + T
352 fveq2 s = x + T D n s = D n x + T
353 351 352 oveq12d s = x + T F X + s D n s = F X + x + T D n x + T
354 353 adantl φ n x s = x + T F X + s D n s = F X + x + T D n x + T
355 317 a1i φ n x T
356 310 355 readdcld φ n x x + T
357 317 a1i φ x T
358 203 357 readdcld φ x x + T
359 202 358 readdcld φ x X + x + T
360 201 359 ffvelrnd φ x F X + x + T
361 360 adantlr φ n x F X + x + T
362 82 ad2antlr φ n x D n :
363 362 356 ffvelrnd φ n x D n x + T
364 363 recnd φ n x D n x + T
365 361 364 mulcld φ n x F X + x + T D n x + T
366 349 354 356 365 fvmptd φ n x G x + T = F X + x + T D n x + T
367 366 eqcomd φ n x F X + x + T D n x + T = G x + T
368 312 348 367 3eqtrrd φ n x G x + T = G x
369 309 368 eqtrd φ n x G x + π X - - π - X = G x
370 196 reseq1i G W i W i + 1 = s F X + s D n s W i W i + 1
371 370 a1i φ n i 0 ..^ M G W i W i + 1 = s F X + s D n s W i W i + 1
372 ioossre W i W i + 1
373 resmpt W i W i + 1 s F X + s D n s W i W i + 1 = s W i W i + 1 F X + s D n s
374 372 373 ax-mp s F X + s D n s W i W i + 1 = s W i W i + 1 F X + s D n s
375 371 374 syl6eq φ n i 0 ..^ M G W i W i + 1 = s W i W i + 1 F X + s D n s
376 273 rexrd φ i 0 ..^ M Q i *
377 376 adantr φ i 0 ..^ M s W i W i + 1 Q i *
378 276 rexrd φ i 0 ..^ M Q i + 1 *
379 378 adantr φ i 0 ..^ M s W i W i + 1 Q i + 1 *
380 8 adantr φ s W i W i + 1 X
381 elioore s W i W i + 1 s
382 381 adantl φ s W i W i + 1 s
383 380 382 readdcld φ s W i W i + 1 X + s
384 383 adantlr φ i 0 ..^ M s W i W i + 1 X + s
385 eleq1 x = s x W i W i + 1 s W i W i + 1
386 385 anbi2d x = s φ i 0 ..^ M x W i W i + 1 φ i 0 ..^ M s W i W i + 1
387 191 breq2d x = s Q i < X + x Q i < X + s
388 386 387 imbi12d x = s φ i 0 ..^ M x W i W i + 1 Q i < X + x φ i 0 ..^ M s W i W i + 1 Q i < X + s
389 154 adantr φ i 0 ..^ M X
390 283 281 eqeltrd φ i 0 ..^ M W i
391 390 recnd φ i 0 ..^ M W i
392 389 391 addcomd φ i 0 ..^ M X + W i = W i + X
393 283 oveq1d φ i 0 ..^ M W i + X = Q i - X + X
394 273 recnd φ i 0 ..^ M Q i
395 394 389 npcand φ i 0 ..^ M Q i - X + X = Q i
396 392 393 395 3eqtrrd φ i 0 ..^ M Q i = X + W i
397 396 adantr φ i 0 ..^ M x W i W i + 1 Q i = X + W i
398 390 adantr φ i 0 ..^ M x W i W i + 1 W i
399 elioore x W i W i + 1 x
400 399 adantl φ i 0 ..^ M x W i W i + 1 x
401 8 ad2antrr φ i 0 ..^ M x W i W i + 1 X
402 390 rexrd φ i 0 ..^ M W i *
403 402 adantr φ i 0 ..^ M x W i W i + 1 W i *
404 293 292 eqeltrd φ i 0 ..^ M W i + 1
405 404 rexrd φ i 0 ..^ M W i + 1 *
406 405 adantr φ i 0 ..^ M x W i W i + 1 W i + 1 *
407 simpr φ i 0 ..^ M x W i W i + 1 x W i W i + 1
408 ioogtlb W i * W i + 1 * x W i W i + 1 W i < x
409 403 406 407 408 syl3anc φ i 0 ..^ M x W i W i + 1 W i < x
410 398 400 401 409 ltadd2dd φ i 0 ..^ M x W i W i + 1 X + W i < X + x
411 397 410 eqbrtrd φ i 0 ..^ M x W i W i + 1 Q i < X + x
412 388 411 chvarvv φ i 0 ..^ M s W i W i + 1 Q i < X + s
413 191 breq1d x = s X + x < Q i + 1 X + s < Q i + 1
414 386 413 imbi12d x = s φ i 0 ..^ M x W i W i + 1 X + x < Q i + 1 φ i 0 ..^ M s W i W i + 1 X + s < Q i + 1
415 404 adantr φ i 0 ..^ M x W i W i + 1 W i + 1
416 iooltub W i * W i + 1 * x W i W i + 1 x < W i + 1
417 403 406 407 416 syl3anc φ i 0 ..^ M x W i W i + 1 x < W i + 1
418 400 415 401 417 ltadd2dd φ i 0 ..^ M x W i W i + 1 X + x < X + W i + 1
419 404 recnd φ i 0 ..^ M W i + 1
420 389 419 addcomd φ i 0 ..^ M X + W i + 1 = W i + 1 + X
421 293 oveq1d φ i 0 ..^ M W i + 1 + X = Q i + 1 - X + X
422 276 recnd φ i 0 ..^ M Q i + 1
423 422 389 npcand φ i 0 ..^ M Q i + 1 - X + X = Q i + 1
424 420 421 423 3eqtrd φ i 0 ..^ M X + W i + 1 = Q i + 1
425 424 adantr φ i 0 ..^ M x W i W i + 1 X + W i + 1 = Q i + 1
426 418 425 breqtrd φ i 0 ..^ M x W i W i + 1 X + x < Q i + 1
427 414 426 chvarvv φ i 0 ..^ M s W i W i + 1 X + s < Q i + 1
428 377 379 384 412 427 eliood φ i 0 ..^ M s W i W i + 1 X + s Q i Q i + 1
429 191 cbvmptv x W i W i + 1 X + x = s W i W i + 1 X + s
430 429 a1i φ i 0 ..^ M x W i W i + 1 X + x = s W i W i + 1 X + s
431 ioossre Q i Q i + 1
432 431 a1i φ Q i Q i + 1
433 9 432 feqresmpt φ F Q i Q i + 1 = x Q i Q i + 1 F x
434 433 adantr φ i 0 ..^ M F Q i Q i + 1 = x Q i Q i + 1 F x
435 fveq2 x = X + s F x = F X + s
436 428 430 434 435 fmptco φ i 0 ..^ M F Q i Q i + 1 x W i W i + 1 X + x = s W i W i + 1 F X + s
437 eqid x X + x = x X + x
438 ssid
439 438 a1i φ
440 439 154 439 constcncfg φ x X : cn
441 cncfmptid x x : cn
442 438 438 441 mp2an x x : cn
443 442 a1i φ x x : cn
444 440 443 addcncf φ x X + x : cn
445 444 adantr φ i 0 ..^ M x X + x : cn
446 ioosscn W i W i + 1
447 446 a1i φ i 0 ..^ M W i W i + 1
448 ioosscn Q i Q i + 1
449 448 a1i φ i 0 ..^ M Q i Q i + 1
450 376 adantr φ i 0 ..^ M x W i W i + 1 Q i *
451 378 adantr φ i 0 ..^ M x W i W i + 1 Q i + 1 *
452 8 adantr φ x W i W i + 1 X
453 399 adantl φ x W i W i + 1 x
454 452 453 readdcld φ x W i W i + 1 X + x
455 454 adantlr φ i 0 ..^ M x W i W i + 1 X + x
456 450 451 455 411 426 eliood φ i 0 ..^ M x W i W i + 1 X + x Q i Q i + 1
457 437 445 447 449 456 cncfmptssg φ i 0 ..^ M x W i W i + 1 X + x : W i W i + 1 cn Q i Q i + 1
458 457 12 cncfco φ i 0 ..^ M F Q i Q i + 1 x W i W i + 1 X + x : W i W i + 1 cn
459 436 458 eqeltrrd φ i 0 ..^ M s W i W i + 1 F X + s : W i W i + 1 cn
460 459 adantlr φ n i 0 ..^ M s W i W i + 1 F X + s : W i W i + 1 cn
461 eqid s D n s = s D n s
462 82 feqmptd n D n = s D n s
463 cncfss cn cn
464 47 438 463 mp2an cn cn
465 4 dirkercncf n D n : cn
466 464 465 sseldi n D n : cn
467 462 466 eqeltrrd n s D n s : cn
468 372 a1i n W i W i + 1
469 438 a1i n
470 cncff D n : cn D n :
471 466 470 syl n D n :
472 471 adantr n s W i W i + 1 D n :
473 381 adantl n s W i W i + 1 s
474 472 473 ffvelrnd n s W i W i + 1 D n s
475 461 467 468 469 474 cncfmptssg n s W i W i + 1 D n s : W i W i + 1 cn
476 475 ad2antlr φ n i 0 ..^ M s W i W i + 1 D n s : W i W i + 1 cn
477 460 476 mulcncf φ n i 0 ..^ M s W i W i + 1 F X + s D n s : W i W i + 1 cn
478 375 477 eqeltrd φ n i 0 ..^ M G W i W i + 1 : W i W i + 1 cn
479 453 205 syldan φ x W i W i + 1 F X + x
480 479 adantlr φ i 0 ..^ M x W i W i + 1 F X + x
481 eqid x W i W i + 1 F X + x = x W i W i + 1 F X + x
482 480 481 fmptd φ i 0 ..^ M x W i W i + 1 F X + x : W i W i + 1
483 482 adantlr φ n i 0 ..^ M x W i W i + 1 F X + x : W i W i + 1
484 82 ad2antlr φ n i 0 ..^ M D n :
485 372 a1i φ n i 0 ..^ M W i W i + 1
486 484 485 fssresd φ n i 0 ..^ M D n W i W i + 1 : W i W i + 1
487 47 a1i φ n i 0 ..^ M
488 486 487 fssd φ n i 0 ..^ M D n W i W i + 1 : W i W i + 1
489 eqid s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s = s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s
490 fdm F : dom F =
491 49 490 syl φ dom F =
492 431 491 sseqtrrid φ Q i Q i + 1 dom F
493 ssdmres Q i Q i + 1 dom F dom F Q i Q i + 1 = Q i Q i + 1
494 492 493 sylib φ dom F Q i Q i + 1 = Q i Q i + 1
495 494 eqcomd φ Q i Q i + 1 = dom F Q i Q i + 1
496 495 ad2antrr φ i 0 ..^ M x W i W i + 1 Q i Q i + 1 = dom F Q i Q i + 1
497 456 496 eleqtrd φ i 0 ..^ M x W i W i + 1 X + x dom F Q i Q i + 1
498 273 adantr φ i 0 ..^ M x W i W i + 1 Q i
499 498 411 gtned φ i 0 ..^ M x W i W i + 1 X + x Q i
500 eldifsn X + x dom F Q i Q i + 1 Q i X + x dom F Q i Q i + 1 X + x Q i
501 497 499 500 sylanbrc φ i 0 ..^ M x W i W i + 1 X + x dom F Q i Q i + 1 Q i
502 501 ralrimiva φ i 0 ..^ M x W i W i + 1 X + x dom F Q i Q i + 1 Q i
503 eqid x W i W i + 1 X + x = x W i W i + 1 X + x
504 503 rnmptss x W i W i + 1 X + x dom F Q i Q i + 1 Q i ran x W i W i + 1 X + x dom F Q i Q i + 1 Q i
505 502 504 syl φ i 0 ..^ M ran x W i W i + 1 X + x dom F Q i Q i + 1 Q i
506 eqidd φ i 0 ..^ M x W i W i + 1 X + x = x W i W i + 1 X + x
507 oveq2 x = W i X + x = X + W i
508 507 adantl φ i 0 ..^ M x = W i X + x = X + W i
509 390 leidd φ i 0 ..^ M W i W i
510 390 404 294 ltled φ i 0 ..^ M W i W i + 1
511 390 404 390 509 510 eliccd φ i 0 ..^ M W i W i W i + 1
512 396 273 eqeltrrd φ i 0 ..^ M X + W i
513 506 508 511 512 fvmptd φ i 0 ..^ M x W i W i + 1 X + x W i = X + W i
514 396 eqcomd φ i 0 ..^ M X + W i = Q i
515 513 514 eqtr2d φ i 0 ..^ M Q i = x W i W i + 1 X + x W i
516 390 404 iccssred φ i 0 ..^ M W i W i + 1
517 516 47 sstrdi φ i 0 ..^ M W i W i + 1
518 517 resmptd φ i 0 ..^ M x X + x W i W i + 1 = x W i W i + 1 X + x
519 rescncf W i W i + 1 x X + x : cn x X + x W i W i + 1 : W i W i + 1 cn
520 517 445 519 sylc φ i 0 ..^ M x X + x W i W i + 1 : W i W i + 1 cn
521 518 520 eqeltrrd φ i 0 ..^ M x W i W i + 1 X + x : W i W i + 1 cn
522 521 511 cnlimci φ i 0 ..^ M x W i W i + 1 X + x W i x W i W i + 1 X + x lim W i
523 515 522 eqeltrd φ i 0 ..^ M Q i x W i W i + 1 X + x lim W i
524 ioossicc W i W i + 1 W i W i + 1
525 resmpt W i W i + 1 W i W i + 1 x W i W i + 1 X + x W i W i + 1 = x W i W i + 1 X + x
526 524 525 ax-mp x W i W i + 1 X + x W i W i + 1 = x W i W i + 1 X + x
527 526 eqcomi x W i W i + 1 X + x = x W i W i + 1 X + x W i W i + 1
528 527 a1i φ i 0 ..^ M x W i W i + 1 X + x = x W i W i + 1 X + x W i W i + 1
529 528 oveq1d φ i 0 ..^ M x W i W i + 1 X + x lim W i = x W i W i + 1 X + x W i W i + 1 lim W i
530 154 ad2antrr φ i 0 ..^ M x W i W i + 1 X
531 390 adantr φ i 0 ..^ M x W i W i + 1 W i
532 404 adantr φ i 0 ..^ M x W i W i + 1 W i + 1
533 simpr φ i 0 ..^ M x W i W i + 1 x W i W i + 1
534 eliccre W i W i + 1 x W i W i + 1 x
535 531 532 533 534 syl3anc φ i 0 ..^ M x W i W i + 1 x
536 535 recnd φ i 0 ..^ M x W i W i + 1 x
537 530 536 addcld φ i 0 ..^ M x W i W i + 1 X + x
538 eqid x W i W i + 1 X + x = x W i W i + 1 X + x
539 537 538 fmptd φ i 0 ..^ M x W i W i + 1 X + x : W i W i + 1
540 390 404 294 539 limciccioolb φ i 0 ..^ M x W i W i + 1 X + x W i W i + 1 lim W i = x W i W i + 1 X + x lim W i
541 529 540 eqtr2d φ i 0 ..^ M x W i W i + 1 X + x lim W i = x W i W i + 1 X + x lim W i
542 523 541 eleqtrd φ i 0 ..^ M Q i x W i W i + 1 X + x lim W i
543 505 542 13 limccog φ i 0 ..^ M R F Q i Q i + 1 x W i W i + 1 X + x lim W i
544 49 432 fssresd φ F Q i Q i + 1 : Q i Q i + 1
545 544 adantr φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
546 456 503 fmptd φ i 0 ..^ M x W i W i + 1 X + x : W i W i + 1 Q i Q i + 1
547 fcompt F Q i Q i + 1 : Q i Q i + 1 x W i W i + 1 X + x : W i W i + 1 Q i Q i + 1 F Q i Q i + 1 x W i W i + 1 X + x = y W i W i + 1 F Q i Q i + 1 x W i W i + 1 X + x y
548 545 546 547 syl2anc φ i 0 ..^ M F Q i Q i + 1 x W i W i + 1 X + x = y W i W i + 1 F Q i Q i + 1 x W i W i + 1 X + x y
549 eqidd φ y W i W i + 1 x W i W i + 1 X + x = x W i W i + 1 X + x
550 oveq2 x = y X + x = X + y
551 550 adantl φ y W i W i + 1 x = y X + x = X + y
552 simpr φ y W i W i + 1 y W i W i + 1
553 8 adantr φ y W i W i + 1 X
554 372 552 sseldi φ y W i W i + 1 y
555 553 554 readdcld φ y W i W i + 1 X + y
556 549 551 552 555 fvmptd φ y W i W i + 1 x W i W i + 1 X + x y = X + y
557 556 fveq2d φ y W i W i + 1 F Q i Q i + 1 x W i W i + 1 X + x y = F Q i Q i + 1 X + y
558 557 adantlr φ i 0 ..^ M y W i W i + 1 F Q i Q i + 1 x W i W i + 1 X + x y = F Q i Q i + 1 X + y
559 376 adantr φ i 0 ..^ M y W i W i + 1 Q i *
560 378 adantr φ i 0 ..^ M y W i W i + 1 Q i + 1 *
561 555 adantlr φ i 0 ..^ M y W i W i + 1 X + y
562 396 adantr φ i 0 ..^ M y W i W i + 1 Q i = X + W i
563 390 adantr φ i 0 ..^ M y W i W i + 1 W i
564 554 adantlr φ i 0 ..^ M y W i W i + 1 y
565 8 ad2antrr φ i 0 ..^ M y W i W i + 1 X
566 402 adantr φ i 0 ..^ M y W i W i + 1 W i *
567 405 adantr φ i 0 ..^ M y W i W i + 1 W i + 1 *
568 simpr φ i 0 ..^ M y W i W i + 1 y W i W i + 1
569 ioogtlb W i * W i + 1 * y W i W i + 1 W i < y
570 566 567 568 569 syl3anc φ i 0 ..^ M y W i W i + 1 W i < y
571 563 564 565 570 ltadd2dd φ i 0 ..^ M y W i W i + 1 X + W i < X + y
572 562 571 eqbrtrd φ i 0 ..^ M y W i W i + 1 Q i < X + y
573 404 adantr φ i 0 ..^ M y W i W i + 1 W i + 1
574 iooltub W i * W i + 1 * y W i W i + 1 y < W i + 1
575 566 567 568 574 syl3anc φ i 0 ..^ M y W i W i + 1 y < W i + 1
576 564 573 565 575 ltadd2dd φ i 0 ..^ M y W i W i + 1 X + y < X + W i + 1
577 424 adantr φ i 0 ..^ M y W i W i + 1 X + W i + 1 = Q i + 1
578 576 577 breqtrd φ i 0 ..^ M y W i W i + 1 X + y < Q i + 1
579 559 560 561 572 578 eliood φ i 0 ..^ M y W i W i + 1 X + y Q i Q i + 1
580 fvres X + y Q i Q i + 1 F Q i Q i + 1 X + y = F X + y
581 579 580 syl φ i 0 ..^ M y W i W i + 1 F Q i Q i + 1 X + y = F X + y
582 558 581 eqtrd φ i 0 ..^ M y W i W i + 1 F Q i Q i + 1 x W i W i + 1 X + x y = F X + y
583 582 mpteq2dva φ i 0 ..^ M y W i W i + 1 F Q i Q i + 1 x W i W i + 1 X + x y = y W i W i + 1 F X + y
584 550 fveq2d x = y F X + x = F X + y
585 584 cbvmptv x W i W i + 1 F X + x = y W i W i + 1 F X + y
586 583 585 syl6eqr φ i 0 ..^ M y W i W i + 1 F Q i Q i + 1 x W i W i + 1 X + x y = x W i W i + 1 F X + x
587 548 586 eqtrd φ i 0 ..^ M F Q i Q i + 1 x W i W i + 1 X + x = x W i W i + 1 F X + x
588 587 oveq1d φ i 0 ..^ M F Q i Q i + 1 x W i W i + 1 X + x lim W i = x W i W i + 1 F X + x lim W i
589 543 588 eleqtrd φ i 0 ..^ M R x W i W i + 1 F X + x lim W i
590 589 adantlr φ n i 0 ..^ M R x W i W i + 1 F X + x lim W i
591 fvres W i W i W i + 1 D n W i W i + 1 W i = D n W i
592 511 591 syl φ i 0 ..^ M D n W i W i + 1 W i = D n W i
593 592 eqcomd φ i 0 ..^ M D n W i = D n W i W i + 1 W i
594 593 adantlr φ n i 0 ..^ M D n W i = D n W i W i + 1 W i
595 516 adantlr φ n i 0 ..^ M W i W i + 1
596 465 ad2antlr φ n i 0 ..^ M D n : cn
597 rescncf W i W i + 1 D n : cn D n W i W i + 1 : W i W i + 1 cn
598 595 596 597 sylc φ n i 0 ..^ M D n W i W i + 1 : W i W i + 1 cn
599 511 adantlr φ n i 0 ..^ M W i W i W i + 1
600 598 599 cnlimci φ n i 0 ..^ M D n W i W i + 1 W i D n W i W i + 1 lim W i
601 594 600 eqeltrd φ n i 0 ..^ M D n W i D n W i W i + 1 lim W i
602 524 a1i φ i 0 ..^ M W i W i + 1 W i W i + 1
603 602 resabs1d φ i 0 ..^ M D n W i W i + 1 W i W i + 1 = D n W i W i + 1
604 603 eqcomd φ i 0 ..^ M D n W i W i + 1 = D n W i W i + 1 W i W i + 1
605 604 oveq1d φ i 0 ..^ M D n W i W i + 1 lim W i = D n W i W i + 1 W i W i + 1 lim W i
606 605 adantlr φ n i 0 ..^ M D n W i W i + 1 lim W i = D n W i W i + 1 W i W i + 1 lim W i
607 390 adantlr φ n i 0 ..^ M W i
608 404 adantlr φ n i 0 ..^ M W i + 1
609 294 adantlr φ n i 0 ..^ M W i < W i + 1
610 471 ad2antlr φ n i 0 ..^ M D n :
611 610 595 fssresd φ n i 0 ..^ M D n W i W i + 1 : W i W i + 1
612 607 608 609 611 limciccioolb φ n i 0 ..^ M D n W i W i + 1 W i W i + 1 lim W i = D n W i W i + 1 lim W i
613 606 612 eqtr2d φ n i 0 ..^ M D n W i W i + 1 lim W i = D n W i W i + 1 lim W i
614 601 613 eleqtrd φ n i 0 ..^ M D n W i D n W i W i + 1 lim W i
615 483 488 489 590 614 mullimcf φ n i 0 ..^ M R D n W i s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s lim W i
616 eqidd φ i 0 ..^ M s W i W i + 1 x W i W i + 1 F X + x = x W i W i + 1 F X + x
617 192 adantl φ i 0 ..^ M s W i W i + 1 x = s F X + x = F X + s
618 simpr φ i 0 ..^ M s W i W i + 1 s W i W i + 1
619 49 adantr φ s W i W i + 1 F :
620 619 383 ffvelrnd φ s W i W i + 1 F X + s
621 620 adantlr φ i 0 ..^ M s W i W i + 1 F X + s
622 616 617 618 621 fvmptd φ i 0 ..^ M s W i W i + 1 x W i W i + 1 F X + x s = F X + s
623 622 adantllr φ n i 0 ..^ M s W i W i + 1 x W i W i + 1 F X + x s = F X + s
624 fvres s W i W i + 1 D n W i W i + 1 s = D n s
625 624 adantl φ n i 0 ..^ M s W i W i + 1 D n W i W i + 1 s = D n s
626 623 625 oveq12d φ n i 0 ..^ M s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s = F X + s D n s
627 626 eqcomd φ n i 0 ..^ M s W i W i + 1 F X + s D n s = x W i W i + 1 F X + x s D n W i W i + 1 s
628 627 mpteq2dva φ n i 0 ..^ M s W i W i + 1 F X + s D n s = s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s
629 375 628 eqtr2d φ n i 0 ..^ M s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s = G W i W i + 1
630 629 oveq1d φ n i 0 ..^ M s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s lim W i = G W i W i + 1 lim W i
631 615 630 eleqtrd φ n i 0 ..^ M R D n W i G W i W i + 1 lim W i
632 455 426 ltned φ i 0 ..^ M x W i W i + 1 X + x Q i + 1
633 eldifsn X + x dom F Q i Q i + 1 Q i + 1 X + x dom F Q i Q i + 1 X + x Q i + 1
634 497 632 633 sylanbrc φ i 0 ..^ M x W i W i + 1 X + x dom F Q i Q i + 1 Q i + 1
635 634 ralrimiva φ i 0 ..^ M x W i W i + 1 X + x dom F Q i Q i + 1 Q i + 1
636 503 rnmptss x W i W i + 1 X + x dom F Q i Q i + 1 Q i + 1 ran x W i W i + 1 X + x dom F Q i Q i + 1 Q i + 1
637 635 636 syl φ i 0 ..^ M ran x W i W i + 1 X + x dom F Q i Q i + 1 Q i + 1
638 404 leidd φ i 0 ..^ M W i + 1 W i + 1
639 390 404 404 510 638 eliccd φ i 0 ..^ M W i + 1 W i W i + 1
640 521 639 cnlimci φ i 0 ..^ M x W i W i + 1 X + x W i + 1 x W i W i + 1 X + x lim W i + 1
641 oveq2 x = W i + 1 X + x = X + W i + 1
642 641 adantl φ i 0 ..^ M x = W i + 1 X + x = X + W i + 1
643 277 404 readdcld φ i 0 ..^ M X + W i + 1
644 506 642 639 643 fvmptd φ i 0 ..^ M x W i W i + 1 X + x W i + 1 = X + W i + 1
645 644 424 eqtrd φ i 0 ..^ M x W i W i + 1 X + x W i + 1 = Q i + 1
646 528 oveq1d φ i 0 ..^ M x W i W i + 1 X + x lim W i + 1 = x W i W i + 1 X + x W i W i + 1 lim W i + 1
647 390 404 294 539 limcicciooub φ i 0 ..^ M x W i W i + 1 X + x W i W i + 1 lim W i + 1 = x W i W i + 1 X + x lim W i + 1
648 646 647 eqtr2d φ i 0 ..^ M x W i W i + 1 X + x lim W i + 1 = x W i W i + 1 X + x lim W i + 1
649 640 645 648 3eltr3d φ i 0 ..^ M Q i + 1 x W i W i + 1 X + x lim W i + 1
650 637 649 14 limccog φ i 0 ..^ M L F Q i Q i + 1 x W i W i + 1 X + x lim W i + 1
651 587 oveq1d φ i 0 ..^ M F Q i Q i + 1 x W i W i + 1 X + x lim W i + 1 = x W i W i + 1 F X + x lim W i + 1
652 650 651 eleqtrd φ i 0 ..^ M L x W i W i + 1 F X + x lim W i + 1
653 652 adantlr φ n i 0 ..^ M L x W i W i + 1 F X + x lim W i + 1
654 639 adantlr φ n i 0 ..^ M W i + 1 W i W i + 1
655 598 654 cnlimci φ n i 0 ..^ M D n W i W i + 1 W i + 1 D n W i W i + 1 lim W i + 1
656 fvres W i + 1 W i W i + 1 D n W i W i + 1 W i + 1 = D n W i + 1
657 654 656 syl φ n i 0 ..^ M D n W i W i + 1 W i + 1 = D n W i + 1
658 607 608 609 611 limcicciooub φ n i 0 ..^ M D n W i W i + 1 W i W i + 1 lim W i + 1 = D n W i W i + 1 lim W i + 1
659 658 eqcomd φ n i 0 ..^ M D n W i W i + 1 lim W i + 1 = D n W i W i + 1 W i W i + 1 lim W i + 1
660 resabs1 W i W i + 1 W i W i + 1 D n W i W i + 1 W i W i + 1 = D n W i W i + 1
661 524 660 mp1i φ n i 0 ..^ M D n W i W i + 1 W i W i + 1 = D n W i W i + 1
662 661 oveq1d φ n i 0 ..^ M D n W i W i + 1 W i W i + 1 lim W i + 1 = D n W i W i + 1 lim W i + 1
663 659 662 eqtrd φ n i 0 ..^ M D n W i W i + 1 lim W i + 1 = D n W i W i + 1 lim W i + 1
664 655 657 663 3eltr3d φ n i 0 ..^ M D n W i + 1 D n W i W i + 1 lim W i + 1
665 483 488 489 653 664 mullimcf φ n i 0 ..^ M L D n W i + 1 s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s lim W i + 1
666 629 oveq1d φ n i 0 ..^ M s W i W i + 1 x W i W i + 1 F X + x s D n W i W i + 1 s lim W i + 1 = G W i W i + 1 lim W i + 1
667 665 666 eleqtrd φ n i 0 ..^ M L D n W i + 1 G W i W i + 1 lim W i + 1
668 130 133 225 226 16 114 300 211 369 478 631 667 fourierdlem110 φ n π - X - X π - X - X G x dx = - π - X π X G x dx
669 668 eqcomd φ n - π - X π X G x dx = π - X - X π - X - X G x dx
670 129 recnd φ - π - X
671 670 154 subnegd φ π - X - X