Metamath Proof Explorer


Theorem dirkercncflem2

Description: Lemma used to prove that the Dirichlet Kernel is continuous at Y points that are multiples of ( 2 x. _pi ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkercncflem2.d D = n y if y mod 2 π = 0 2 n + 1 2 π sin n + 1 2 y 2 π sin y 2
dirkercncflem2.f F = y A B Y sin N + 1 2 y
dirkercncflem2.g G = y A B Y 2 π sin y 2
dirkercncflem2.yne0 φ y A B Y sin y 2 0
dirkercncflem2.h H = y A B Y N + 1 2 cos N + 1 2 y
dirkercncflem2.i I = y A B Y π cos y 2
dirkercncflem2.l L = w A B N + 1 2 cos N + 1 2 w π cos w 2
dirkercncflem2.n φ N
dirkercncflem2.y φ Y A B
dirkercncflem2.ymod φ Y mod 2 π = 0
dirkercncflem2.11 φ y A B Y cos y 2 0
Assertion dirkercncflem2 φ D N Y D N A B Y lim Y

Proof

Step Hyp Ref Expression
1 dirkercncflem2.d D = n y if y mod 2 π = 0 2 n + 1 2 π sin n + 1 2 y 2 π sin y 2
2 dirkercncflem2.f F = y A B Y sin N + 1 2 y
3 dirkercncflem2.g G = y A B Y 2 π sin y 2
4 dirkercncflem2.yne0 φ y A B Y sin y 2 0
5 dirkercncflem2.h H = y A B Y N + 1 2 cos N + 1 2 y
6 dirkercncflem2.i I = y A B Y π cos y 2
7 dirkercncflem2.l L = w A B N + 1 2 cos N + 1 2 w π cos w 2
8 dirkercncflem2.n φ N
9 dirkercncflem2.y φ Y A B
10 dirkercncflem2.ymod φ Y mod 2 π = 0
11 dirkercncflem2.11 φ y A B Y cos y 2 0
12 difss A B Y A B
13 ioossre A B
14 12 13 sstri A B Y
15 14 a1i φ A B Y
16 8 adantr φ y A B Y N
17 16 nnred φ y A B Y N
18 halfre 1 2
19 18 a1i φ y A B Y 1 2
20 17 19 readdcld φ y A B Y N + 1 2
21 15 sselda φ y A B Y y
22 20 21 remulcld φ y A B Y N + 1 2 y
23 22 resincld φ y A B Y sin N + 1 2 y
24 23 2 fmptd φ F : A B Y
25 2re 2
26 pire π
27 25 26 remulcli 2 π
28 27 a1i φ y A B Y 2 π
29 21 rehalfcld φ y A B Y y 2
30 29 resincld φ y A B Y sin y 2
31 28 30 remulcld φ y A B Y 2 π sin y 2
32 31 3 fmptd φ G : A B Y
33 iooretop A B topGen ran .
34 33 a1i φ A B topGen ran .
35 eqid A B Y = A B Y
36 2 a1i φ F = y A B Y sin N + 1 2 y
37 36 oveq2d φ D F = dy A B Y sin N + 1 2 y d y
38 resmpt A B Y y sin N + 1 2 y A B Y = y A B Y sin N + 1 2 y
39 14 38 ax-mp y sin N + 1 2 y A B Y = y A B Y sin N + 1 2 y
40 39 eqcomi y A B Y sin N + 1 2 y = y sin N + 1 2 y A B Y
41 40 a1i φ y A B Y sin N + 1 2 y = y sin N + 1 2 y A B Y
42 41 oveq2d φ dy A B Y sin N + 1 2 y d y = D y sin N + 1 2 y A B Y
43 ax-resscn
44 43 a1i φ
45 8 nncnd φ N
46 halfcn 1 2
47 46 a1i φ 1 2
48 45 47 addcld φ N + 1 2
49 48 adantr φ y N + 1 2
50 44 sselda φ y y
51 49 50 mulcld φ y N + 1 2 y
52 51 sincld φ y sin N + 1 2 y
53 eqid y sin N + 1 2 y = y sin N + 1 2 y
54 52 53 fmptd φ y sin N + 1 2 y :
55 ssid
56 55 14 pm3.2i A B Y
57 56 a1i φ A B Y
58 eqid TopOpen fld = TopOpen fld
59 58 tgioo2 topGen ran . = TopOpen fld 𝑡
60 58 59 dvres y sin N + 1 2 y : A B Y D y sin N + 1 2 y A B Y = dy sin N + 1 2 y d y int topGen ran . A B Y
61 44 54 57 60 syl21anc φ D y sin N + 1 2 y A B Y = dy sin N + 1 2 y d y int topGen ran . A B Y
62 retop topGen ran . Top
63 rehaus topGen ran . Haus
64 9 elioored φ Y
65 uniretop = topGen ran .
66 65 sncld topGen ran . Haus Y Y Clsd topGen ran .
67 63 64 66 sylancr φ Y Clsd topGen ran .
68 65 difopn A B topGen ran . Y Clsd topGen ran . A B Y topGen ran .
69 33 67 68 sylancr φ A B Y topGen ran .
70 isopn3i topGen ran . Top A B Y topGen ran . int topGen ran . A B Y = A B Y
71 62 69 70 sylancr φ int topGen ran . A B Y = A B Y
72 71 reseq2d φ dy sin N + 1 2 y d y int topGen ran . A B Y = dy sin N + 1 2 y d y A B Y
73 reelprrecn
74 73 a1i φ
75 48 adantr φ y N + 1 2
76 simpr φ y y
77 75 76 mulcld φ y N + 1 2 y
78 77 sincld φ y sin N + 1 2 y
79 eqid y sin N + 1 2 y = y sin N + 1 2 y
80 78 79 fmptd φ y sin N + 1 2 y :
81 ssid
82 81 a1i φ
83 dvsinax N + 1 2 dy sin N + 1 2 y d y = y N + 1 2 cos N + 1 2 y
84 48 83 syl φ dy sin N + 1 2 y d y = y N + 1 2 cos N + 1 2 y
85 84 dmeqd φ dom dy sin N + 1 2 y d y = dom y N + 1 2 cos N + 1 2 y
86 eqid y N + 1 2 cos N + 1 2 y = y N + 1 2 cos N + 1 2 y
87 77 coscld φ y cos N + 1 2 y
88 75 87 mulcld φ y N + 1 2 cos N + 1 2 y
89 86 88 dmmptd φ dom y N + 1 2 cos N + 1 2 y =
90 85 89 eqtrd φ dom dy sin N + 1 2 y d y =
91 43 90 sseqtrrid φ dom dy sin N + 1 2 y d y
92 dvres3 y sin N + 1 2 y : dom dy sin N + 1 2 y d y D y sin N + 1 2 y = dy sin N + 1 2 y d y
93 74 80 82 91 92 syl22anc φ D y sin N + 1 2 y = dy sin N + 1 2 y d y
94 resmpt y sin N + 1 2 y = y sin N + 1 2 y
95 43 94 mp1i φ y sin N + 1 2 y = y sin N + 1 2 y
96 95 oveq2d φ D y sin N + 1 2 y = dy sin N + 1 2 y d y
97 84 reseq1d φ dy sin N + 1 2 y d y = y N + 1 2 cos N + 1 2 y
98 resmpt y N + 1 2 cos N + 1 2 y = y N + 1 2 cos N + 1 2 y
99 43 98 ax-mp y N + 1 2 cos N + 1 2 y = y N + 1 2 cos N + 1 2 y
100 97 99 eqtrdi φ dy sin N + 1 2 y d y = y N + 1 2 cos N + 1 2 y
101 93 96 100 3eqtr3d φ dy sin N + 1 2 y d y = y N + 1 2 cos N + 1 2 y
102 101 reseq1d φ dy sin N + 1 2 y d y A B Y = y N + 1 2 cos N + 1 2 y A B Y
103 resmpt A B Y y N + 1 2 cos N + 1 2 y A B Y = y A B Y N + 1 2 cos N + 1 2 y
104 14 103 mp1i φ y N + 1 2 cos N + 1 2 y A B Y = y A B Y N + 1 2 cos N + 1 2 y
105 72 102 104 3eqtrd φ dy sin N + 1 2 y d y int topGen ran . A B Y = y A B Y N + 1 2 cos N + 1 2 y
106 42 61 105 3eqtrd φ dy A B Y sin N + 1 2 y d y = y A B Y N + 1 2 cos N + 1 2 y
107 5 a1i φ H = y A B Y N + 1 2 cos N + 1 2 y
108 107 eqcomd φ y A B Y N + 1 2 cos N + 1 2 y = H
109 37 106 108 3eqtrd φ D F = H
110 109 dmeqd φ dom F = dom H
111 21 recnd φ y A B Y y
112 111 88 syldan φ y A B Y N + 1 2 cos N + 1 2 y
113 5 112 dmmptd φ dom H = A B Y
114 110 113 eqtr2d φ A B Y = dom F
115 eqimss A B Y = dom F A B Y dom F
116 114 115 syl φ A B Y dom F
117 6 a1i φ I = y A B Y π cos y 2
118 resmpt A B Y y 2 π sin y 2 A B Y = y A B Y 2 π sin y 2
119 14 118 ax-mp y 2 π sin y 2 A B Y = y A B Y 2 π sin y 2
120 119 eqcomi y A B Y 2 π sin y 2 = y 2 π sin y 2 A B Y
121 120 oveq2i dy A B Y 2 π sin y 2 d y = D y 2 π sin y 2 A B Y
122 121 a1i φ dy A B Y 2 π sin y 2 d y = D y 2 π sin y 2 A B Y
123 2cn 2
124 picn π
125 123 124 mulcli 2 π
126 125 a1i φ y 2 π
127 50 halfcld φ y y 2
128 127 sincld φ y sin y 2
129 126 128 mulcld φ y 2 π sin y 2
130 eqid y 2 π sin y 2 = y 2 π sin y 2
131 129 130 fmptd φ y 2 π sin y 2 :
132 58 59 dvres y 2 π sin y 2 : A B Y D y 2 π sin y 2 A B Y = dy 2 π sin y 2 d y int topGen ran . A B Y
133 44 131 57 132 syl21anc φ D y 2 π sin y 2 A B Y = dy 2 π sin y 2 d y int topGen ran . A B Y
134 71 reseq2d φ dy 2 π sin y 2 d y int topGen ran . A B Y = dy 2 π sin y 2 d y A B Y
135 43 sseli y y
136 1cnd y 1
137 2cnd y 2
138 id y y
139 2ne0 2 0
140 139 a1i y 2 0
141 136 137 138 140 div13d y 1 2 y = y 2 1
142 halfcl y y 2
143 142 mulid1d y y 2 1 = y 2
144 141 143 eqtrd y 1 2 y = y 2
145 144 fveq2d y sin 1 2 y = sin y 2
146 145 oveq2d y 2 π sin 1 2 y = 2 π sin y 2
147 146 eqcomd y 2 π sin y 2 = 2 π sin 1 2 y
148 135 147 syl y 2 π sin y 2 = 2 π sin 1 2 y
149 148 adantl φ y 2 π sin y 2 = 2 π sin 1 2 y
150 149 mpteq2dva φ y 2 π sin y 2 = y 2 π sin 1 2 y
151 150 oveq2d φ dy 2 π sin y 2 d y = dy 2 π sin 1 2 y d y
152 125 a1i φ y 2 π
153 46 a1i φ y 1 2
154 153 76 mulcld φ y 1 2 y
155 154 sincld φ y sin 1 2 y
156 152 155 mulcld φ y 2 π sin 1 2 y
157 eqid y 2 π sin 1 2 y = y 2 π sin 1 2 y
158 156 157 fmptd φ y 2 π sin 1 2 y :
159 2cnd φ 2
160 124 a1i φ π
161 159 160 mulcld φ 2 π
162 dvasinbx 2 π 1 2 dy 2 π sin 1 2 y d y = y 2 π 1 2 cos 1 2 y
163 161 46 162 sylancl φ dy 2 π sin 1 2 y d y = y 2 π 1 2 cos 1 2 y
164 2cnd φ y 2
165 124 a1i φ y π
166 164 165 153 mul32d φ y 2 π 1 2 = 2 1 2 π
167 139 a1i φ y 2 0
168 164 167 recidd φ y 2 1 2 = 1
169 168 oveq1d φ y 2 1 2 π = 1 π
170 165 mulid2d φ y 1 π = π
171 166 169 170 3eqtrd φ y 2 π 1 2 = π
172 144 fveq2d y cos 1 2 y = cos y 2
173 172 adantl φ y cos 1 2 y = cos y 2
174 171 173 oveq12d φ y 2 π 1 2 cos 1 2 y = π cos y 2
175 174 mpteq2dva φ y 2 π 1 2 cos 1 2 y = y π cos y 2
176 163 175 eqtrd φ dy 2 π sin 1 2 y d y = y π cos y 2
177 176 dmeqd φ dom dy 2 π sin 1 2 y d y = dom y π cos y 2
178 eqid y π cos y 2 = y π cos y 2
179 76 halfcld φ y y 2
180 179 coscld φ y cos y 2
181 165 180 mulcld φ y π cos y 2
182 178 181 dmmptd φ dom y π cos y 2 =
183 177 182 eqtrd φ dom dy 2 π sin 1 2 y d y =
184 43 183 sseqtrrid φ dom dy 2 π sin 1 2 y d y
185 dvres3 y 2 π sin 1 2 y : dom dy 2 π sin 1 2 y d y D y 2 π sin 1 2 y = dy 2 π sin 1 2 y d y
186 74 158 82 184 185 syl22anc φ D y 2 π sin 1 2 y = dy 2 π sin 1 2 y d y
187 resmpt y 2 π sin 1 2 y = y 2 π sin 1 2 y
188 43 187 mp1i φ y 2 π sin 1 2 y = y 2 π sin 1 2 y
189 188 oveq2d φ D y 2 π sin 1 2 y = dy 2 π sin 1 2 y d y
190 176 reseq1d φ dy 2 π sin 1 2 y d y = y π cos y 2
191 186 189 190 3eqtr3d φ dy 2 π sin 1 2 y d y = y π cos y 2
192 resmpt y π cos y 2 = y π cos y 2
193 43 192 ax-mp y π cos y 2 = y π cos y 2
194 191 193 eqtrdi φ dy 2 π sin 1 2 y d y = y π cos y 2
195 151 194 eqtrd φ dy 2 π sin y 2 d y = y π cos y 2
196 195 reseq1d φ dy 2 π sin y 2 d y A B Y = y π cos y 2 A B Y
197 15 resmptd φ y π cos y 2 A B Y = y A B Y π cos y 2
198 134 196 197 3eqtrd φ dy 2 π sin y 2 d y int topGen ran . A B Y = y A B Y π cos y 2
199 122 133 198 3eqtrd φ dy A B Y 2 π sin y 2 d y = y A B Y π cos y 2
200 199 eqcomd φ y A B Y π cos y 2 = dy A B Y 2 π sin y 2 d y
201 3 a1i φ G = y A B Y 2 π sin y 2
202 201 oveq2d φ D G = dy A B Y 2 π sin y 2 d y
203 202 eqcomd φ dy A B Y 2 π sin y 2 d y = D G
204 117 200 203 3eqtrrd φ D G = I
205 204 dmeqd φ dom G = dom I
206 111 181 syldan φ y A B Y π cos y 2
207 6 206 dmmptd φ dom I = A B Y
208 205 207 eqtr2d φ A B Y = dom G
209 eqimss A B Y = dom G A B Y dom G
210 208 209 syl φ A B Y dom G
211 111 77 syldan φ y A B Y N + 1 2 y
212 211 ralrimiva φ y A B Y N + 1 2 y
213 eqid y A B Y N + 1 2 y = y A B Y N + 1 2 y
214 213 fnmpt y A B Y N + 1 2 y y A B Y N + 1 2 y Fn A B Y
215 212 214 syl φ y A B Y N + 1 2 y Fn A B Y
216 eqidd φ w A B Y y A B Y N + 1 2 y = y A B Y N + 1 2 y
217 simpr φ w A B Y y = w y = w
218 217 oveq2d φ w A B Y y = w N + 1 2 y = N + 1 2 w
219 simpr φ w A B Y w A B Y
220 45 adantr φ w A B Y N
221 1cnd φ w A B Y 1
222 221 halfcld φ w A B Y 1 2
223 220 222 addcld φ w A B Y N + 1 2
224 eldifi w A B Y w A B
225 224 elioored w A B Y w
226 225 recnd w A B Y w
227 226 adantl φ w A B Y w
228 223 227 mulcld φ w A B Y N + 1 2 w
229 216 218 219 228 fvmptd φ w A B Y y A B Y N + 1 2 y w = N + 1 2 w
230 eleq1w y = w y A B Y w A B Y
231 230 anbi2d y = w φ y A B Y φ w A B Y
232 oveq1 y = w y mod 2 π = w mod 2 π
233 232 neeq1d y = w y mod 2 π 0 w mod 2 π 0
234 231 233 imbi12d y = w φ y A B Y y mod 2 π 0 φ w A B Y w mod 2 π 0
235 eldifi y A B Y y A B
236 elioore y A B y
237 235 236 135 3syl y A B Y y
238 2cnd y A B Y 2
239 124 a1i y A B Y π
240 139 a1i y A B Y 2 0
241 0re 0
242 pipos 0 < π
243 241 242 gtneii π 0
244 243 a1i y A B Y π 0
245 237 238 239 240 244 divdiv1d y A B Y y 2 π = y 2 π
246 245 eqcomd y A B Y y 2 π = y 2 π
247 246 adantl φ y A B Y y 2 π = y 2 π
248 4 neneqd φ y A B Y ¬ sin y 2 = 0
249 111 halfcld φ y A B Y y 2
250 sineq0 y 2 sin y 2 = 0 y 2 π
251 249 250 syl φ y A B Y sin y 2 = 0 y 2 π
252 248 251 mtbid φ y A B Y ¬ y 2 π
253 247 252 eqneltrd φ y A B Y ¬ y 2 π
254 2rp 2 +
255 pirp π +
256 rpmulcl 2 + π + 2 π +
257 254 255 256 mp2an 2 π +
258 mod0 y 2 π + y mod 2 π = 0 y 2 π
259 21 257 258 sylancl φ y A B Y y mod 2 π = 0 y 2 π
260 253 259 mtbird φ y A B Y ¬ y mod 2 π = 0
261 260 neqned φ y A B Y y mod 2 π 0
262 234 261 chvarvv φ w A B Y w mod 2 π 0
263 262 neneqd φ w A B Y ¬ w mod 2 π = 0
264 simpll φ w A B Y N + 1 2 w = N + 1 2 Y φ
265 simpr φ w A B Y N + 1 2 w = N + 1 2 Y N + 1 2 w = N + 1 2 Y
266 226 ad2antlr φ w A B Y N + 1 2 w = N + 1 2 Y w
267 64 recnd φ Y
268 267 ad2antrr φ w A B Y N + 1 2 w = N + 1 2 Y Y
269 0red φ 0
270 8 nnred φ N
271 1red φ 1
272 271 rehalfcld φ 1 2
273 270 272 readdcld φ N + 1 2
274 8 nngt0d φ 0 < N
275 254 a1i φ 2 +
276 275 rpreccld φ 1 2 +
277 270 276 ltaddrpd φ N < N + 1 2
278 269 270 273 274 277 lttrd φ 0 < N + 1 2
279 278 gt0ne0d φ N + 1 2 0
280 48 279 jca φ N + 1 2 N + 1 2 0
281 280 ad2antrr φ w A B Y N + 1 2 w = N + 1 2 Y N + 1 2 N + 1 2 0
282 mulcan w Y N + 1 2 N + 1 2 0 N + 1 2 w = N + 1 2 Y w = Y
283 266 268 281 282 syl3anc φ w A B Y N + 1 2 w = N + 1 2 Y N + 1 2 w = N + 1 2 Y w = Y
284 265 283 mpbid φ w A B Y N + 1 2 w = N + 1 2 Y w = Y
285 oveq1 w = Y w mod 2 π = Y mod 2 π
286 285 10 sylan9eqr φ w = Y w mod 2 π = 0
287 264 284 286 syl2anc φ w A B Y N + 1 2 w = N + 1 2 Y w mod 2 π = 0
288 263 287 mtand φ w A B Y ¬ N + 1 2 w = N + 1 2 Y
289 48 267 mulcld φ N + 1 2 Y
290 289 adantr φ w A B Y N + 1 2 Y
291 elsn2g N + 1 2 Y N + 1 2 w N + 1 2 Y N + 1 2 w = N + 1 2 Y
292 290 291 syl φ w A B Y N + 1 2 w N + 1 2 Y N + 1 2 w = N + 1 2 Y
293 288 292 mtbird φ w A B Y ¬ N + 1 2 w N + 1 2 Y
294 228 293 eldifd φ w A B Y N + 1 2 w N + 1 2 Y
295 229 294 eqeltrd φ w A B Y y A B Y N + 1 2 y w N + 1 2 Y
296 sinf sin :
297 296 fdmi dom sin =
298 297 eqcomi = dom sin
299 298 a1i φ w A B Y = dom sin
300 299 difeq1d φ w A B Y N + 1 2 Y = dom sin N + 1 2 Y
301 295 300 eleqtrd φ w A B Y y A B Y N + 1 2 y w dom sin N + 1 2 Y
302 301 ralrimiva φ w A B Y y A B Y N + 1 2 y w dom sin N + 1 2 Y
303 fnfvrnss y A B Y N + 1 2 y Fn A B Y w A B Y y A B Y N + 1 2 y w dom sin N + 1 2 Y ran y A B Y N + 1 2 y dom sin N + 1 2 Y
304 215 302 303 syl2anc φ ran y A B Y N + 1 2 y dom sin N + 1 2 Y
305 uncom A B Y Y = Y A B Y
306 305 a1i φ A B Y Y = Y A B Y
307 9 snssd φ Y A B
308 undif Y A B Y A B Y = A B
309 307 308 sylib φ Y A B Y = A B
310 306 309 eqtrd φ A B Y Y = A B
311 310 mpteq1d φ w A B Y Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w = w A B if w = Y N + 1 2 Y y A B Y N + 1 2 y w
312 iftrue w = Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w = N + 1 2 Y
313 oveq2 w = Y N + 1 2 w = N + 1 2 Y
314 312 313 eqtr4d w = Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w = N + 1 2 w
315 314 adantl φ w A B w = Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w = N + 1 2 w
316 iffalse ¬ w = Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w = y A B Y N + 1 2 y w
317 316 adantl φ w A B ¬ w = Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w = y A B Y N + 1 2 y w
318 eqidd φ w A B ¬ w = Y y A B Y N + 1 2 y = y A B Y N + 1 2 y
319 oveq2 y = w N + 1 2 y = N + 1 2 w
320 319 adantl φ w A B ¬ w = Y y = w N + 1 2 y = N + 1 2 w
321 simpl w A B ¬ w = Y w A B
322 id ¬ w = Y ¬ w = Y
323 velsn w Y w = Y
324 322 323 sylnibr ¬ w = Y ¬ w Y
325 324 adantl w A B ¬ w = Y ¬ w Y
326 321 325 eldifd w A B ¬ w = Y w A B Y
327 326 adantll φ w A B ¬ w = Y w A B Y
328 48 adantr φ w A B N + 1 2
329 elioore w A B w
330 329 recnd w A B w
331 330 adantl φ w A B w
332 328 331 mulcld φ w A B N + 1 2 w
333 332 adantr φ w A B ¬ w = Y N + 1 2 w
334 318 320 327 333 fvmptd φ w A B ¬ w = Y y A B Y N + 1 2 y w = N + 1 2 w
335 317 334 eqtrd φ w A B ¬ w = Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w = N + 1 2 w
336 315 335 pm2.61dan φ w A B if w = Y N + 1 2 Y y A B Y N + 1 2 y w = N + 1 2 w
337 336 mpteq2dva φ w A B if w = Y N + 1 2 Y y A B Y N + 1 2 y w = w A B N + 1 2 w
338 ioosscn A B
339 resmpt A B w N + 1 2 w A B = w A B N + 1 2 w
340 338 339 ax-mp w N + 1 2 w A B = w A B N + 1 2 w
341 eqid w N + 1 2 w = w N + 1 2 w
342 341 mulc1cncf N + 1 2 w N + 1 2 w : cn
343 48 342 syl φ w N + 1 2 w : cn
344 58 cnfldtop TopOpen fld Top
345 unicntop = TopOpen fld
346 345 restid TopOpen fld Top TopOpen fld 𝑡 = TopOpen fld
347 344 346 ax-mp TopOpen fld 𝑡 = TopOpen fld
348 347 eqcomi TopOpen fld = TopOpen fld 𝑡
349 58 348 348 cncfcn cn = TopOpen fld Cn TopOpen fld
350 81 82 349 sylancr φ cn = TopOpen fld Cn TopOpen fld
351 343 350 eleqtrd φ w N + 1 2 w TopOpen fld Cn TopOpen fld
352 13 44 sstrid φ A B
353 345 cnrest w N + 1 2 w TopOpen fld Cn TopOpen fld A B w N + 1 2 w A B TopOpen fld 𝑡 A B Cn TopOpen fld
354 351 352 353 syl2anc φ w N + 1 2 w A B TopOpen fld 𝑡 A B Cn TopOpen fld
355 340 354 eqeltrrid φ w A B N + 1 2 w TopOpen fld 𝑡 A B Cn TopOpen fld
356 58 cnfldtopon TopOpen fld TopOn
357 resttopon TopOpen fld TopOn A B TopOpen fld 𝑡 A B TopOn A B
358 356 352 357 sylancr φ TopOpen fld 𝑡 A B TopOn A B
359 cncnp TopOpen fld 𝑡 A B TopOn A B TopOpen fld TopOn w A B N + 1 2 w TopOpen fld 𝑡 A B Cn TopOpen fld w A B N + 1 2 w : A B y A B w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld y
360 358 356 359 sylancl φ w A B N + 1 2 w TopOpen fld 𝑡 A B Cn TopOpen fld w A B N + 1 2 w : A B y A B w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld y
361 355 360 mpbid φ w A B N + 1 2 w : A B y A B w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld y
362 361 simprd φ y A B w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld y
363 fveq2 y = Y TopOpen fld 𝑡 A B CnP TopOpen fld y = TopOpen fld 𝑡 A B CnP TopOpen fld Y
364 363 eleq2d y = Y w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld y w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld Y
365 364 rspccva y A B w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld y Y A B w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld Y
366 362 9 365 syl2anc φ w A B N + 1 2 w TopOpen fld 𝑡 A B CnP TopOpen fld Y
367 337 366 eqeltrd φ w A B if w = Y N + 1 2 Y y A B Y N + 1 2 y w TopOpen fld 𝑡 A B CnP TopOpen fld Y
368 310 eqcomd φ A B = A B Y Y
369 368 oveq2d φ TopOpen fld 𝑡 A B = TopOpen fld 𝑡 A B Y Y
370 369 oveq1d φ TopOpen fld 𝑡 A B CnP TopOpen fld = TopOpen fld 𝑡 A B Y Y CnP TopOpen fld
371 370 fveq1d φ TopOpen fld 𝑡 A B CnP TopOpen fld Y = TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y
372 367 371 eleqtrd φ w A B if w = Y N + 1 2 Y y A B Y N + 1 2 y w TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y
373 311 372 eqeltrd φ w A B Y Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y
374 eqid TopOpen fld 𝑡 A B Y Y = TopOpen fld 𝑡 A B Y Y
375 eqid w A B Y Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w = w A B Y Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w
376 211 213 fmptd φ y A B Y N + 1 2 y : A B Y
377 15 43 sstrdi φ A B Y
378 374 58 375 376 377 267 ellimc φ N + 1 2 Y y A B Y N + 1 2 y lim Y w A B Y Y if w = Y N + 1 2 Y y A B Y N + 1 2 y w TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y
379 373 378 mpbird φ N + 1 2 Y y A B Y N + 1 2 y lim Y
380 139 a1i φ 2 0
381 243 a1i φ π 0
382 159 160 380 381 mulne0d φ 2 π 0
383 267 161 382 divcan1d φ Y 2 π 2 π = Y
384 383 eqcomd φ Y = Y 2 π 2 π
385 384 oveq2d φ N + 1 2 Y = N + 1 2 Y 2 π 2 π
386 385 fveq2d φ sin N + 1 2 Y = sin N + 1 2 Y 2 π 2 π
387 267 161 382 divcld φ Y 2 π
388 48 387 161 mul12d φ N + 1 2 Y 2 π 2 π = Y 2 π N + 1 2 2 π
389 48 159 160 mulassd φ N + 1 2 2 π = N + 1 2 2 π
390 389 eqcomd φ N + 1 2 2 π = N + 1 2 2 π
391 390 oveq2d φ Y 2 π N + 1 2 2 π = Y 2 π N + 1 2 2 π
392 45 47 159 adddird φ N + 1 2 2 = N 2 + 1 2 2
393 159 380 recid2d φ 1 2 2 = 1
394 393 oveq2d φ N 2 + 1 2 2 = N 2 + 1
395 392 394 eqtrd φ N + 1 2 2 = N 2 + 1
396 395 oveq1d φ N + 1 2 2 π = N 2 + 1 π
397 396 oveq2d φ Y 2 π N + 1 2 2 π = Y 2 π N 2 + 1 π
398 388 391 397 3eqtrd φ N + 1 2 Y 2 π 2 π = Y 2 π N 2 + 1 π
399 45 159 mulcld φ N 2
400 1cnd φ 1
401 399 400 addcld φ N 2 + 1
402 387 401 160 mulassd φ Y 2 π N 2 + 1 π = Y 2 π N 2 + 1 π
403 398 402 eqtr4d φ N + 1 2 Y 2 π 2 π = Y 2 π N 2 + 1 π
404 403 fveq2d φ sin N + 1 2 Y 2 π 2 π = sin Y 2 π N 2 + 1 π
405 mod0 Y 2 π + Y mod 2 π = 0 Y 2 π
406 64 257 405 sylancl φ Y mod 2 π = 0 Y 2 π
407 10 406 mpbid φ Y 2 π
408 8 nnzd φ N
409 2z 2
410 409 a1i φ 2
411 408 410 zmulcld φ N 2
412 411 peano2zd φ N 2 + 1
413 407 412 zmulcld φ Y 2 π N 2 + 1
414 sinkpi Y 2 π N 2 + 1 sin Y 2 π N 2 + 1 π = 0
415 413 414 syl φ sin Y 2 π N 2 + 1 π = 0
416 386 404 415 3eqtrd φ sin N + 1 2 Y = 0
417 sincn sin : cn
418 417 a1i φ sin : cn
419 418 289 cnlimci φ sin N + 1 2 Y sin lim N + 1 2 Y
420 416 419 eqeltrrd φ 0 sin lim N + 1 2 Y
421 304 379 420 limccog φ 0 sin y A B Y N + 1 2 y lim Y
422 2 a1i φ w A B Y F = y A B Y sin N + 1 2 y
423 218 fveq2d φ w A B Y y = w sin N + 1 2 y = sin N + 1 2 w
424 228 sincld φ w A B Y sin N + 1 2 w
425 422 423 219 424 fvmptd φ w A B Y F w = sin N + 1 2 w
426 229 fveq2d φ w A B Y sin y A B Y N + 1 2 y w = sin N + 1 2 w
427 425 426 eqtr4d φ w A B Y F w = sin y A B Y N + 1 2 y w
428 427 mpteq2dva φ w A B Y F w = w A B Y sin y A B Y N + 1 2 y w
429 24 feqmptd φ F = w A B Y F w
430 fcompt sin : y A B Y N + 1 2 y : A B Y sin y A B Y N + 1 2 y = w A B Y sin y A B Y N + 1 2 y w
431 296 376 430 sylancr φ sin y A B Y N + 1 2 y = w A B Y sin y A B Y N + 1 2 y w
432 428 429 431 3eqtr4rd φ sin y A B Y N + 1 2 y = F
433 432 oveq1d φ sin y A B Y N + 1 2 y lim Y = F lim Y
434 421 433 eleqtrd φ 0 F lim Y
435 simpr φ w A B w = Y w = Y
436 435 iftrued φ w A B w = Y if w = Y 0 G w = 0
437 267 159 161 380 382 divdiv32d φ Y 2 2 π = Y 2 π 2
438 437 oveq1d φ Y 2 2 π 2 π = Y 2 π 2 2 π
439 267 halfcld φ Y 2
440 439 161 382 divcan1d φ Y 2 2 π 2 π = Y 2
441 387 159 161 380 div32d φ Y 2 π 2 2 π = Y 2 π 2 π 2
442 160 159 380 divcan3d φ 2 π 2 = π
443 442 oveq2d φ Y 2 π 2 π 2 = Y 2 π π
444 441 443 eqtrd φ Y 2 π 2 2 π = Y 2 π π
445 438 440 444 3eqtr3d φ Y 2 = Y 2 π π
446 445 fveq2d φ sin Y 2 = sin Y 2 π π
447 sinkpi Y 2 π sin Y 2 π π = 0
448 407 447 syl φ sin Y 2 π π = 0
449 446 448 eqtrd φ sin Y 2 = 0
450 449 oveq2d φ 2 π sin Y 2 = 2 π 0
451 161 mul01d φ 2 π 0 = 0
452 450 451 eqtrd φ 2 π sin Y 2 = 0
453 452 eqcomd φ 0 = 2 π sin Y 2
454 453 ad2antrr φ w A B w = Y 0 = 2 π sin Y 2
455 fvoveq1 w = Y sin w 2 = sin Y 2
456 455 oveq2d w = Y 2 π sin w 2 = 2 π sin Y 2
457 456 eqcomd w = Y 2 π sin Y 2 = 2 π sin w 2
458 457 adantl φ w A B w = Y 2 π sin Y 2 = 2 π sin w 2
459 436 454 458 3eqtrd φ w A B w = Y if w = Y 0 G w = 2 π sin w 2
460 iffalse ¬ w = Y if w = Y 0 G w = G w
461 460 adantl φ w A B ¬ w = Y if w = Y 0 G w = G w
462 fvoveq1 y = w sin y 2 = sin w 2
463 462 oveq2d y = w 2 π sin y 2 = 2 π sin w 2
464 125 a1i φ w A B 2 π
465 331 halfcld φ w A B w 2
466 465 sincld φ w A B sin w 2
467 464 466 mulcld φ w A B 2 π sin w 2
468 467 adantr φ w A B ¬ w = Y 2 π sin w 2
469 3 463 327 468 fvmptd3 φ w A B ¬ w = Y G w = 2 π sin w 2
470 461 469 eqtrd φ w A B ¬ w = Y if w = Y 0 G w = 2 π sin w 2
471 459 470 pm2.61dan φ w A B if w = Y 0 G w = 2 π sin w 2
472 471 mpteq2dva φ w A B if w = Y 0 G w = w A B 2 π sin w 2
473 eqid w 2 π sin w 2 = w 2 π sin w 2
474 82 161 82 constcncfg φ w 2 π : cn
475 id w w
476 2cnd w 2
477 139 a1i w 2 0
478 475 476 477 divrec2d w w 2 = 1 2 w
479 478 mpteq2ia w w 2 = w 1 2 w
480 eqid w 1 2 w = w 1 2 w
481 480 mulc1cncf 1 2 w 1 2 w : cn
482 46 481 ax-mp w 1 2 w : cn
483 479 482 eqeltri w w 2 : cn
484 483 a1i φ w w 2 : cn
485 418 484 cncfmpt1f φ w sin w 2 : cn
486 474 485 mulcncf φ w 2 π sin w 2 : cn
487 473 486 352 82 467 cncfmptssg φ w A B 2 π sin w 2 : A B cn
488 eqid TopOpen fld 𝑡 A B = TopOpen fld 𝑡 A B
489 58 488 348 cncfcn A B A B cn = TopOpen fld 𝑡 A B Cn TopOpen fld
490 352 81 489 sylancl φ A B cn = TopOpen fld 𝑡 A B Cn TopOpen fld
491 487 490 eleqtrd φ w A B 2 π sin w 2 TopOpen fld 𝑡 A B Cn TopOpen fld
492 cncnp TopOpen fld 𝑡 A B TopOn A B TopOpen fld TopOn w A B 2 π sin w 2 TopOpen fld 𝑡 A B Cn TopOpen fld w A B 2 π sin w 2 : A B y A B w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld y
493 358 356 492 sylancl φ w A B 2 π sin w 2 TopOpen fld 𝑡 A B Cn TopOpen fld w A B 2 π sin w 2 : A B y A B w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld y
494 491 493 mpbid φ w A B 2 π sin w 2 : A B y A B w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld y
495 494 simprd φ y A B w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld y
496 363 eleq2d y = Y w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld y w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld Y
497 496 rspccva y A B w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld y Y A B w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld Y
498 495 9 497 syl2anc φ w A B 2 π sin w 2 TopOpen fld 𝑡 A B CnP TopOpen fld Y
499 472 498 eqeltrd φ w A B if w = Y 0 G w TopOpen fld 𝑡 A B CnP TopOpen fld Y
500 310 mpteq1d φ w A B Y Y if w = Y 0 G w = w A B if w = Y 0 G w
501 369 eqcomd φ TopOpen fld 𝑡 A B Y Y = TopOpen fld 𝑡 A B
502 501 oveq1d φ TopOpen fld 𝑡 A B Y Y CnP TopOpen fld = TopOpen fld 𝑡 A B CnP TopOpen fld
503 502 fveq1d φ TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y = TopOpen fld 𝑡 A B CnP TopOpen fld Y
504 499 500 503 3eltr4d φ w A B Y Y if w = Y 0 G w TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y
505 eqid w A B Y Y if w = Y 0 G w = w A B Y Y if w = Y 0 G w
506 21 129 syldan φ y A B Y 2 π sin y 2
507 506 3 fmptd φ G : A B Y
508 374 58 505 507 377 267 ellimc φ 0 G lim Y w A B Y Y if w = Y 0 G w TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y
509 504 508 mpbird φ 0 G lim Y
510 260 nrexdv φ ¬ y A B Y y mod 2 π = 0
511 507 ffund φ Fun G
512 fvelima Fun G 0 G A B Y y A B Y G y = 0
513 511 512 sylan φ 0 G A B Y y A B Y G y = 0
514 2cnd φ y A B Y 2
515 124 a1i φ y A B Y π
516 139 a1i φ y A B Y 2 0
517 243 a1i φ y A B Y π 0
518 111 514 515 516 517 divdiv1d φ y A B Y y 2 π = y 2 π
519 518 eqcomd φ y A B Y y 2 π = y 2 π
520 519 adantr φ y A B Y G y = 0 y 2 π = y 2 π
521 2cnd y A B Y G y = 0 2
522 124 a1i y A B Y G y = 0 π
523 521 522 mulcld y A B Y G y = 0 2 π
524 237 adantr y A B Y G y = 0 y
525 524 halfcld y A B Y G y = 0 y 2
526 525 sincld y A B Y G y = 0 sin y 2
527 523 526 mulcld y A B Y G y = 0 2 π sin y 2
528 3 fvmpt2 y A B Y 2 π sin y 2 G y = 2 π sin y 2
529 527 528 syldan y A B Y G y = 0 G y = 2 π sin y 2
530 529 eqcomd y A B Y G y = 0 2 π sin y 2 = G y
531 simpr y A B Y G y = 0 G y = 0
532 530 531 eqtrd y A B Y G y = 0 2 π sin y 2 = 0
533 125 a1i y A B Y 2 π
534 237 halfcld y A B Y y 2
535 534 sincld y A B Y sin y 2
536 533 535 mul0ord y A B Y 2 π sin y 2 = 0 2 π = 0 sin y 2 = 0
537 536 adantr y A B Y G y = 0 2 π sin y 2 = 0 2 π = 0 sin y 2 = 0
538 532 537 mpbid y A B Y G y = 0 2 π = 0 sin y 2 = 0
539 2cnne0 2 2 0
540 124 243 pm3.2i π π 0
541 mulne0 2 2 0 π π 0 2 π 0
542 539 540 541 mp2an 2 π 0
543 542 neii ¬ 2 π = 0
544 pm2.53 2 π = 0 sin y 2 = 0 ¬ 2 π = 0 sin y 2 = 0
545 538 543 544 mpisyl y A B Y G y = 0 sin y 2 = 0
546 545 adantll φ y A B Y G y = 0 sin y 2 = 0
547 111 adantr φ y A B Y G y = 0 y
548 547 halfcld φ y A B Y G y = 0 y 2
549 548 250 syl φ y A B Y G y = 0 sin y 2 = 0 y 2 π
550 546 549 mpbid φ y A B Y G y = 0 y 2 π
551 520 550 eqeltrd φ y A B Y G y = 0 y 2 π
552 21 adantr φ y A B Y G y = 0 y
553 552 257 258 sylancl φ y A B Y G y = 0 y mod 2 π = 0 y 2 π
554 551 553 mpbird φ y A B Y G y = 0 y mod 2 π = 0
555 554 ex φ y A B Y G y = 0 y mod 2 π = 0
556 555 reximdva φ y A B Y G y = 0 y A B Y y mod 2 π = 0
557 556 adantr φ 0 G A B Y y A B Y G y = 0 y A B Y y mod 2 π = 0
558 513 557 mpd φ 0 G A B Y y A B Y y mod 2 π = 0
559 510 558 mtand φ ¬ 0 G A B Y
560 simpr φ y A B Y y A B Y
561 6 fvmpt2 y A B Y π cos y 2 I y = π cos y 2
562 560 206 561 syl2anc φ y A B Y I y = π cos y 2
563 534 coscld y A B Y cos y 2
564 563 adantl φ y A B Y cos y 2
565 515 564 517 11 mulne0d φ y A B Y π cos y 2 0
566 562 565 eqnetrd φ y A B Y I y 0
567 566 neneqd φ y A B Y ¬ I y = 0
568 567 nrexdv φ ¬ y A B Y I y = 0
569 206 6 fmptd φ I : A B Y
570 569 ffund φ Fun I
571 fvelima Fun I 0 I A B Y y A B Y I y = 0
572 570 571 sylan φ 0 I A B Y y A B Y I y = 0
573 568 572 mtand φ ¬ 0 I A B Y
574 204 imaeq1d φ G A B Y = I A B Y
575 573 574 neleqtrrd φ ¬ 0 G A B Y
576 1 dirkerval2 N Y D N Y = if Y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 Y 2 π sin Y 2
577 8 64 576 syl2anc φ D N Y = if Y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 Y 2 π sin Y 2
578 10 iftrued φ if Y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 Y 2 π sin Y 2 = 2 N + 1 2 π
579 7 a1i φ L = w A B N + 1 2 cos N + 1 2 w π cos w 2
580 iftrue w = Y if w = Y 2 N + 1 2 π y A B Y H y I y w = 2 N + 1 2 π
581 580 adantl φ w A B w = Y if w = Y 2 N + 1 2 π y A B Y H y I y w = 2 N + 1 2 π
582 159 45 mulcld φ 2 N
583 582 400 addcld φ 2 N + 1
584 583 159 160 380 381 divdiv1d φ 2 N + 1 2 π = 2 N + 1 2 π
585 584 eqcomd φ 2 N + 1 2 π = 2 N + 1 2 π
586 582 400 159 380 divdird φ 2 N + 1 2 = 2 N 2 + 1 2
587 45 159 380 divcan3d φ 2 N 2 = N
588 587 oveq1d φ 2 N 2 + 1 2 = N + 1 2
589 586 588 eqtrd φ 2 N + 1 2 = N + 1 2
590 589 oveq1d φ 2 N + 1 2 π = N + 1 2 π
591 585 590 eqtrd φ 2 N + 1 2 π = N + 1 2 π
592 591 ad2antrr φ w A B w = Y 2 N + 1 2 π = N + 1 2 π
593 313 fveq2d w = Y cos N + 1 2 w = cos N + 1 2 Y
594 593 oveq2d w = Y N + 1 2 cos N + 1 2 w = N + 1 2 cos N + 1 2 Y
595 fvoveq1 w = Y cos w 2 = cos Y 2
596 595 oveq2d w = Y π cos w 2 = π cos Y 2
597 594 596 oveq12d w = Y N + 1 2 cos N + 1 2 w π cos w 2 = N + 1 2 cos N + 1 2 Y π cos Y 2
598 597 adantl φ w A B w = Y N + 1 2 cos N + 1 2 w π cos w 2 = N + 1 2 cos N + 1 2 Y π cos Y 2
599 45 47 267 adddird φ N + 1 2 Y = N Y + 1 2 Y
600 400 159 267 380 div32d φ 1 2 Y = 1 Y 2
601 439 mulid2d φ 1 Y 2 = Y 2
602 600 601 eqtrd φ 1 2 Y = Y 2
603 602 oveq2d φ N Y + 1 2 Y = N Y + Y 2
604 45 267 mulcld φ N Y
605 604 439 addcomd φ N Y + Y 2 = Y 2 + N Y
606 599 603 605 3eqtrd φ N + 1 2 Y = Y 2 + N Y
607 606 fveq2d φ cos N + 1 2 Y = cos Y 2 + N Y
608 604 161 382 divcan1d φ N Y 2 π 2 π = N Y
609 608 eqcomd φ N Y = N Y 2 π 2 π
610 609 oveq2d φ Y 2 + N Y = Y 2 + N Y 2 π 2 π
611 610 fveq2d φ cos Y 2 + N Y = cos Y 2 + N Y 2 π 2 π
612 45 267 161 382 divassd φ N Y 2 π = N Y 2 π
613 408 407 zmulcld φ N Y 2 π
614 612 613 eqeltrd φ N Y 2 π
615 cosper Y 2 N Y 2 π cos Y 2 + N Y 2 π 2 π = cos Y 2
616 439 614 615 syl2anc φ cos Y 2 + N Y 2 π 2 π = cos Y 2
617 607 611 616 3eqtrd φ cos N + 1 2 Y = cos Y 2
618 617 oveq2d φ N + 1 2 cos N + 1 2 Y = N + 1 2 cos Y 2
619 618 oveq1d φ N + 1 2 cos N + 1 2 Y π cos Y 2 = N + 1 2 cos Y 2 π cos Y 2
620 439 coscld φ cos Y 2
621 267 159 160 380 381 divdiv1d φ Y 2 π = Y 2 π
622 621 407 eqeltrd φ Y 2 π
623 622 zred φ Y 2 π
624 623 276 ltaddrpd φ Y 2 π < Y 2 π + 1 2
625 halflt1 1 2 < 1
626 625 a1i φ 1 2 < 1
627 272 271 623 626 ltadd2dd φ Y 2 π + 1 2 < Y 2 π + 1
628 btwnnz Y 2 π Y 2 π < Y 2 π + 1 2 Y 2 π + 1 2 < Y 2 π + 1 ¬ Y 2 π + 1 2
629 622 624 627 628 syl3anc φ ¬ Y 2 π + 1 2
630 coseq0 Y 2 cos Y 2 = 0 Y 2 π + 1 2
631 439 630 syl φ cos Y 2 = 0 Y 2 π + 1 2
632 629 631 mtbird φ ¬ cos Y 2 = 0
633 632 neqned φ cos Y 2 0
634 48 160 620 381 633 divcan5rd φ N + 1 2 cos Y 2 π cos Y 2 = N + 1 2 π
635 619 634 eqtrd φ N + 1 2 cos N + 1 2 Y π cos Y 2 = N + 1 2 π
636 635 ad2antrr φ w A B w = Y N + 1 2 cos N + 1 2 Y π cos Y 2 = N + 1 2 π
637 598 636 eqtr2d φ w A B w = Y N + 1 2 π = N + 1 2 cos N + 1 2 w π cos w 2
638 581 592 637 3eqtrrd φ w A B w = Y N + 1 2 cos N + 1 2 w π cos w 2 = if w = Y 2 N + 1 2 π y A B Y H y I y w
639 iffalse ¬ w = Y if w = Y 2 N + 1 2 π y A B Y H y I y w = y A B Y H y I y w
640 639 adantl φ w A B ¬ w = Y if w = Y 2 N + 1 2 π y A B Y H y I y w = y A B Y H y I y w
641 eqidd φ w A B ¬ w = Y y A B Y H y I y = y A B Y H y I y
642 fveq2 y = w H y = H w
643 fveq2 y = w I y = I w
644 642 643 oveq12d y = w H y I y = H w I w
645 644 adantl φ w A B ¬ w = Y y = w H y I y = H w I w
646 112 5 fmptd φ H : A B Y
647 646 ad2antrr φ w A B ¬ w = Y H : A B Y
648 647 327 ffvelrnd φ w A B ¬ w = Y H w
649 569 ad2antrr φ w A B ¬ w = Y I : A B Y
650 649 327 ffvelrnd φ w A B ¬ w = Y I w
651 6 a1i φ w A B ¬ w = Y I = y A B Y π cos y 2
652 simpr φ w A B ¬ w = Y y = w y = w
653 652 fvoveq1d φ w A B ¬ w = Y y = w cos y 2 = cos w 2
654 653 oveq2d φ w A B ¬ w = Y y = w π cos y 2 = π cos w 2
655 124 a1i w A B π
656 330 halfcld w A B w 2
657 656 coscld w A B cos w 2
658 655 657 mulcld w A B π cos w 2
659 658 ad2antlr φ w A B ¬ w = Y π cos w 2
660 651 654 327 659 fvmptd φ w A B ¬ w = Y I w = π cos w 2
661 540 a1i φ w A B ¬ w = Y π π 0
662 657 ad2antlr φ w A B ¬ w = Y cos w 2
663 simpll φ w A B ¬ w = Y φ
664 fvoveq1 y = w cos y 2 = cos w 2
665 664 neeq1d y = w cos y 2 0 cos w 2 0
666 231 665 imbi12d y = w φ y A B Y cos y 2 0 φ w A B Y cos w 2 0
667 666 11 chvarvv φ w A B Y cos w 2 0
668 663 327 667 syl2anc φ w A B ¬ w = Y cos w 2 0
669 mulne0 π π 0 cos w 2 cos w 2 0 π cos w 2 0
670 661 662 668 669 syl12anc φ w A B ¬ w = Y π cos w 2 0
671 660 670 eqnetrd φ w A B ¬ w = Y I w 0
672 648 650 671 divcld φ w A B ¬ w = Y H w I w
673 641 645 327 672 fvmptd φ w A B ¬ w = Y y A B Y H y I y w = H w I w
674 5 a1i φ w A B ¬ w = Y H = y A B Y N + 1 2 cos N + 1 2 y
675 320 fveq2d φ w A B ¬ w = Y y = w cos N + 1 2 y = cos N + 1 2 w
676 675 oveq2d φ w A B ¬ w = Y y = w N + 1 2 cos N + 1 2 y = N + 1 2 cos N + 1 2 w
677 332 coscld φ w A B cos N + 1 2 w
678 328 677 mulcld φ w A B N + 1 2 cos N + 1 2 w
679 678 adantr φ w A B ¬ w = Y N + 1 2 cos N + 1 2 w
680 674 676 327 679 fvmptd φ w A B ¬ w = Y H w = N + 1 2 cos N + 1 2 w
681 680 660 oveq12d φ w A B ¬ w = Y H w I w = N + 1 2 cos N + 1 2 w π cos w 2
682 640 673 681 3eqtrrd φ w A B ¬ w = Y N + 1 2 cos N + 1 2 w π cos w 2 = if w = Y 2 N + 1 2 π y A B Y H y I y w
683 638 682 pm2.61dan φ w A B N + 1 2 cos N + 1 2 w π cos w 2 = if w = Y 2 N + 1 2 π y A B Y H y I y w
684 683 mpteq2dva φ w A B N + 1 2 cos N + 1 2 w π cos w 2 = w A B if w = Y 2 N + 1 2 π y A B Y H y I y w
685 579 684 eqtr2d φ w A B if w = Y 2 N + 1 2 π y A B Y H y I y w = L
686 352 48 82 constcncfg φ w A B N + 1 2 : A B cn
687 cosf cos :
688 236 51 sylan2 φ y A B N + 1 2 y
689 eqid y A B N + 1 2 y = y A B N + 1 2 y
690 688 689 fmptd φ y A B N + 1 2 y : A B
691 fcompt cos : y A B N + 1 2 y : A B cos y A B N + 1 2 y = w A B cos y A B N + 1 2 y w
692 687 690 691 sylancr φ cos y A B N + 1 2 y = w A B cos y A B N + 1 2 y w
693 eqidd φ w A B y A B N + 1 2 y = y A B N + 1 2 y
694 319 adantl φ w A B y = w N + 1 2 y = N + 1 2 w
695 simpr φ w A B w A B
696 693 694 695 332 fvmptd φ w A B y A B N + 1 2 y w = N + 1 2 w
697 696 fveq2d φ w A B cos y A B N + 1 2 y w = cos N + 1 2 w
698 697 mpteq2dva φ w A B cos y A B N + 1 2 y w = w A B cos N + 1 2 w
699 692 698 eqtr2d φ w A B cos N + 1 2 w = cos y A B N + 1 2 y
700 352 48 82 constcncfg φ y A B N + 1 2 : A B cn
701 352 82 idcncfg φ y A B y : A B cn
702 700 701 mulcncf φ y A B N + 1 2 y : A B cn
703 coscn cos : cn
704 703 a1i φ cos : cn
705 702 704 cncfco φ cos y A B N + 1 2 y : A B cn
706 699 705 eqeltrd φ w A B cos N + 1 2 w : A B cn
707 686 706 mulcncf φ w A B N + 1 2 cos N + 1 2 w : A B cn
708 eqid w A B π cos w 2 = w A B π cos w 2
709 352 160 82 constcncfg φ w A B π : A B cn
710 2cnd φ w A B 2
711 139 a1i φ w A B 2 0
712 331 710 711 divrecd φ w A B w 2 = w 1 2
713 712 mpteq2dva φ w A B w 2 = w A B w 1 2
714 eqid w w 1 2 = w w 1 2
715 cncfmptid w w : cn
716 81 81 715 mp2an w w : cn
717 716 a1i φ w w : cn
718 81 a1i 1 2
719 id 1 2 1 2
720 718 719 718 constcncfg 1 2 w 1 2 : cn
721 46 720 mp1i φ w 1 2 : cn
722 717 721 mulcncf φ w w 1 2 : cn
723 712 465 eqeltrrd φ w A B w 1 2
724 714 722 352 82 723 cncfmptssg φ w A B w 1 2 : A B cn
725 713 724 eqeltrd φ w A B w 2 : A B cn
726 704 725 cncfmpt1f φ w A B cos w 2 : A B cn
727 709 726 mulcncf φ w A B π cos w 2 : A B cn
728 ssid A B A B
729 728 a1i φ A B A B
730 difssd φ 0
731 658 adantl φ w A B π cos w 2
732 124 a1i φ w A B π
733 657 adantl φ w A B cos w 2
734 243 a1i φ w A B π 0
735 595 adantl φ w = Y cos w 2 = cos Y 2
736 633 adantr φ w = Y cos Y 2 0
737 735 736 eqnetrd φ w = Y cos w 2 0
738 737 adantlr φ w A B w = Y cos w 2 0
739 738 668 pm2.61dan φ w A B cos w 2 0
740 732 733 734 739 mulne0d φ w A B π cos w 2 0
741 740 neneqd φ w A B ¬ π cos w 2 = 0
742 elsng π cos w 2 π cos w 2 0 π cos w 2 = 0
743 731 742 syl φ w A B π cos w 2 0 π cos w 2 = 0
744 741 743 mtbird φ w A B ¬ π cos w 2 0
745 731 744 eldifd φ w A B π cos w 2 0
746 708 727 729 730 745 cncfmptssg φ w A B π cos w 2 : A B cn 0
747 707 746 divcncf φ w A B N + 1 2 cos N + 1 2 w π cos w 2 : A B cn
748 747 490 eleqtrd φ w A B N + 1 2 cos N + 1 2 w π cos w 2 TopOpen fld 𝑡 A B Cn TopOpen fld
749 579 748 eqeltrd φ L TopOpen fld 𝑡 A B Cn TopOpen fld
750 cncnp TopOpen fld 𝑡 A B TopOn A B TopOpen fld TopOn L TopOpen fld 𝑡 A B Cn TopOpen fld L : A B y A B L TopOpen fld 𝑡 A B CnP TopOpen fld y
751 358 356 750 sylancl φ L TopOpen fld 𝑡 A B Cn TopOpen fld L : A B y A B L TopOpen fld 𝑡 A B CnP TopOpen fld y
752 749 751 mpbid φ L : A B y A B L TopOpen fld 𝑡 A B CnP TopOpen fld y
753 752 simprd φ y A B L TopOpen fld 𝑡 A B CnP TopOpen fld y
754 363 eleq2d y = Y L TopOpen fld 𝑡 A B CnP TopOpen fld y L TopOpen fld 𝑡 A B CnP TopOpen fld Y
755 754 rspccva y A B L TopOpen fld 𝑡 A B CnP TopOpen fld y Y A B L TopOpen fld 𝑡 A B CnP TopOpen fld Y
756 753 9 755 syl2anc φ L TopOpen fld 𝑡 A B CnP TopOpen fld Y
757 685 756 eqeltrd φ w A B if w = Y 2 N + 1 2 π y A B Y H y I y w TopOpen fld 𝑡 A B CnP TopOpen fld Y
758 310 mpteq1d φ w A B Y Y if w = Y 2 N + 1 2 π y A B Y H y I y w = w A B if w = Y 2 N + 1 2 π y A B Y H y I y w
759 757 758 503 3eltr4d φ w A B Y Y if w = Y 2 N + 1 2 π y A B Y H y I y w TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y
760 eqid w A B Y Y if w = Y 2 N + 1 2 π y A B Y H y I y w = w A B Y Y if w = Y 2 N + 1 2 π y A B Y H y I y w
761 5 fvmpt2 y A B Y N + 1 2 cos N + 1 2 y H y = N + 1 2 cos N + 1 2 y
762 560 112 761 syl2anc φ y A B Y H y = N + 1 2 cos N + 1 2 y
763 762 562 oveq12d φ y A B Y H y I y = N + 1 2 cos N + 1 2 y π cos y 2
764 112 206 565 divcld φ y A B Y N + 1 2 cos N + 1 2 y π cos y 2
765 763 764 eqeltrd φ y A B Y H y I y
766 eqid y A B Y H y I y = y A B Y H y I y
767 765 766 fmptd φ y A B Y H y I y : A B Y
768 374 58 760 767 377 267 ellimc φ 2 N + 1 2 π y A B Y H y I y lim Y w A B Y Y if w = Y 2 N + 1 2 π y A B Y H y I y w TopOpen fld 𝑡 A B Y Y CnP TopOpen fld Y
769 759 768 mpbird φ 2 N + 1 2 π y A B Y H y I y lim Y
770 109 eqcomd φ H = D F
771 770 fveq1d φ H y = F y
772 204 eqcomd φ I = D G
773 772 fveq1d φ I y = G y
774 771 773 oveq12d φ H y I y = F y G y
775 774 mpteq2dv φ y A B Y H y I y = y A B Y F y G y
776 775 oveq1d φ y A B Y H y I y lim Y = y A B Y F y G y lim Y
777 769 776 eleqtrd φ 2 N + 1 2 π y A B Y F y G y lim Y
778 578 777 eqeltrd φ if Y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 Y 2 π sin Y 2 y A B Y F y G y lim Y
779 577 778 eqeltrd φ D N Y y A B Y F y G y lim Y
780 15 24 32 34 9 35 116 210 434 509 559 575 779 lhop φ D N Y y A B Y F y G y lim Y
781 1 dirkerval N D N = y if y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 y 2 π sin y 2
782 8 781 syl φ D N = y if y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 y 2 π sin y 2
783 782 reseq1d φ D N A B Y = y if y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 y 2 π sin y 2 A B Y
784 15 resmptd φ y if y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 y 2 π sin y 2 A B Y = y A B Y if y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 y 2 π sin y 2
785 260 iffalsed φ y A B Y if y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 y 2 π sin y 2 = sin N + 1 2 y 2 π sin y 2
786 23 recnd φ y A B Y sin N + 1 2 y
787 2 fvmpt2 y A B Y sin N + 1 2 y F y = sin N + 1 2 y
788 560 786 787 syl2anc φ y A B Y F y = sin N + 1 2 y
789 560 506 528 syl2anc φ y A B Y G y = 2 π sin y 2
790 788 789 oveq12d φ y A B Y F y G y = sin N + 1 2 y 2 π sin y 2
791 785 790 eqtr4d φ y A B Y if y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 y 2 π sin y 2 = F y G y
792 791 mpteq2dva φ y A B Y if y mod 2 π = 0 2 N + 1 2 π sin N + 1 2 y 2 π sin y 2 = y A B Y F y G y
793 783 784 792 3eqtrrd φ y A B Y F y G y = D N A B Y
794 793 oveq1d φ y A B Y F y G y lim Y = D N A B Y lim Y
795 780 794 eleqtrd φ D N Y D N A B Y lim Y