Metamath Proof Explorer


Theorem fourierdlem93

Description: Integral by substitution (the domain is shifted by X ) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem93.1 P = m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1
fourierdlem93.2 H = i 0 M Q i X
fourierdlem93.3 φ M
fourierdlem93.4 φ Q P M
fourierdlem93.5 φ X
fourierdlem93.6 φ F : π π
fourierdlem93.7 φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem93.8 φ i 0 ..^ M R F Q i Q i + 1 lim Q i
fourierdlem93.9 φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
Assertion fourierdlem93 φ π π F t dt = - π - X π X F X + s ds

Proof

Step Hyp Ref Expression
1 fourierdlem93.1 P = m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1
2 fourierdlem93.2 H = i 0 M Q i X
3 fourierdlem93.3 φ M
4 fourierdlem93.4 φ Q P M
5 fourierdlem93.5 φ X
6 fourierdlem93.6 φ F : π π
7 fourierdlem93.7 φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
8 fourierdlem93.8 φ i 0 ..^ M R F Q i Q i + 1 lim Q i
9 fourierdlem93.9 φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
10 1 fourierdlem2 M Q P M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
11 3 10 syl φ Q P M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
12 4 11 mpbid φ Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
13 12 simprd φ Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
14 13 simplld φ Q 0 = π
15 14 eqcomd φ π = Q 0
16 13 simplrd φ Q M = π
17 16 eqcomd φ π = Q M
18 15 17 oveq12d φ π π = Q 0 Q M
19 18 itgeq1d φ π π F t dt = Q 0 Q M F t dt
20 0zd φ 0
21 nnuz = 1
22 3 21 eleqtrdi φ M 1
23 1e0p1 1 = 0 + 1
24 23 a1i φ 1 = 0 + 1
25 24 fveq2d φ 1 = 0 + 1
26 22 25 eleqtrd φ M 0 + 1
27 1 3 4 fourierdlem15 φ Q : 0 M π π
28 pire π
29 28 renegcli π
30 iccssre π π π π
31 29 28 30 mp2an π π
32 31 a1i φ π π
33 27 32 fssd φ Q : 0 M
34 13 simprd φ i 0 ..^ M Q i < Q i + 1
35 34 r19.21bi φ i 0 ..^ M Q i < Q i + 1
36 6 adantr φ t Q 0 Q M F : π π
37 simpr φ t Q 0 Q M t Q 0 Q M
38 18 eqcomd φ Q 0 Q M = π π
39 38 adantr φ t Q 0 Q M Q 0 Q M = π π
40 37 39 eleqtrd φ t Q 0 Q M t π π
41 36 40 ffvelrnd φ t Q 0 Q M F t
42 33 adantr φ i 0 ..^ M Q : 0 M
43 elfzofz i 0 ..^ M i 0 M
44 43 adantl φ i 0 ..^ M i 0 M
45 42 44 ffvelrnd φ i 0 ..^ M Q i
46 fzofzp1 i 0 ..^ M i + 1 0 M
47 46 adantl φ i 0 ..^ M i + 1 0 M
48 42 47 ffvelrnd φ i 0 ..^ M Q i + 1
49 6 feqmptd φ F = t π π F t
50 49 adantr φ i 0 ..^ M F = t π π F t
51 50 reseq1d φ i 0 ..^ M F Q i Q i + 1 = t π π F t Q i Q i + 1
52 ioossicc Q i Q i + 1 Q i Q i + 1
53 52 a1i φ i 0 ..^ M Q i Q i + 1 Q i Q i + 1
54 29 rexri π *
55 54 a1i φ i 0 ..^ M t Q i Q i + 1 π *
56 28 rexri π *
57 56 a1i φ i 0 ..^ M t Q i Q i + 1 π *
58 27 ad2antrr φ i 0 ..^ M t Q i Q i + 1 Q : 0 M π π
59 simplr φ i 0 ..^ M t Q i Q i + 1 i 0 ..^ M
60 simpr φ i 0 ..^ M t Q i Q i + 1 t Q i Q i + 1
61 55 57 58 59 60 fourierdlem1 φ i 0 ..^ M t Q i Q i + 1 t π π
62 61 ralrimiva φ i 0 ..^ M t Q i Q i + 1 t π π
63 dfss3 Q i Q i + 1 π π t Q i Q i + 1 t π π
64 62 63 sylibr φ i 0 ..^ M Q i Q i + 1 π π
65 53 64 sstrd φ i 0 ..^ M Q i Q i + 1 π π
66 65 resmptd φ i 0 ..^ M t π π F t Q i Q i + 1 = t Q i Q i + 1 F t
67 51 66 eqtrd φ i 0 ..^ M F Q i Q i + 1 = t Q i Q i + 1 F t
68 67 eqcomd φ i 0 ..^ M t Q i Q i + 1 F t = F Q i Q i + 1
69 68 7 eqeltrd φ i 0 ..^ M t Q i Q i + 1 F t : Q i Q i + 1 cn
70 67 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1 = t Q i Q i + 1 F t lim Q i + 1
71 9 70 eleqtrd φ i 0 ..^ M L t Q i Q i + 1 F t lim Q i + 1
72 67 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i = t Q i Q i + 1 F t lim Q i
73 8 72 eleqtrd φ i 0 ..^ M R t Q i Q i + 1 F t lim Q i
74 45 48 69 71 73 iblcncfioo φ i 0 ..^ M t Q i Q i + 1 F t 𝐿 1
75 6 ad2antrr φ i 0 ..^ M t Q i Q i + 1 F : π π
76 75 61 ffvelrnd φ i 0 ..^ M t Q i Q i + 1 F t
77 45 48 74 76 ibliooicc φ i 0 ..^ M t Q i Q i + 1 F t 𝐿 1
78 20 26 33 35 41 77 itgspltprt φ Q 0 Q M F t dt = i 0 ..^ M Q i Q i + 1 F t dt
79 fvres t Q i Q i + 1 F Q i Q i + 1 t = F t
80 79 eqcomd t Q i Q i + 1 F t = F Q i Q i + 1 t
81 80 adantl φ i 0 ..^ M t Q i Q i + 1 F t = F Q i Q i + 1 t
82 81 itgeq2dv φ i 0 ..^ M Q i Q i + 1 F t dt = Q i Q i + 1 F Q i Q i + 1 t dt
83 eqid x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F Q i Q i + 1 Q i Q i + 1 x = x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F Q i Q i + 1 Q i Q i + 1 x
84 6 adantr φ i 0 ..^ M F : π π
85 84 64 fssresd φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
86 53 resabs1d φ i 0 ..^ M F Q i Q i + 1 Q i Q i + 1 = F Q i Q i + 1
87 86 7 eqeltrd φ i 0 ..^ M F Q i Q i + 1 Q i Q i + 1 : Q i Q i + 1 cn
88 86 oveq1d φ i 0 ..^ M F Q i Q i + 1 Q i Q i + 1 lim Q i + 1 = F Q i Q i + 1 lim Q i + 1
89 45 48 35 85 limcicciooub φ i 0 ..^ M F Q i Q i + 1 Q i Q i + 1 lim Q i + 1 = F Q i Q i + 1 lim Q i + 1
90 88 89 eqtr3d φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1 = F Q i Q i + 1 lim Q i + 1
91 9 90 eleqtrd φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
92 86 eqcomd φ i 0 ..^ M F Q i Q i + 1 = F Q i Q i + 1 Q i Q i + 1
93 92 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i = F Q i Q i + 1 Q i Q i + 1 lim Q i
94 45 48 35 85 limciccioolb φ i 0 ..^ M F Q i Q i + 1 Q i Q i + 1 lim Q i = F Q i Q i + 1 lim Q i
95 93 94 eqtrd φ i 0 ..^ M F Q i Q i + 1 lim Q i = F Q i Q i + 1 lim Q i
96 8 95 eleqtrd φ i 0 ..^ M R F Q i Q i + 1 lim Q i
97 5 adantr φ i 0 ..^ M X
98 83 45 48 35 85 87 91 96 97 fourierdlem82 φ i 0 ..^ M Q i Q i + 1 F Q i Q i + 1 t dt = Q i X Q i + 1 X F Q i Q i + 1 X + t dt
99 45 adantr φ i 0 ..^ M t Q i X Q i + 1 X Q i
100 48 adantr φ i 0 ..^ M t Q i X Q i + 1 X Q i + 1
101 5 ad2antrr φ i 0 ..^ M t Q i X Q i + 1 X X
102 99 101 resubcld φ i 0 ..^ M t Q i X Q i + 1 X Q i X
103 100 101 resubcld φ i 0 ..^ M t Q i X Q i + 1 X Q i + 1 X
104 simpr φ i 0 ..^ M t Q i X Q i + 1 X t Q i X Q i + 1 X
105 eliccre Q i X Q i + 1 X t Q i X Q i + 1 X t
106 102 103 104 105 syl3anc φ i 0 ..^ M t Q i X Q i + 1 X t
107 101 106 readdcld φ i 0 ..^ M t Q i X Q i + 1 X X + t
108 elicc2 Q i X Q i + 1 X t Q i X Q i + 1 X t Q i X t t Q i + 1 X
109 102 103 108 syl2anc φ i 0 ..^ M t Q i X Q i + 1 X t Q i X Q i + 1 X t Q i X t t Q i + 1 X
110 104 109 mpbid φ i 0 ..^ M t Q i X Q i + 1 X t Q i X t t Q i + 1 X
111 110 simp2d φ i 0 ..^ M t Q i X Q i + 1 X Q i X t
112 99 101 106 lesubadd2d φ i 0 ..^ M t Q i X Q i + 1 X Q i X t Q i X + t
113 111 112 mpbid φ i 0 ..^ M t Q i X Q i + 1 X Q i X + t
114 110 simp3d φ i 0 ..^ M t Q i X Q i + 1 X t Q i + 1 X
115 101 106 100 leaddsub2d φ i 0 ..^ M t Q i X Q i + 1 X X + t Q i + 1 t Q i + 1 X
116 114 115 mpbird φ i 0 ..^ M t Q i X Q i + 1 X X + t Q i + 1
117 99 100 107 113 116 eliccd φ i 0 ..^ M t Q i X Q i + 1 X X + t Q i Q i + 1
118 fvres X + t Q i Q i + 1 F Q i Q i + 1 X + t = F X + t
119 117 118 syl φ i 0 ..^ M t Q i X Q i + 1 X F Q i Q i + 1 X + t = F X + t
120 119 itgeq2dv φ i 0 ..^ M Q i X Q i + 1 X F Q i Q i + 1 X + t dt = Q i X Q i + 1 X F X + t dt
121 82 98 120 3eqtrd φ i 0 ..^ M Q i Q i + 1 F t dt = Q i X Q i + 1 X F X + t dt
122 121 sumeq2dv φ i 0 ..^ M Q i Q i + 1 F t dt = i 0 ..^ M Q i X Q i + 1 X F X + t dt
123 oveq2 s = t X + s = X + t
124 123 fveq2d s = t F X + s = F X + t
125 124 cbvitgv - π - X π X F X + s ds = - π - X π X F X + t dt
126 125 a1i φ - π - X π X F X + s ds = - π - X π X F X + t dt
127 2 a1i φ H = i 0 M Q i X
128 fveq2 i = 0 Q i = Q 0
129 128 oveq1d i = 0 Q i X = Q 0 X
130 129 adantl φ i = 0 Q i X = Q 0 X
131 3 nnzd φ M
132 0le0 0 0
133 132 a1i φ 0 0
134 0red φ 0
135 3 nnred φ M
136 3 nngt0d φ 0 < M
137 134 135 136 ltled φ 0 M
138 20 131 20 133 137 elfzd φ 0 0 M
139 14 29 eqeltrdi φ Q 0
140 139 5 resubcld φ Q 0 X
141 127 130 138 140 fvmptd φ H 0 = Q 0 X
142 14 oveq1d φ Q 0 X = - π - X
143 141 142 eqtr2d φ - π - X = H 0
144 fveq2 i = M Q i = Q M
145 144 oveq1d i = M Q i X = Q M X
146 145 adantl φ i = M Q i X = Q M X
147 135 leidd φ M M
148 20 131 131 137 147 elfzd φ M 0 M
149 16 28 eqeltrdi φ Q M
150 149 5 resubcld φ Q M X
151 127 146 148 150 fvmptd φ H M = Q M X
152 16 oveq1d φ Q M X = π X
153 151 152 eqtr2d φ π X = H M
154 143 153 oveq12d φ - π - X π X = H 0 H M
155 154 itgeq1d φ - π - X π X F X + t dt = H 0 H M F X + t dt
156 33 ffvelrnda φ i 0 M Q i
157 5 adantr φ i 0 M X
158 156 157 resubcld φ i 0 M Q i X
159 158 2 fmptd φ H : 0 M
160 45 48 97 35 ltsub1dd φ i 0 ..^ M Q i X < Q i + 1 X
161 44 158 syldan φ i 0 ..^ M Q i X
162 2 fvmpt2 i 0 M Q i X H i = Q i X
163 44 161 162 syl2anc φ i 0 ..^ M H i = Q i X
164 fveq2 i = j Q i = Q j
165 164 oveq1d i = j Q i X = Q j X
166 165 cbvmptv i 0 M Q i X = j 0 M Q j X
167 2 166 eqtri H = j 0 M Q j X
168 167 a1i φ i 0 ..^ M H = j 0 M Q j X
169 fveq2 j = i + 1 Q j = Q i + 1
170 169 oveq1d j = i + 1 Q j X = Q i + 1 X
171 170 adantl φ i 0 ..^ M j = i + 1 Q j X = Q i + 1 X
172 48 97 resubcld φ i 0 ..^ M Q i + 1 X
173 168 171 47 172 fvmptd φ i 0 ..^ M H i + 1 = Q i + 1 X
174 160 163 173 3brtr4d φ i 0 ..^ M H i < H i + 1
175 frn F : π π ran F
176 6 175 syl φ ran F
177 176 adantr φ t H 0 H M ran F
178 ffun F : π π Fun F
179 6 178 syl φ Fun F
180 179 adantr φ t H 0 H M Fun F
181 29 a1i φ t H 0 H M π
182 28 a1i φ t H 0 H M π
183 5 adantr φ t H 0 H M X
184 141 140 eqeltrd φ H 0
185 184 adantr φ t H 0 H M H 0
186 151 150 eqeltrd φ H M
187 186 adantr φ t H 0 H M H M
188 simpr φ t H 0 H M t H 0 H M
189 eliccre H 0 H M t H 0 H M t
190 185 187 188 189 syl3anc φ t H 0 H M t
191 183 190 readdcld φ t H 0 H M X + t
192 128 adantl φ i = 0 Q i = Q 0
193 192 oveq1d φ i = 0 Q i X = Q 0 X
194 127 193 138 140 fvmptd φ H 0 = Q 0 X
195 194 oveq2d φ X + H 0 = X + Q 0 - X
196 5 recnd φ X
197 139 recnd φ Q 0
198 196 197 pncan3d φ X + Q 0 - X = Q 0
199 195 198 14 3eqtrrd φ π = X + H 0
200 199 adantr φ t H 0 H M π = X + H 0
201 elicc2 H 0 H M t H 0 H M t H 0 t t H M
202 185 187 201 syl2anc φ t H 0 H M t H 0 H M t H 0 t t H M
203 188 202 mpbid φ t H 0 H M t H 0 t t H M
204 203 simp2d φ t H 0 H M H 0 t
205 185 190 183 204 leadd2dd φ t H 0 H M X + H 0 X + t
206 200 205 eqbrtrd φ t H 0 H M π X + t
207 203 simp3d φ t H 0 H M t H M
208 190 187 183 207 leadd2dd φ t H 0 H M X + t X + H M
209 151 oveq2d φ X + H M = X + Q M - X
210 149 recnd φ Q M
211 196 210 pncan3d φ X + Q M - X = Q M
212 209 211 16 3eqtrrd φ π = X + H M
213 212 adantr φ t H 0 H M π = X + H M
214 208 213 breqtrrd φ t H 0 H M X + t π
215 181 182 191 206 214 eliccd φ t H 0 H M X + t π π
216 fdm F : π π dom F = π π
217 6 216 syl φ dom F = π π
218 217 eqcomd φ π π = dom F
219 218 adantr φ t H 0 H M π π = dom F
220 215 219 eleqtrd φ t H 0 H M X + t dom F
221 fvelrn Fun F X + t dom F F X + t ran F
222 180 220 221 syl2anc φ t H 0 H M F X + t ran F
223 177 222 sseldd φ t H 0 H M F X + t
224 163 161 eqeltrd φ i 0 ..^ M H i
225 173 172 eqeltrd φ i 0 ..^ M H i + 1
226 84 65 fssresd φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
227 45 rexrd φ i 0 ..^ M Q i *
228 227 adantr φ i 0 ..^ M t H i H i + 1 Q i *
229 48 rexrd φ i 0 ..^ M Q i + 1 *
230 229 adantr φ i 0 ..^ M t H i H i + 1 Q i + 1 *
231 5 ad2antrr φ i 0 ..^ M t H i H i + 1 X
232 elioore t H i H i + 1 t
233 232 adantl φ i 0 ..^ M t H i H i + 1 t
234 231 233 readdcld φ i 0 ..^ M t H i H i + 1 X + t
235 163 oveq2d φ i 0 ..^ M X + H i = X + Q i - X
236 196 adantr φ i 0 ..^ M X
237 45 recnd φ i 0 ..^ M Q i
238 236 237 pncan3d φ i 0 ..^ M X + Q i - X = Q i
239 eqidd φ i 0 ..^ M Q i = Q i
240 235 238 239 3eqtrrd φ i 0 ..^ M Q i = X + H i
241 240 adantr φ i 0 ..^ M t H i H i + 1 Q i = X + H i
242 224 adantr φ i 0 ..^ M t H i H i + 1 H i
243 simpr φ i 0 ..^ M t H i H i + 1 t H i H i + 1
244 242 rexrd φ i 0 ..^ M t H i H i + 1 H i *
245 225 rexrd φ i 0 ..^ M H i + 1 *
246 245 adantr φ i 0 ..^ M t H i H i + 1 H i + 1 *
247 elioo2 H i * H i + 1 * t H i H i + 1 t H i < t t < H i + 1
248 244 246 247 syl2anc φ i 0 ..^ M t H i H i + 1 t H i H i + 1 t H i < t t < H i + 1
249 243 248 mpbid φ i 0 ..^ M t H i H i + 1 t H i < t t < H i + 1
250 249 simp2d φ i 0 ..^ M t H i H i + 1 H i < t
251 242 233 231 250 ltadd2dd φ i 0 ..^ M t H i H i + 1 X + H i < X + t
252 241 251 eqbrtrd φ i 0 ..^ M t H i H i + 1 Q i < X + t
253 225 adantr φ i 0 ..^ M t H i H i + 1 H i + 1
254 249 simp3d φ i 0 ..^ M t H i H i + 1 t < H i + 1
255 233 253 231 254 ltadd2dd φ i 0 ..^ M t H i H i + 1 X + t < X + H i + 1
256 173 oveq2d φ i 0 ..^ M X + H i + 1 = X + Q i + 1 - X
257 48 recnd φ i 0 ..^ M Q i + 1
258 236 257 pncan3d φ i 0 ..^ M X + Q i + 1 - X = Q i + 1
259 256 258 eqtrd φ i 0 ..^ M X + H i + 1 = Q i + 1
260 259 adantr φ i 0 ..^ M t H i H i + 1 X + H i + 1 = Q i + 1
261 255 260 breqtrd φ i 0 ..^ M t H i H i + 1 X + t < Q i + 1
262 228 230 234 252 261 eliood φ i 0 ..^ M t H i H i + 1 X + t Q i Q i + 1
263 eqid t H i H i + 1 X + t = t H i H i + 1 X + t
264 262 263 fmptd φ i 0 ..^ M t H i H i + 1 X + t : H i H i + 1 Q i Q i + 1
265 fcompt F Q i Q i + 1 : Q i Q i + 1 t H i H i + 1 X + t : H i H i + 1 Q i Q i + 1 F Q i Q i + 1 t H i H i + 1 X + t = s H i H i + 1 F Q i Q i + 1 t H i H i + 1 X + t s
266 226 264 265 syl2anc φ i 0 ..^ M F Q i Q i + 1 t H i H i + 1 X + t = s H i H i + 1 F Q i Q i + 1 t H i H i + 1 X + t s
267 oveq2 t = r X + t = X + r
268 267 cbvmptv t H i H i + 1 X + t = r H i H i + 1 X + r
269 268 fveq1i t H i H i + 1 X + t s = r H i H i + 1 X + r s
270 269 fveq2i F Q i Q i + 1 t H i H i + 1 X + t s = F Q i Q i + 1 r H i H i + 1 X + r s
271 270 mpteq2i s H i H i + 1 F Q i Q i + 1 t H i H i + 1 X + t s = s H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r s
272 271 a1i φ i 0 ..^ M s H i H i + 1 F Q i Q i + 1 t H i H i + 1 X + t s = s H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r s
273 fveq2 s = t r H i H i + 1 X + r s = r H i H i + 1 X + r t
274 273 fveq2d s = t F Q i Q i + 1 r H i H i + 1 X + r s = F Q i Q i + 1 r H i H i + 1 X + r t
275 274 cbvmptv s H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r s = t H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r t
276 275 a1i φ i 0 ..^ M s H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r s = t H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r t
277 eqidd φ i 0 ..^ M t H i H i + 1 r H i H i + 1 X + r = r H i H i + 1 X + r
278 oveq2 r = t X + r = X + t
279 278 adantl φ i 0 ..^ M t H i H i + 1 r = t X + r = X + t
280 277 279 243 234 fvmptd φ i 0 ..^ M t H i H i + 1 r H i H i + 1 X + r t = X + t
281 280 fveq2d φ i 0 ..^ M t H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r t = F Q i Q i + 1 X + t
282 fvres X + t Q i Q i + 1 F Q i Q i + 1 X + t = F X + t
283 262 282 syl φ i 0 ..^ M t H i H i + 1 F Q i Q i + 1 X + t = F X + t
284 281 283 eqtrd φ i 0 ..^ M t H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r t = F X + t
285 284 mpteq2dva φ i 0 ..^ M t H i H i + 1 F Q i Q i + 1 r H i H i + 1 X + r t = t H i H i + 1 F X + t
286 272 276 285 3eqtrd φ i 0 ..^ M s H i H i + 1 F Q i Q i + 1 t H i H i + 1 X + t s = t H i H i + 1 F X + t
287 266 286 eqtr2d φ i 0 ..^ M t H i H i + 1 F X + t = F Q i Q i + 1 t H i H i + 1 X + t
288 eqid t X + t = t X + t
289 ssid
290 289 a1i X
291 id X X
292 290 291 290 constcncfg X t X : cn
293 cncfmptid t t : cn
294 289 289 293 mp2an t t : cn
295 294 a1i X t t : cn
296 292 295 addcncf X t X + t : cn
297 236 296 syl φ i 0 ..^ M t X + t : cn
298 ioosscn H i H i + 1
299 298 a1i φ i 0 ..^ M H i H i + 1
300 ioosscn Q i Q i + 1
301 300 a1i φ i 0 ..^ M Q i Q i + 1
302 288 297 299 301 262 cncfmptssg φ i 0 ..^ M t H i H i + 1 X + t : H i H i + 1 cn Q i Q i + 1
303 302 7 cncfco φ i 0 ..^ M F Q i Q i + 1 t H i H i + 1 X + t : H i H i + 1 cn
304 287 303 eqeltrd φ i 0 ..^ M t H i H i + 1 F X + t : H i H i + 1 cn
305 227 adantr φ i 0 ..^ M r ran t H i H i + 1 X + t Q i *
306 229 adantr φ i 0 ..^ M r ran t H i H i + 1 X + t Q i + 1 *
307 simpr φ i 0 ..^ M r ran t H i H i + 1 X + t r ran t H i H i + 1 X + t
308 vex r V
309 263 elrnmpt r V r ran t H i H i + 1 X + t t H i H i + 1 r = X + t
310 308 309 ax-mp r ran t H i H i + 1 X + t t H i H i + 1 r = X + t
311 307 310 sylib φ i 0 ..^ M r ran t H i H i + 1 X + t t H i H i + 1 r = X + t
312 nfv t φ i 0 ..^ M
313 nfmpt1 _ t t H i H i + 1 X + t
314 313 nfrn _ t ran t H i H i + 1 X + t
315 314 nfcri t r ran t H i H i + 1 X + t
316 312 315 nfan t φ i 0 ..^ M r ran t H i H i + 1 X + t
317 nfv t r
318 simp3 φ t H i H i + 1 r = X + t r = X + t
319 5 3ad2ant1 φ t H i H i + 1 r = X + t X
320 232 3ad2ant2 φ t H i H i + 1 r = X + t t
321 319 320 readdcld φ t H i H i + 1 r = X + t X + t
322 318 321 eqeltrd φ t H i H i + 1 r = X + t r
323 322 3exp φ t H i H i + 1 r = X + t r
324 323 ad2antrr φ i 0 ..^ M r ran t H i H i + 1 X + t t H i H i + 1 r = X + t r
325 316 317 324 rexlimd φ i 0 ..^ M r ran t H i H i + 1 X + t t H i H i + 1 r = X + t r
326 311 325 mpd φ i 0 ..^ M r ran t H i H i + 1 X + t r
327 nfv t Q i < r
328 252 3adant3 φ i 0 ..^ M t H i H i + 1 r = X + t Q i < X + t
329 simp3 φ i 0 ..^ M t H i H i + 1 r = X + t r = X + t
330 328 329 breqtrrd φ i 0 ..^ M t H i H i + 1 r = X + t Q i < r
331 330 3exp φ i 0 ..^ M t H i H i + 1 r = X + t Q i < r
332 331 adantr φ i 0 ..^ M r ran t H i H i + 1 X + t t H i H i + 1 r = X + t Q i < r
333 316 327 332 rexlimd φ i 0 ..^ M r ran t H i H i + 1 X + t t H i H i + 1 r = X + t Q i < r
334 311 333 mpd φ i 0 ..^ M r ran t H i H i + 1 X + t Q i < r
335 nfv t r < Q i + 1
336 261 3adant3 φ i 0 ..^ M t H i H i + 1 r = X + t X + t < Q i + 1
337 329 336 eqbrtrd φ i 0 ..^ M t H i H i + 1 r = X + t r < Q i + 1
338 337 3exp φ i 0 ..^ M t H i H i + 1 r = X + t r < Q i + 1
339 338 adantr φ i 0 ..^ M r ran t H i H i + 1 X + t t H i H i + 1 r = X + t r < Q i + 1
340 316 335 339 rexlimd φ i 0 ..^ M r ran t H i H i + 1 X + t t H i H i + 1 r = X + t r < Q i + 1
341 311 340 mpd φ i 0 ..^ M r ran t H i H i + 1 X + t r < Q i + 1
342 305 306 326 334 341 eliood φ i 0 ..^ M r ran t H i H i + 1 X + t r Q i Q i + 1
343 217 ineq2d φ Q i Q i + 1 dom F = Q i Q i + 1 π π
344 343 adantr φ i 0 ..^ M Q i Q i + 1 dom F = Q i Q i + 1 π π
345 dmres dom F Q i Q i + 1 = Q i Q i + 1 dom F
346 345 a1i φ i 0 ..^ M dom F Q i Q i + 1 = Q i Q i + 1 dom F
347 dfss Q i Q i + 1 π π Q i Q i + 1 = Q i Q i + 1 π π
348 65 347 sylib φ i 0 ..^ M Q i Q i + 1 = Q i Q i + 1 π π
349 344 346 348 3eqtr4d φ i 0 ..^ M dom F Q i Q i + 1 = Q i Q i + 1
350 349 adantr φ i 0 ..^ M r ran t H i H i + 1 X + t dom F Q i Q i + 1 = Q i Q i + 1
351 342 350 eleqtrrd φ i 0 ..^ M r ran t H i H i + 1 X + t r dom F Q i Q i + 1
352 326 341 ltned φ i 0 ..^ M r ran t H i H i + 1 X + t r Q i + 1
353 352 neneqd φ i 0 ..^ M r ran t H i H i + 1 X + t ¬ r = Q i + 1
354 velsn r Q i + 1 r = Q i + 1
355 353 354 sylnibr φ i 0 ..^ M r ran t H i H i + 1 X + t ¬ r Q i + 1
356 351 355 eldifd φ i 0 ..^ M r ran t H i H i + 1 X + t r dom F Q i Q i + 1 Q i + 1
357 356 ralrimiva φ i 0 ..^ M r ran t H i H i + 1 X + t r dom F Q i Q i + 1 Q i + 1
358 dfss3 ran t H i H i + 1 X + t dom F Q i Q i + 1 Q i + 1 r ran t H i H i + 1 X + t r dom F Q i Q i + 1 Q i + 1
359 357 358 sylibr φ i 0 ..^ M ran t H i H i + 1 X + t dom F Q i Q i + 1 Q i + 1
360 eqid s X + s = s X + s
361 196 adantr φ s X
362 simpr φ s s
363 361 362 addcomd φ s X + s = s + X
364 363 mpteq2dva φ s X + s = s s + X
365 eqid s s + X = s s + X
366 365 addccncf X s s + X : cn
367 196 366 syl φ s s + X : cn
368 364 367 eqeltrd φ s X + s : cn
369 368 adantr φ i 0 ..^ M s X + s : cn
370 224 rexrd φ i 0 ..^ M H i *
371 iocssre H i * H i + 1 H i H i + 1
372 370 225 371 syl2anc φ i 0 ..^ M H i H i + 1
373 ax-resscn
374 372 373 sstrdi φ i 0 ..^ M H i H i + 1
375 289 a1i φ i 0 ..^ M
376 196 ad2antrr φ i 0 ..^ M s H i H i + 1 X
377 374 sselda φ i 0 ..^ M s H i H i + 1 s
378 376 377 addcld φ i 0 ..^ M s H i H i + 1 X + s
379 360 369 374 375 378 cncfmptssg φ i 0 ..^ M s H i H i + 1 X + s : H i H i + 1 cn
380 eqid TopOpen fld = TopOpen fld
381 eqid TopOpen fld 𝑡 H i H i + 1 = TopOpen fld 𝑡 H i H i + 1
382 380 cnfldtop TopOpen fld Top
383 unicntop = TopOpen fld
384 383 restid TopOpen fld Top TopOpen fld 𝑡 = TopOpen fld
385 382 384 ax-mp TopOpen fld 𝑡 = TopOpen fld
386 385 eqcomi TopOpen fld = TopOpen fld 𝑡
387 380 381 386 cncfcn H i H i + 1 H i H i + 1 cn = TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld
388 374 375 387 syl2anc φ i 0 ..^ M H i H i + 1 cn = TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld
389 379 388 eleqtrd φ i 0 ..^ M s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld
390 380 cnfldtopon TopOpen fld TopOn
391 390 a1i φ i 0 ..^ M TopOpen fld TopOn
392 resttopon TopOpen fld TopOn H i H i + 1 TopOpen fld 𝑡 H i H i + 1 TopOn H i H i + 1
393 391 374 392 syl2anc φ i 0 ..^ M TopOpen fld 𝑡 H i H i + 1 TopOn H i H i + 1
394 cncnp TopOpen fld 𝑡 H i H i + 1 TopOn H i H i + 1 TopOpen fld TopOn s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld s H i H i + 1 X + s : H i H i + 1 t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t
395 393 391 394 syl2anc φ i 0 ..^ M s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld s H i H i + 1 X + s : H i H i + 1 t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t
396 389 395 mpbid φ i 0 ..^ M s H i H i + 1 X + s : H i H i + 1 t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t
397 396 simprd φ i 0 ..^ M t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t
398 ubioc1 H i * H i + 1 * H i < H i + 1 H i + 1 H i H i + 1
399 370 245 174 398 syl3anc φ i 0 ..^ M H i + 1 H i H i + 1
400 fveq2 t = H i + 1 TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t = TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i + 1
401 400 eleq2d t = H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i + 1
402 401 rspccva t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t H i + 1 H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i + 1
403 397 399 402 syl2anc φ i 0 ..^ M s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i + 1
404 ioounsn H i * H i + 1 * H i < H i + 1 H i H i + 1 H i + 1 = H i H i + 1
405 370 245 174 404 syl3anc φ i 0 ..^ M H i H i + 1 H i + 1 = H i H i + 1
406 259 eqcomd φ i 0 ..^ M Q i + 1 = X + H i + 1
407 406 ad2antrr φ i 0 ..^ M s H i H i + 1 H i + 1 s = H i + 1 Q i + 1 = X + H i + 1
408 iftrue s = H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = Q i + 1
409 408 adantl φ i 0 ..^ M s H i H i + 1 H i + 1 s = H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = Q i + 1
410 oveq2 s = H i + 1 X + s = X + H i + 1
411 410 adantl φ i 0 ..^ M s H i H i + 1 H i + 1 s = H i + 1 X + s = X + H i + 1
412 407 409 411 3eqtr4d φ i 0 ..^ M s H i H i + 1 H i + 1 s = H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = X + s
413 iffalse ¬ s = H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = t H i H i + 1 X + t s
414 413 adantl φ i 0 ..^ M s H i H i + 1 H i + 1 ¬ s = H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = t H i H i + 1 X + t s
415 eqidd φ i 0 ..^ M s H i H i + 1 H i + 1 ¬ s = H i + 1 t H i H i + 1 X + t = t H i H i + 1 X + t
416 oveq2 t = s X + t = X + s
417 416 adantl φ i 0 ..^ M s H i H i + 1 H i + 1 ¬ s = H i + 1 t = s X + t = X + s
418 velsn s H i + 1 s = H i + 1
419 418 notbii ¬ s H i + 1 ¬ s = H i + 1
420 elun s H i H i + 1 H i + 1 s H i H i + 1 s H i + 1
421 420 biimpi s H i H i + 1 H i + 1 s H i H i + 1 s H i + 1
422 421 orcomd s H i H i + 1 H i + 1 s H i + 1 s H i H i + 1
423 422 ord s H i H i + 1 H i + 1 ¬ s H i + 1 s H i H i + 1
424 419 423 syl5bir s H i H i + 1 H i + 1 ¬ s = H i + 1 s H i H i + 1
425 424 imp s H i H i + 1 H i + 1 ¬ s = H i + 1 s H i H i + 1
426 425 adantll φ i 0 ..^ M s H i H i + 1 H i + 1 ¬ s = H i + 1 s H i H i + 1
427 5 ad2antrr φ i 0 ..^ M s H i H i + 1 H i + 1 X
428 elioore s H i H i + 1 s
429 428 adantl φ i 0 ..^ M s H i H i + 1 s
430 elsni s H i + 1 s = H i + 1
431 430 adantl φ i 0 ..^ M s H i + 1 s = H i + 1
432 225 adantr φ i 0 ..^ M s H i + 1 H i + 1
433 431 432 eqeltrd φ i 0 ..^ M s H i + 1 s
434 429 433 jaodan φ i 0 ..^ M s H i H i + 1 s H i + 1 s
435 420 434 sylan2b φ i 0 ..^ M s H i H i + 1 H i + 1 s
436 427 435 readdcld φ i 0 ..^ M s H i H i + 1 H i + 1 X + s
437 436 adantr φ i 0 ..^ M s H i H i + 1 H i + 1 ¬ s = H i + 1 X + s
438 415 417 426 437 fvmptd φ i 0 ..^ M s H i H i + 1 H i + 1 ¬ s = H i + 1 t H i H i + 1 X + t s = X + s
439 414 438 eqtrd φ i 0 ..^ M s H i H i + 1 H i + 1 ¬ s = H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = X + s
440 412 439 pm2.61dan φ i 0 ..^ M s H i H i + 1 H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = X + s
441 405 440 mpteq12dva φ i 0 ..^ M s H i H i + 1 H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = s H i H i + 1 X + s
442 405 oveq2d φ i 0 ..^ M TopOpen fld 𝑡 H i H i + 1 H i + 1 = TopOpen fld 𝑡 H i H i + 1
443 442 oveq1d φ i 0 ..^ M TopOpen fld 𝑡 H i H i + 1 H i + 1 CnP TopOpen fld = TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld
444 443 fveq1d φ i 0 ..^ M TopOpen fld 𝑡 H i H i + 1 H i + 1 CnP TopOpen fld H i + 1 = TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i + 1
445 403 441 444 3eltr4d φ i 0 ..^ M s H i H i + 1 H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s TopOpen fld 𝑡 H i H i + 1 H i + 1 CnP TopOpen fld H i + 1
446 eqid TopOpen fld 𝑡 H i H i + 1 H i + 1 = TopOpen fld 𝑡 H i H i + 1 H i + 1
447 eqid s H i H i + 1 H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s = s H i H i + 1 H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s
448 264 301 fssd φ i 0 ..^ M t H i H i + 1 X + t : H i H i + 1
449 225 recnd φ i 0 ..^ M H i + 1
450 446 380 447 448 299 449 ellimc φ i 0 ..^ M Q i + 1 t H i H i + 1 X + t lim H i + 1 s H i H i + 1 H i + 1 if s = H i + 1 Q i + 1 t H i H i + 1 X + t s TopOpen fld 𝑡 H i H i + 1 H i + 1 CnP TopOpen fld H i + 1
451 445 450 mpbird φ i 0 ..^ M Q i + 1 t H i H i + 1 X + t lim H i + 1
452 359 451 9 limccog φ i 0 ..^ M L F Q i Q i + 1 t H i H i + 1 X + t lim H i + 1
453 266 286 eqtrd φ i 0 ..^ M F Q i Q i + 1 t H i H i + 1 X + t = t H i H i + 1 F X + t
454 453 oveq1d φ i 0 ..^ M F Q i Q i + 1 t H i H i + 1 X + t lim H i + 1 = t H i H i + 1 F X + t lim H i + 1
455 452 454 eleqtrd φ i 0 ..^ M L t H i H i + 1 F X + t lim H i + 1
456 45 adantr φ i 0 ..^ M r ran t H i H i + 1 X + t Q i
457 456 334 gtned φ i 0 ..^ M r ran t H i H i + 1 X + t r Q i
458 457 neneqd φ i 0 ..^ M r ran t H i H i + 1 X + t ¬ r = Q i
459 velsn r Q i r = Q i
460 458 459 sylnibr φ i 0 ..^ M r ran t H i H i + 1 X + t ¬ r Q i
461 351 460 eldifd φ i 0 ..^ M r ran t H i H i + 1 X + t r dom F Q i Q i + 1 Q i
462 461 ralrimiva φ i 0 ..^ M r ran t H i H i + 1 X + t r dom F Q i Q i + 1 Q i
463 dfss3 ran t H i H i + 1 X + t dom F Q i Q i + 1 Q i r ran t H i H i + 1 X + t r dom F Q i Q i + 1 Q i
464 462 463 sylibr φ i 0 ..^ M ran t H i H i + 1 X + t dom F Q i Q i + 1 Q i
465 icossre H i H i + 1 * H i H i + 1
466 224 245 465 syl2anc φ i 0 ..^ M H i H i + 1
467 466 373 sstrdi φ i 0 ..^ M H i H i + 1
468 196 ad2antrr φ i 0 ..^ M s H i H i + 1 X
469 467 sselda φ i 0 ..^ M s H i H i + 1 s
470 468 469 addcld φ i 0 ..^ M s H i H i + 1 X + s
471 360 369 467 375 470 cncfmptssg φ i 0 ..^ M s H i H i + 1 X + s : H i H i + 1 cn
472 eqid TopOpen fld 𝑡 H i H i + 1 = TopOpen fld 𝑡 H i H i + 1
473 380 472 386 cncfcn H i H i + 1 H i H i + 1 cn = TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld
474 467 375 473 syl2anc φ i 0 ..^ M H i H i + 1 cn = TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld
475 471 474 eleqtrd φ i 0 ..^ M s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld
476 resttopon TopOpen fld TopOn H i H i + 1 TopOpen fld 𝑡 H i H i + 1 TopOn H i H i + 1
477 391 467 476 syl2anc φ i 0 ..^ M TopOpen fld 𝑡 H i H i + 1 TopOn H i H i + 1
478 cncnp TopOpen fld 𝑡 H i H i + 1 TopOn H i H i + 1 TopOpen fld TopOn s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld s H i H i + 1 X + s : H i H i + 1 t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t
479 477 391 478 syl2anc φ i 0 ..^ M s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 Cn TopOpen fld s H i H i + 1 X + s : H i H i + 1 t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t
480 475 479 mpbid φ i 0 ..^ M s H i H i + 1 X + s : H i H i + 1 t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t
481 480 simprd φ i 0 ..^ M t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t
482 lbico1 H i * H i + 1 * H i < H i + 1 H i H i H i + 1
483 370 245 174 482 syl3anc φ i 0 ..^ M H i H i H i + 1
484 fveq2 t = H i TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t = TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i
485 484 eleq2d t = H i s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i
486 485 rspccva t H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld t H i H i H i + 1 s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i
487 481 483 486 syl2anc φ i 0 ..^ M s H i H i + 1 X + s TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i
488 uncom H i H i + 1 H i = H i H i H i + 1
489 snunioo H i * H i + 1 * H i < H i + 1 H i H i H i + 1 = H i H i + 1
490 370 245 174 489 syl3anc φ i 0 ..^ M H i H i H i + 1 = H i H i + 1
491 488 490 syl5eq φ i 0 ..^ M H i H i + 1 H i = H i H i + 1
492 iftrue s = H i if s = H i Q i t H i H i + 1 X + t s = Q i
493 492 adantl φ i 0 ..^ M s = H i if s = H i Q i t H i H i + 1 X + t s = Q i
494 240 adantr φ i 0 ..^ M s = H i Q i = X + H i
495 oveq2 s = H i X + s = X + H i
496 495 eqcomd s = H i X + H i = X + s
497 496 adantl φ i 0 ..^ M s = H i X + H i = X + s
498 493 494 497 3eqtrd φ i 0 ..^ M s = H i if s = H i Q i t H i H i + 1 X + t s = X + s
499 498 adantlr φ i 0 ..^ M s H i H i + 1 H i s = H i if s = H i Q i t H i H i + 1 X + t s = X + s
500 iffalse ¬ s = H i if s = H i Q i t H i H i + 1 X + t s = t H i H i + 1 X + t s
501 500 adantl φ i 0 ..^ M s H i H i + 1 H i ¬ s = H i if s = H i Q i t H i H i + 1 X + t s = t H i H i + 1 X + t s
502 eqidd φ i 0 ..^ M s H i H i + 1 H i ¬ s = H i t H i H i + 1 X + t = t H i H i + 1 X + t
503 416 adantl φ i 0 ..^ M s H i H i + 1 H i ¬ s = H i t = s X + t = X + s
504 velsn s H i s = H i
505 504 notbii ¬ s H i ¬ s = H i
506 elun s H i H i + 1 H i s H i H i + 1 s H i
507 506 biimpi s H i H i + 1 H i s H i H i + 1 s H i
508 507 orcomd s H i H i + 1 H i s H i s H i H i + 1
509 508 ord s H i H i + 1 H i ¬ s H i s H i H i + 1
510 505 509 syl5bir s H i H i + 1 H i ¬ s = H i s H i H i + 1
511 510 imp s H i H i + 1 H i ¬ s = H i s H i H i + 1
512 511 adantll φ i 0 ..^ M s H i H i + 1 H i ¬ s = H i s H i H i + 1
513 5 ad2antrr φ i 0 ..^ M s H i H i + 1 H i X
514 elsni s H i s = H i
515 514 adantl φ i 0 ..^ M s H i s = H i
516 224 adantr φ i 0 ..^ M s H i H i
517 515 516 eqeltrd φ i 0 ..^ M s H i s
518 429 517 jaodan φ i 0 ..^ M s H i H i + 1 s H i s
519 506 518 sylan2b φ i 0 ..^ M s H i H i + 1 H i s
520 513 519 readdcld φ i 0 ..^ M s H i H i + 1 H i X + s
521 520 adantr φ i 0 ..^ M s H i H i + 1 H i ¬ s = H i X + s
522 502 503 512 521 fvmptd φ i 0 ..^ M s H i H i + 1 H i ¬ s = H i t H i H i + 1 X + t s = X + s
523 501 522 eqtrd φ i 0 ..^ M s H i H i + 1 H i ¬ s = H i if s = H i Q i t H i H i + 1 X + t s = X + s
524 499 523 pm2.61dan φ i 0 ..^ M s H i H i + 1 H i if s = H i Q i t H i H i + 1 X + t s = X + s
525 491 524 mpteq12dva φ i 0 ..^ M s H i H i + 1 H i if s = H i Q i t H i H i + 1 X + t s = s H i H i + 1 X + s
526 491 oveq2d φ i 0 ..^ M TopOpen fld 𝑡 H i H i + 1 H i = TopOpen fld 𝑡 H i H i + 1
527 526 oveq1d φ i 0 ..^ M TopOpen fld 𝑡 H i H i + 1 H i CnP TopOpen fld = TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld
528 527 fveq1d φ i 0 ..^ M TopOpen fld 𝑡 H i H i + 1 H i CnP TopOpen fld H i = TopOpen fld 𝑡 H i H i + 1 CnP TopOpen fld H i
529 487 525 528 3eltr4d φ i 0 ..^ M s H i H i + 1 H i if s = H i Q i t H i H i + 1 X + t s TopOpen fld 𝑡 H i H i + 1 H i CnP TopOpen fld H i
530 eqid TopOpen fld 𝑡 H i H i + 1 H i = TopOpen fld 𝑡 H i H i + 1 H i
531 eqid s H i H i + 1 H i if s = H i Q i t H i H i + 1 X + t s = s H i H i + 1 H i if s = H i Q i t H i H i + 1 X + t s
532 224 recnd φ i 0 ..^ M H i
533 530 380 531 448 299 532 ellimc φ i 0 ..^ M Q i t H i H i + 1 X + t lim H i s H i H i + 1 H i if s = H i Q i t H i H i + 1 X + t s TopOpen fld 𝑡 H i H i + 1 H i CnP TopOpen fld H i
534 529 533 mpbird φ i 0 ..^ M Q i t H i H i + 1 X + t lim H i
535 464 534 8 limccog φ i 0 ..^ M R F Q i Q i + 1 t H i H i + 1 X + t lim H i
536 453 oveq1d φ i 0 ..^ M F Q i Q i + 1 t H i H i + 1 X + t lim H i = t H i H i + 1 F X + t lim H i
537 535 536 eleqtrd φ i 0 ..^ M R t H i H i + 1 F X + t lim H i
538 224 225 304 455 537 iblcncfioo φ i 0 ..^ M t H i H i + 1 F X + t 𝐿 1
539 6 ad2antrr φ i 0 ..^ M t H i H i + 1 F : π π
540 54 a1i φ i 0 ..^ M t H i H i + 1 π *
541 56 a1i φ i 0 ..^ M t H i H i + 1 π *
542 27 ad2antrr φ i 0 ..^ M t H i H i + 1 Q : 0 M π π
543 simplr φ i 0 ..^ M t H i H i + 1 i 0 ..^ M
544 simpr φ i 0 ..^ M t H i H i + 1 t H i H i + 1
545 163 173 oveq12d φ i 0 ..^ M H i H i + 1 = Q i X Q i + 1 X
546 545 adantr φ i 0 ..^ M t H i H i + 1 H i H i + 1 = Q i X Q i + 1 X
547 544 546 eleqtrd φ i 0 ..^ M t H i H i + 1 t Q i X Q i + 1 X
548 547 117 syldan φ i 0 ..^ M t H i H i + 1 X + t Q i Q i + 1
549 540 541 542 543 548 fourierdlem1 φ i 0 ..^ M t H i H i + 1 X + t π π
550 539 549 ffvelrnd φ i 0 ..^ M t H i H i + 1 F X + t
551 224 225 538 550 ibliooicc φ i 0 ..^ M t H i H i + 1 F X + t 𝐿 1
552 20 26 159 174 223 551 itgspltprt φ H 0 H M F X + t dt = i 0 ..^ M H i H i + 1 F X + t dt
553 545 itgeq1d φ i 0 ..^ M H i H i + 1 F X + t dt = Q i X Q i + 1 X F X + t dt
554 553 sumeq2dv φ i 0 ..^ M H i H i + 1 F X + t dt = i 0 ..^ M Q i X Q i + 1 X F X + t dt
555 552 554 eqtrd φ H 0 H M F X + t dt = i 0 ..^ M Q i X Q i + 1 X F X + t dt
556 126 155 555 3eqtrd φ - π - X π X F X + s ds = i 0 ..^ M Q i X Q i + 1 X F X + t dt
557 122 556 eqtr4d φ i 0 ..^ M Q i Q i + 1 F t dt = - π - X π X F X + s ds
558 19 78 557 3eqtrd φ π π F t dt = - π - X π X F X + s ds