Metamath Proof Explorer


Theorem dirkertrigeqlem3

Description: Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of _pi . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkertrigeqlem3.n φ N
dirkertrigeqlem3.k φ K
dirkertrigeqlem3.a A = 2 K + 1 π
Assertion dirkertrigeqlem3 φ 1 2 + n = 1 N cos n A π = sin N + 1 2 A 2 π sin A 2

Proof

Step Hyp Ref Expression
1 dirkertrigeqlem3.n φ N
2 dirkertrigeqlem3.k φ K
3 dirkertrigeqlem3.a A = 2 K + 1 π
4 3 a1i φ n 1 N A = 2 K + 1 π
5 4 oveq2d φ n 1 N n A = n 2 K + 1 π
6 elfzelz n 1 N n
7 6 zcnd n 1 N n
8 7 adantl φ n 1 N n
9 2cnd φ n 1 N 2
10 2 zcnd φ K
11 10 adantr φ n 1 N K
12 9 11 mulcld φ n 1 N 2 K
13 1cnd φ n 1 N 1
14 12 13 addcld φ n 1 N 2 K + 1
15 picn π
16 15 a1i φ n 1 N π
17 14 16 mulcld φ n 1 N 2 K + 1 π
18 8 17 mulcomd φ n 1 N n 2 K + 1 π = 2 K + 1 π n
19 14 16 8 mulassd φ n 1 N 2 K + 1 π n = 2 K + 1 π n
20 16 8 mulcld φ n 1 N π n
21 12 13 20 adddird φ n 1 N 2 K + 1 π n = 2 K π n + 1 π n
22 12 20 mulcld φ n 1 N 2 K π n
23 13 20 mulcld φ n 1 N 1 π n
24 22 23 addcomd φ n 1 N 2 K π n + 1 π n = 1 π n + 2 K π n
25 15 a1i n 1 N π
26 25 7 mulcld n 1 N π n
27 26 mulid2d n 1 N 1 π n = π n
28 27 adantl φ n 1 N 1 π n = π n
29 9 11 16 8 mul4d φ n 1 N 2 K π n = 2 π K n
30 9 16 mulcld φ n 1 N 2 π
31 11 8 mulcld φ n 1 N K n
32 30 31 mulcomd φ n 1 N 2 π K n = K n 2 π
33 29 32 eqtrd φ n 1 N 2 K π n = K n 2 π
34 28 33 oveq12d φ n 1 N 1 π n + 2 K π n = π n + K n 2 π
35 24 34 eqtrd φ n 1 N 2 K π n + 1 π n = π n + K n 2 π
36 19 21 35 3eqtrd φ n 1 N 2 K + 1 π n = π n + K n 2 π
37 5 18 36 3eqtrd φ n 1 N n A = π n + K n 2 π
38 37 fveq2d φ n 1 N cos n A = cos π n + K n 2 π
39 2 adantr φ n 1 N K
40 6 adantl φ n 1 N n
41 39 40 zmulcld φ n 1 N K n
42 cosper π n K n cos π n + K n 2 π = cos π n
43 20 41 42 syl2anc φ n 1 N cos π n + K n 2 π = cos π n
44 38 43 eqtrd φ n 1 N cos n A = cos π n
45 44 sumeq2dv φ n = 1 N cos n A = n = 1 N cos π n
46 45 oveq2d φ 1 2 + n = 1 N cos n A = 1 2 + n = 1 N cos π n
47 46 oveq1d φ 1 2 + n = 1 N cos n A π = 1 2 + n = 1 N cos π n π
48 47 adantr φ N mod 2 = 0 1 2 + n = 1 N cos n A π = 1 2 + n = 1 N cos π n π
49 1 nncnd φ N
50 2cnd φ 2
51 2ne0 2 0
52 51 a1i φ 2 0
53 49 50 52 divcan2d φ 2 N 2 = N
54 53 eqcomd φ N = 2 N 2
55 54 oveq2d φ 1 N = 1 2 N 2
56 55 sumeq1d φ n = 1 N cos π n = n = 1 2 N 2 cos π n
57 56 adantr φ N mod 2 = 0 n = 1 N cos π n = n = 1 2 N 2 cos π n
58 15 a1i n 1 2 N 2 π
59 elfzelz n 1 2 N 2 n
60 59 zcnd n 1 2 N 2 n
61 58 60 mulcomd n 1 2 N 2 π n = n π
62 61 fveq2d n 1 2 N 2 cos π n = cos n π
63 62 rgen n 1 2 N 2 cos π n = cos n π
64 63 a1i φ N mod 2 = 0 n 1 2 N 2 cos π n = cos n π
65 64 sumeq2d φ N mod 2 = 0 n = 1 2 N 2 cos π n = n = 1 2 N 2 cos n π
66 simpr φ N mod 2 = 0 N mod 2 = 0
67 1 nnred φ N
68 67 adantr φ N mod 2 = 0 N
69 2rp 2 +
70 mod0 N 2 + N mod 2 = 0 N 2
71 68 69 70 sylancl φ N mod 2 = 0 N mod 2 = 0 N 2
72 66 71 mpbid φ N mod 2 = 0 N 2
73 2re 2
74 73 a1i φ 2
75 1 nngt0d φ 0 < N
76 2pos 0 < 2
77 76 a1i φ 0 < 2
78 67 74 75 77 divgt0d φ 0 < N 2
79 78 adantr φ N mod 2 = 0 0 < N 2
80 elnnz N 2 N 2 0 < N 2
81 72 79 80 sylanbrc φ N mod 2 = 0 N 2
82 dirkertrigeqlem1 N 2 n = 1 2 N 2 cos n π = 0
83 81 82 syl φ N mod 2 = 0 n = 1 2 N 2 cos n π = 0
84 57 65 83 3eqtrd φ N mod 2 = 0 n = 1 N cos π n = 0
85 84 oveq2d φ N mod 2 = 0 1 2 + n = 1 N cos π n = 1 2 + 0
86 halfcn 1 2
87 86 addid1i 1 2 + 0 = 1 2
88 85 87 eqtrdi φ N mod 2 = 0 1 2 + n = 1 N cos π n = 1 2
89 88 oveq1d φ N mod 2 = 0 1 2 + n = 1 N cos π n π = 1 2 π
90 ax-1cn 1
91 2cnne0 2 2 0
92 pire π
93 pipos 0 < π
94 92 93 gt0ne0ii π 0
95 15 94 pm3.2i π π 0
96 divdiv1 1 2 2 0 π π 0 1 2 π = 1 2 π
97 90 91 95 96 mp3an 1 2 π = 1 2 π
98 97 a1i φ N mod 2 = 0 1 2 π = 1 2 π
99 48 89 98 3eqtrd φ N mod 2 = 0 1 2 + n = 1 N cos n A π = 1 2 π
100 3 oveq2i N + 1 2 A = N + 1 2 2 K + 1 π
101 100 a1i φ N + 1 2 A = N + 1 2 2 K + 1 π
102 86 a1i φ 1 2
103 49 102 addcld φ N + 1 2
104 50 10 mulcld φ 2 K
105 peano2cn 2 K 2 K + 1
106 104 105 syl φ 2 K + 1
107 15 a1i φ π
108 103 106 107 mulassd φ N + 1 2 2 K + 1 π = N + 1 2 2 K + 1 π
109 1cnd φ 1
110 49 102 104 109 muladdd φ N + 1 2 2 K + 1 = N 2 K + 1 1 2 + N 1 + 2 K 1 2
111 49 50 10 mul12d φ N 2 K = 2 N K
112 102 mulid2d φ 1 1 2 = 1 2
113 111 112 oveq12d φ N 2 K + 1 1 2 = 2 N K + 1 2
114 49 mulid1d φ N 1 = N
115 50 10 mulcomd φ 2 K = K 2
116 115 oveq1d φ 2 K 1 2 = K 2 1 2
117 10 50 102 mulassd φ K 2 1 2 = K 2 1 2
118 2cn 2
119 118 51 recidi 2 1 2 = 1
120 119 oveq2i K 2 1 2 = K 1
121 10 mulid1d φ K 1 = K
122 120 121 syl5eq φ K 2 1 2 = K
123 116 117 122 3eqtrd φ 2 K 1 2 = K
124 114 123 oveq12d φ N 1 + 2 K 1 2 = N + K
125 113 124 oveq12d φ N 2 K + 1 1 2 + N 1 + 2 K 1 2 = 2 N K + 1 2 + N + K
126 49 10 mulcld φ N K
127 50 126 mulcld φ 2 N K
128 49 10 addcld φ N + K
129 127 102 128 addassd φ 2 N K + 1 2 + N + K = 2 N K + 1 2 + N + K
130 110 125 129 3eqtrd φ N + 1 2 2 K + 1 = 2 N K + 1 2 + N + K
131 102 128 addcld φ 1 2 + N + K
132 127 131 addcomd φ 2 N K + 1 2 + N + K = 1 2 + N + K + 2 N K
133 50 126 mulcomd φ 2 N K = N K 2
134 133 oveq2d φ 1 2 + N + K + 2 N K = 1 2 + N + K + N K 2
135 130 132 134 3eqtrd φ N + 1 2 2 K + 1 = 1 2 + N + K + N K 2
136 135 oveq1d φ N + 1 2 2 K + 1 π = 1 2 + N + K + N K 2 π
137 126 50 mulcld φ N K 2
138 131 137 107 adddird φ 1 2 + N + K + N K 2 π = 1 2 + N + K π + N K 2 π
139 126 50 107 mulassd φ N K 2 π = N K 2 π
140 139 oveq2d φ 1 2 + N + K π + N K 2 π = 1 2 + N + K π + N K 2 π
141 136 138 140 3eqtrd φ N + 1 2 2 K + 1 π = 1 2 + N + K π + N K 2 π
142 101 108 141 3eqtr2d φ N + 1 2 A = 1 2 + N + K π + N K 2 π
143 142 fveq2d φ sin N + 1 2 A = sin 1 2 + N + K π + N K 2 π
144 131 107 mulcld φ 1 2 + N + K π
145 1 nnzd φ N
146 145 2 zmulcld φ N K
147 sinper 1 2 + N + K π N K sin 1 2 + N + K π + N K 2 π = sin 1 2 + N + K π
148 144 146 147 syl2anc φ sin 1 2 + N + K π + N K 2 π = sin 1 2 + N + K π
149 102 128 addcomd φ 1 2 + N + K = N + K + 1 2
150 49 10 102 addassd φ N + K + 1 2 = N + K + 1 2
151 10 102 addcld φ K + 1 2
152 49 151 addcomd φ N + K + 1 2 = K + 1 2 + N
153 149 150 152 3eqtrd φ 1 2 + N + K = K + 1 2 + N
154 153 oveq1d φ 1 2 + N + K π = K + 1 2 + N π
155 154 fveq2d φ sin 1 2 + N + K π = sin K + 1 2 + N π
156 143 148 155 3eqtrd φ sin N + 1 2 A = sin K + 1 2 + N π
157 3 a1i φ A = 2 K + 1 π
158 157 oveq1d φ A 2 = 2 K + 1 π 2
159 106 107 50 52 div23d φ 2 K + 1 π 2 = 2 K + 1 2 π
160 104 109 50 52 divdird φ 2 K + 1 2 = 2 K 2 + 1 2
161 10 50 52 divcan3d φ 2 K 2 = K
162 161 oveq1d φ 2 K 2 + 1 2 = K + 1 2
163 160 162 eqtrd φ 2 K + 1 2 = K + 1 2
164 163 oveq1d φ 2 K + 1 2 π = K + 1 2 π
165 158 159 164 3eqtrd φ A 2 = K + 1 2 π
166 165 fveq2d φ sin A 2 = sin K + 1 2 π
167 166 oveq2d φ 2 π sin A 2 = 2 π sin K + 1 2 π
168 156 167 oveq12d φ sin N + 1 2 A 2 π sin A 2 = sin K + 1 2 + N π 2 π sin K + 1 2 π
169 168 adantr φ N mod 2 = 0 sin N + 1 2 A 2 π sin A 2 = sin K + 1 2 + N π 2 π sin K + 1 2 π
170 151 49 107 adddird φ K + 1 2 + N π = K + 1 2 π + N π
171 170 fveq2d φ sin K + 1 2 + N π = sin K + 1 2 π + N π
172 171 oveq1d φ sin K + 1 2 + N π 2 π sin K + 1 2 π = sin K + 1 2 π + N π 2 π sin K + 1 2 π
173 172 adantr φ N mod 2 = 0 sin K + 1 2 + N π 2 π sin K + 1 2 π = sin K + 1 2 π + N π 2 π sin K + 1 2 π
174 49 halfcld φ N 2
175 50 174 mulcomd φ 2 N 2 = N 2 2
176 53 175 eqtr3d φ N = N 2 2
177 176 oveq1d φ N π = N 2 2 π
178 174 50 107 mulassd φ N 2 2 π = N 2 2 π
179 177 178 eqtrd φ N π = N 2 2 π
180 179 oveq2d φ K + 1 2 π + N π = K + 1 2 π + N 2 2 π
181 180 fveq2d φ sin K + 1 2 π + N π = sin K + 1 2 π + N 2 2 π
182 181 adantr φ N mod 2 = 0 sin K + 1 2 π + N π = sin K + 1 2 π + N 2 2 π
183 10 adantr φ N mod 2 = 0 K
184 1cnd φ N mod 2 = 0 1
185 184 halfcld φ N mod 2 = 0 1 2
186 183 185 addcld φ N mod 2 = 0 K + 1 2
187 15 a1i φ N mod 2 = 0 π
188 186 187 mulcld φ N mod 2 = 0 K + 1 2 π
189 sinper K + 1 2 π N 2 sin K + 1 2 π + N 2 2 π = sin K + 1 2 π
190 188 72 189 syl2anc φ N mod 2 = 0 sin K + 1 2 π + N 2 2 π = sin K + 1 2 π
191 182 190 eqtrd φ N mod 2 = 0 sin K + 1 2 π + N π = sin K + 1 2 π
192 50 107 mulcld φ 2 π
193 151 107 mulcld φ K + 1 2 π
194 193 sincld φ sin K + 1 2 π
195 192 194 mulcomd φ 2 π sin K + 1 2 π = sin K + 1 2 π 2 π
196 195 adantr φ N mod 2 = 0 2 π sin K + 1 2 π = sin K + 1 2 π 2 π
197 191 196 oveq12d φ N mod 2 = 0 sin K + 1 2 π + N π 2 π sin K + 1 2 π = sin K + 1 2 π sin K + 1 2 π 2 π
198 94 a1i φ π 0
199 151 107 198 divcan4d φ K + 1 2 π π = K + 1 2
200 2 zred φ K
201 69 a1i φ 2 +
202 201 rpreccld φ 1 2 +
203 200 202 ltaddrpd φ K < K + 1 2
204 1red φ 1
205 204 rehalfcld φ 1 2
206 halflt1 1 2 < 1
207 206 a1i φ 1 2 < 1
208 205 204 200 207 ltadd2dd φ K + 1 2 < K + 1
209 btwnnz K K < K + 1 2 K + 1 2 < K + 1 ¬ K + 1 2
210 2 203 208 209 syl3anc φ ¬ K + 1 2
211 199 210 eqneltrd φ ¬ K + 1 2 π π
212 sineq0 K + 1 2 π sin K + 1 2 π = 0 K + 1 2 π π
213 193 212 syl φ sin K + 1 2 π = 0 K + 1 2 π π
214 211 213 mtbird φ ¬ sin K + 1 2 π = 0
215 214 neqned φ sin K + 1 2 π 0
216 50 107 52 198 mulne0d φ 2 π 0
217 194 194 192 215 216 divdiv1d φ sin K + 1 2 π sin K + 1 2 π 2 π = sin K + 1 2 π sin K + 1 2 π 2 π
218 194 215 dividd φ sin K + 1 2 π sin K + 1 2 π = 1
219 218 oveq1d φ sin K + 1 2 π sin K + 1 2 π 2 π = 1 2 π
220 217 219 eqtr3d φ sin K + 1 2 π sin K + 1 2 π 2 π = 1 2 π
221 220 adantr φ N mod 2 = 0 sin K + 1 2 π sin K + 1 2 π 2 π = 1 2 π
222 197 221 eqtrd φ N mod 2 = 0 sin K + 1 2 π + N π 2 π sin K + 1 2 π = 1 2 π
223 169 173 222 3eqtrrd φ N mod 2 = 0 1 2 π = sin N + 1 2 A 2 π sin A 2
224 99 223 eqtrd φ N mod 2 = 0 1 2 + n = 1 N cos n A π = sin N + 1 2 A 2 π sin A 2
225 47 adantr φ ¬ N mod 2 = 0 1 2 + n = 1 N cos n A π = 1 2 + n = 1 N cos π n π
226 145 adantr φ ¬ N mod 2 = 0 N
227 simpr φ ¬ N mod 2 = 0 ¬ N mod 2 = 0
228 227 neqned φ ¬ N mod 2 = 0 N mod 2 0
229 oddfl N N mod 2 0 N = 2 N 2 + 1
230 226 228 229 syl2anc φ ¬ N mod 2 = 0 N = 2 N 2 + 1
231 230 oveq2d φ ¬ N mod 2 = 0 1 N = 1 2 N 2 + 1
232 231 sumeq1d φ ¬ N mod 2 = 0 n = 1 N cos π n = n = 1 2 N 2 + 1 cos π n
233 fvoveq1 N = 1 N 2 = 1 2
234 halffl 1 2 = 0
235 233 234 eqtrdi N = 1 N 2 = 0
236 235 oveq2d N = 1 2 N 2 = 2 0
237 2t0e0 2 0 = 0
238 236 237 eqtrdi N = 1 2 N 2 = 0
239 238 oveq1d N = 1 2 N 2 + 1 = 0 + 1
240 90 addid2i 0 + 1 = 1
241 239 240 eqtrdi N = 1 2 N 2 + 1 = 1
242 241 oveq2d N = 1 1 2 N 2 + 1 = 1 1
243 242 sumeq1d N = 1 n = 1 2 N 2 + 1 cos π n = n = 1 1 cos π n
244 1z 1
245 coscl π cos π
246 15 245 ax-mp cos π
247 oveq2 n = 1 π n = π 1
248 15 mulid1i π 1 = π
249 247 248 eqtrdi n = 1 π n = π
250 249 fveq2d n = 1 cos π n = cos π
251 250 fsum1 1 cos π n = 1 1 cos π n = cos π
252 244 246 251 mp2an n = 1 1 cos π n = cos π
253 252 a1i N = 1 n = 1 1 cos π n = cos π
254 cospi cos π = 1
255 254 a1i N = 1 cos π = 1
256 243 253 255 3eqtrd N = 1 n = 1 2 N 2 + 1 cos π n = 1
257 256 adantl φ N = 1 n = 1 2 N 2 + 1 cos π n = 1
258 2nn 2
259 258 a1i φ ¬ N = 1 2
260 67 rehalfcld φ N 2
261 260 flcld φ N 2
262 261 adantr φ ¬ N = 1 N 2
263 2div2e1 2 2 = 1
264 73 a1i φ ¬ N = 1 2
265 67 adantr φ ¬ N = 1 N
266 69 a1i φ ¬ N = 1 2 +
267 neqne ¬ N = 1 N 1
268 nnne1ge2 N N 1 2 N
269 1 267 268 syl2an φ ¬ N = 1 2 N
270 264 265 266 269 lediv1dd φ ¬ N = 1 2 2 N 2
271 263 270 eqbrtrrid φ ¬ N = 1 1 N 2
272 260 adantr φ ¬ N = 1 N 2
273 flge N 2 1 1 N 2 1 N 2
274 272 244 273 sylancl φ ¬ N = 1 1 N 2 1 N 2
275 271 274 mpbid φ ¬ N = 1 1 N 2
276 elnnz1 N 2 N 2 1 N 2
277 262 275 276 sylanbrc φ ¬ N = 1 N 2
278 259 277 nnmulcld φ ¬ N = 1 2 N 2
279 nnuz = 1
280 278 279 eleqtrdi φ ¬ N = 1 2 N 2 1
281 15 a1i φ ¬ N = 1 n 1 2 N 2 + 1 π
282 elfzelz n 1 2 N 2 + 1 n
283 282 zcnd n 1 2 N 2 + 1 n
284 283 adantl φ ¬ N = 1 n 1 2 N 2 + 1 n
285 281 284 mulcld φ ¬ N = 1 n 1 2 N 2 + 1 π n
286 285 coscld φ ¬ N = 1 n 1 2 N 2 + 1 cos π n
287 oveq2 n = 2 N 2 + 1 π n = π 2 N 2 + 1
288 287 fveq2d n = 2 N 2 + 1 cos π n = cos π 2 N 2 + 1
289 280 286 288 fsump1 φ ¬ N = 1 n = 1 2 N 2 + 1 cos π n = n = 1 2 N 2 cos π n + cos π 2 N 2 + 1
290 15 a1i n 1 2 N 2 π
291 elfzelz n 1 2 N 2 n
292 291 zcnd n 1 2 N 2 n
293 290 292 mulcomd n 1 2 N 2 π n = n π
294 293 fveq2d n 1 2 N 2 cos π n = cos n π
295 294 sumeq2i n = 1 2 N 2 cos π n = n = 1 2 N 2 cos n π
296 dirkertrigeqlem1 N 2 n = 1 2 N 2 cos n π = 0
297 277 296 syl φ ¬ N = 1 n = 1 2 N 2 cos n π = 0
298 295 297 syl5eq φ ¬ N = 1 n = 1 2 N 2 cos π n = 0
299 261 zcnd φ N 2
300 50 299 mulcld φ 2 N 2
301 107 300 109 adddid φ π 2 N 2 + 1 = π 2 N 2 + π 1
302 107 50 299 mul13d φ π 2 N 2 = N 2 2 π
303 248 a1i φ π 1 = π
304 302 303 oveq12d φ π 2 N 2 + π 1 = N 2 2 π + π
305 299 192 mulcld φ N 2 2 π
306 305 107 addcomd φ N 2 2 π + π = π + N 2 2 π
307 301 304 306 3eqtrd φ π 2 N 2 + 1 = π + N 2 2 π
308 307 fveq2d φ cos π 2 N 2 + 1 = cos π + N 2 2 π
309 cosper π N 2 cos π + N 2 2 π = cos π
310 107 261 309 syl2anc φ cos π + N 2 2 π = cos π
311 254 a1i φ cos π = 1
312 308 310 311 3eqtrd φ cos π 2 N 2 + 1 = 1
313 312 adantr φ ¬ N = 1 cos π 2 N 2 + 1 = 1
314 298 313 oveq12d φ ¬ N = 1 n = 1 2 N 2 cos π n + cos π 2 N 2 + 1 = 0 + -1
315 neg1cn 1
316 315 addid2i 0 + -1 = 1
317 316 a1i φ ¬ N = 1 0 + -1 = 1
318 289 314 317 3eqtrd φ ¬ N = 1 n = 1 2 N 2 + 1 cos π n = 1
319 257 318 pm2.61dan φ n = 1 2 N 2 + 1 cos π n = 1
320 319 adantr φ ¬ N mod 2 = 0 n = 1 2 N 2 + 1 cos π n = 1
321 232 320 eqtrd φ ¬ N mod 2 = 0 n = 1 N cos π n = 1
322 321 oveq2d φ ¬ N mod 2 = 0 1 2 + n = 1 N cos π n = 1 2 + -1
323 322 oveq1d φ ¬ N mod 2 = 0 1 2 + n = 1 N cos π n π = 1 2 + -1 π
324 168 172 eqtrd φ sin N + 1 2 A 2 π sin A 2 = sin K + 1 2 π + N π 2 π sin K + 1 2 π
325 324 adantr φ ¬ N mod 2 = 0 sin N + 1 2 A 2 π sin A 2 = sin K + 1 2 π + N π 2 π sin K + 1 2 π
326 230 oveq1d φ ¬ N mod 2 = 0 N π = 2 N 2 + 1 π
327 300 109 107 adddird φ 2 N 2 + 1 π = 2 N 2 π + 1 π
328 107 mulid2d φ 1 π = π
329 328 oveq2d φ 2 N 2 π + 1 π = 2 N 2 π + π
330 300 107 mulcld φ 2 N 2 π
331 330 107 addcomd φ 2 N 2 π + π = π + 2 N 2 π
332 327 329 331 3eqtrd φ 2 N 2 + 1 π = π + 2 N 2 π
333 332 adantr φ ¬ N mod 2 = 0 2 N 2 + 1 π = π + 2 N 2 π
334 50 299 mulcomd φ 2 N 2 = N 2 2
335 334 oveq1d φ 2 N 2 π = N 2 2 π
336 299 50 107 mulassd φ N 2 2 π = N 2 2 π
337 335 336 eqtrd φ 2 N 2 π = N 2 2 π
338 337 oveq2d φ π + 2 N 2 π = π + N 2 2 π
339 338 adantr φ ¬ N mod 2 = 0 π + 2 N 2 π = π + N 2 2 π
340 326 333 339 3eqtrd φ ¬ N mod 2 = 0 N π = π + N 2 2 π
341 340 oveq2d φ ¬ N mod 2 = 0 K + 1 2 π + N π = K + 1 2 π + π + N 2 2 π
342 193 adantr φ ¬ N mod 2 = 0 K + 1 2 π
343 15 a1i φ ¬ N mod 2 = 0 π
344 305 adantr φ ¬ N mod 2 = 0 N 2 2 π
345 342 343 344 addassd φ ¬ N mod 2 = 0 K + 1 2 π + π + N 2 2 π = K + 1 2 π + π + N 2 2 π
346 341 345 eqtr4d φ ¬ N mod 2 = 0 K + 1 2 π + N π = K + 1 2 π + π + N 2 2 π
347 346 fveq2d φ ¬ N mod 2 = 0 sin K + 1 2 π + N π = sin K + 1 2 π + π + N 2 2 π
348 347 oveq1d φ ¬ N mod 2 = 0 sin K + 1 2 π + N π 2 π sin K + 1 2 π = sin K + 1 2 π + π + N 2 2 π 2 π sin K + 1 2 π
349 193 107 addcld φ K + 1 2 π + π
350 sinper K + 1 2 π + π N 2 sin K + 1 2 π + π + N 2 2 π = sin K + 1 2 π + π
351 349 261 350 syl2anc φ sin K + 1 2 π + π + N 2 2 π = sin K + 1 2 π + π
352 sinppi K + 1 2 π sin K + 1 2 π + π = sin K + 1 2 π
353 193 352 syl φ sin K + 1 2 π + π = sin K + 1 2 π
354 351 353 eqtrd φ sin K + 1 2 π + π + N 2 2 π = sin K + 1 2 π
355 354 oveq1d φ sin K + 1 2 π + π + N 2 2 π 2 π sin K + 1 2 π = sin K + 1 2 π 2 π sin K + 1 2 π
356 195 oveq2d φ sin K + 1 2 π 2 π sin K + 1 2 π = sin K + 1 2 π sin K + 1 2 π 2 π
357 194 194 215 divnegd φ sin K + 1 2 π sin K + 1 2 π = sin K + 1 2 π sin K + 1 2 π
358 218 negeqd φ sin K + 1 2 π sin K + 1 2 π = 1
359 357 358 eqtr3d φ sin K + 1 2 π sin K + 1 2 π = 1
360 359 oveq1d φ sin K + 1 2 π sin K + 1 2 π 2 π = 1 2 π
361 194 negcld φ sin K + 1 2 π
362 361 194 192 215 216 divdiv1d φ sin K + 1 2 π sin K + 1 2 π 2 π = sin K + 1 2 π sin K + 1 2 π 2 π
363 86 90 negsubi 1 2 + -1 = 1 2 1
364 90 86 negsubdi2i 1 1 2 = 1 2 1
365 1mhlfehlf 1 1 2 = 1 2
366 365 negeqi 1 1 2 = 1 2
367 divneg 1 2 2 0 1 2 = 1 2
368 90 118 51 367 mp3an 1 2 = 1 2
369 366 368 eqtri 1 1 2 = 1 2
370 363 364 369 3eqtr2i 1 2 + -1 = 1 2
371 370 oveq1i 1 2 + -1 π = 1 2 π
372 divdiv1 1 2 2 0 π π 0 1 2 π = 1 2 π
373 315 91 95 372 mp3an 1 2 π = 1 2 π
374 371 373 eqtr2i 1 2 π = 1 2 + -1 π
375 374 a1i φ 1 2 π = 1 2 + -1 π
376 360 362 375 3eqtr3d φ sin K + 1 2 π sin K + 1 2 π 2 π = 1 2 + -1 π
377 355 356 376 3eqtrd φ sin K + 1 2 π + π + N 2 2 π 2 π sin K + 1 2 π = 1 2 + -1 π
378 377 adantr φ ¬ N mod 2 = 0 sin K + 1 2 π + π + N 2 2 π 2 π sin K + 1 2 π = 1 2 + -1 π
379 325 348 378 3eqtrrd φ ¬ N mod 2 = 0 1 2 + -1 π = sin N + 1 2 A 2 π sin A 2
380 225 323 379 3eqtrd φ ¬ N mod 2 = 0 1 2 + n = 1 N cos n A π = sin N + 1 2 A 2 π sin A 2
381 224 380 pm2.61dan φ 1 2 + n = 1 N cos n A π = sin N + 1 2 A 2 π sin A 2