Metamath Proof Explorer


Theorem basellem8

Description: Lemma for basel . The function F of partial sums of the inverse squares is bounded below by J and above by K , obtained by summing the inequality cot ^ 2 x <_ 1 / x ^ 2 <_ csc ^ 2 x = cot ^ 2 x + 1 over the M roots of the polynomial P , and applying the identity basellem5 . (Contributed by Mario Carneiro, 29-Jul-2014)

Ref Expression
Hypotheses basel.g G = n 1 2 n + 1
basel.f F = seq 1 + n n 2
basel.h H = × π 2 6 × f × 1 f G
basel.j J = H × f × 1 + f × 2 × f G
basel.k K = H × f × 1 + f G
basellem8.n N = 2 M + 1
Assertion basellem8 M J M F M F M K M

Proof

Step Hyp Ref Expression
1 basel.g G = n 1 2 n + 1
2 basel.f F = seq 1 + n n 2
3 basel.h H = × π 2 6 × f × 1 f G
4 basel.j J = H × f × 1 + f × 2 × f G
5 basel.k K = H × f × 1 + f G
6 basellem8.n N = 2 M + 1
7 fzfid M 1 M Fin
8 pire π
9 2nn 2
10 nnmulcl 2 M 2 M
11 9 10 mpan M 2 M
12 11 peano2nnd M 2 M + 1
13 6 12 eqeltrid M N
14 nndivre π N π N
15 8 13 14 sylancr M π N
16 15 resqcld M π N 2
17 16 adantr M k 1 M π N 2
18 6 basellem1 M k 1 M k π N 0 π 2
19 tanrpcl k π N 0 π 2 tan k π N +
20 18 19 syl M k 1 M tan k π N +
21 20 rpred M k 1 M tan k π N
22 20 rpne0d M k 1 M tan k π N 0
23 2z 2
24 znegcl 2 2
25 23 24 ax-mp 2
26 25 a1i M k 1 M 2
27 21 22 26 reexpclzd M k 1 M tan k π N 2
28 17 27 remulcld M k 1 M π N 2 tan k π N 2
29 elfznn k 1 M k
30 29 adantl M k 1 M k
31 30 nnred M k 1 M k
32 30 nnne0d M k 1 M k 0
33 31 32 26 reexpclzd M k 1 M k 2
34 21 recnd M k 1 M tan k π N
35 2nn0 2 0
36 expneg tan k π N 2 0 tan k π N 2 = 1 tan k π N 2
37 34 35 36 sylancl M k 1 M tan k π N 2 = 1 tan k π N 2
38 37 oveq2d M k 1 M π N 2 tan k π N 2 = π N 2 1 tan k π N 2
39 15 recnd M π N
40 39 sqcld M π N 2
41 40 adantr M k 1 M π N 2
42 rpexpcl tan k π N + 2 tan k π N 2 +
43 20 23 42 sylancl M k 1 M tan k π N 2 +
44 43 rpred M k 1 M tan k π N 2
45 44 recnd M k 1 M tan k π N 2
46 43 rpne0d M k 1 M tan k π N 2 0
47 41 45 46 divrecd M k 1 M π N 2 tan k π N 2 = π N 2 1 tan k π N 2
48 38 47 eqtr4d M k 1 M π N 2 tan k π N 2 = π N 2 tan k π N 2
49 30 nnrpd M k 1 M k +
50 rpexpcl k + 2 k 2 +
51 49 25 50 sylancl M k 1 M k 2 +
52 30 nncnd M k 1 M k
53 52 32 26 expnegd M k 1 M k -2 = 1 k 2
54 2cn 2
55 54 negnegi -2 = 2
56 55 oveq2i k -2 = k 2
57 53 56 eqtr3di M k 1 M 1 k 2 = k 2
58 57 oveq1d M k 1 M 1 k 2 π N 2 = k 2 π N 2
59 nncn k k
60 nnne0 k k 0
61 25 a1i k 2
62 59 60 61 expclzd k k 2
63 30 62 syl M k 1 M k 2
64 52 32 26 expne0d M k 1 M k 2 0
65 41 63 64 divrec2d M k 1 M π N 2 k 2 = 1 k 2 π N 2
66 8 recni π
67 66 a1i M k 1 M π
68 13 nncnd M N
69 13 nnne0d M N 0
70 68 69 jca M N N 0
71 70 adantr M k 1 M N N 0
72 divass k π N N 0 k π N = k π N
73 52 67 71 72 syl3anc M k 1 M k π N = k π N
74 73 oveq1d M k 1 M k π N 2 = k π N 2
75 39 adantr M k 1 M π N
76 52 75 sqmuld M k 1 M k π N 2 = k 2 π N 2
77 74 76 eqtrd M k 1 M k π N 2 = k 2 π N 2
78 58 65 77 3eqtr4d M k 1 M π N 2 k 2 = k π N 2
79 elioore k π N 0 π 2 k π N
80 18 79 syl M k 1 M k π N
81 80 resqcld M k 1 M k π N 2
82 tangtx k π N 0 π 2 k π N < tan k π N
83 18 82 syl M k 1 M k π N < tan k π N
84 eliooord k π N 0 π 2 0 < k π N k π N < π 2
85 18 84 syl M k 1 M 0 < k π N k π N < π 2
86 85 simpld M k 1 M 0 < k π N
87 80 86 elrpd M k 1 M k π N +
88 87 rpge0d M k 1 M 0 k π N
89 20 rpge0d M k 1 M 0 tan k π N
90 80 21 88 89 lt2sqd M k 1 M k π N < tan k π N k π N 2 < tan k π N 2
91 83 90 mpbid M k 1 M k π N 2 < tan k π N 2
92 81 44 91 ltled M k 1 M k π N 2 tan k π N 2
93 78 92 eqbrtrd M k 1 M π N 2 k 2 tan k π N 2
94 17 51 43 93 lediv23d M k 1 M π N 2 tan k π N 2 k 2
95 48 94 eqbrtrd M k 1 M π N 2 tan k π N 2 k 2
96 7 28 33 95 fsumle M k = 1 M π N 2 tan k π N 2 k = 1 M k 2
97 oveq2 n = M 2 n = 2 M
98 97 oveq1d n = M 2 n + 1 = 2 M + 1
99 98 6 eqtr4di n = M 2 n + 1 = N
100 99 oveq2d n = M 1 2 n + 1 = 1 N
101 100 oveq2d n = M 1 1 2 n + 1 = 1 1 N
102 101 oveq2d n = M π 2 6 1 1 2 n + 1 = π 2 6 1 1 N
103 100 oveq2d n = M -2 1 2 n + 1 = -2 1 N
104 103 oveq2d n = M 1 + -2 1 2 n + 1 = 1 + -2 1 N
105 102 104 oveq12d n = M π 2 6 1 1 2 n + 1 1 + -2 1 2 n + 1 = π 2 6 1 1 N 1 + -2 1 N
106 nnex V
107 106 a1i V
108 ovexd n π 2 6 1 1 2 n + 1 V
109 ovexd n 1 + -2 1 2 n + 1 V
110 8 resqcli π 2
111 6re 6
112 6nn 6
113 112 nnne0i 6 0
114 110 111 113 redivcli π 2 6
115 114 a1i n π 2 6
116 ovexd n 1 1 2 n + 1 V
117 fconstmpt × π 2 6 = n π 2 6
118 117 a1i × π 2 6 = n π 2 6
119 1zzd n 1
120 ovexd n 1 2 n + 1 V
121 fconstmpt × 1 = n 1
122 121 a1i × 1 = n 1
123 1 a1i G = n 1 2 n + 1
124 107 119 120 122 123 offval2 × 1 f G = n 1 1 2 n + 1
125 107 115 116 118 124 offval2 × π 2 6 × f × 1 f G = n π 2 6 1 1 2 n + 1
126 3 125 syl5eq H = n π 2 6 1 1 2 n + 1
127 ovexd n -2 1 2 n + 1 V
128 54 negcli 2
129 128 a1i n 2
130 fconstmpt × 2 = n 2
131 130 a1i × 2 = n 2
132 107 129 120 131 123 offval2 × 2 × f G = n -2 1 2 n + 1
133 107 119 127 122 132 offval2 × 1 + f × 2 × f G = n 1 + -2 1 2 n + 1
134 107 108 109 126 133 offval2 H × f × 1 + f × 2 × f G = n π 2 6 1 1 2 n + 1 1 + -2 1 2 n + 1
135 134 mptru H × f × 1 + f × 2 × f G = n π 2 6 1 1 2 n + 1 1 + -2 1 2 n + 1
136 4 135 eqtri J = n π 2 6 1 1 2 n + 1 1 + -2 1 2 n + 1
137 ovex π 2 6 1 1 N 1 + -2 1 N V
138 105 136 137 fvmpt M J M = π 2 6 1 1 N 1 + -2 1 N
139 114 recni π 2 6
140 139 a1i M π 2 6
141 11 nncnd M 2 M
142 141 68 69 divcld M 2 M N
143 ax-1cn 1
144 subcl 2 M 1 2 M 1
145 141 143 144 sylancl M 2 M 1
146 145 68 69 divcld M 2 M 1 N
147 140 142 146 mulassd M π 2 6 2 M N 2 M 1 N = π 2 6 2 M N 2 M 1 N
148 1cnd M 1
149 68 148 68 69 divsubdird M N 1 N = N N 1 N
150 6 oveq1i N 1 = 2 M + 1 - 1
151 pncan 2 M 1 2 M + 1 - 1 = 2 M
152 141 143 151 sylancl M 2 M + 1 - 1 = 2 M
153 150 152 syl5eq M N 1 = 2 M
154 153 oveq1d M N 1 N = 2 M N
155 68 69 dividd M N N = 1
156 155 oveq1d M N N 1 N = 1 1 N
157 149 154 156 3eqtr3rd M 1 1 N = 2 M N
158 157 oveq2d M π 2 6 1 1 N = π 2 6 2 M N
159 128 a1i M 2
160 68 159 68 69 divdird M N + -2 N = N N + 2 N
161 negsub N 2 N + -2 = N 2
162 68 54 161 sylancl M N + -2 = N 2
163 df-2 2 = 1 + 1
164 6 163 oveq12i N 2 = 2 M + 1 - 1 + 1
165 141 148 148 pnpcan2d M 2 M + 1 - 1 + 1 = 2 M 1
166 164 165 syl5eq M N 2 = 2 M 1
167 162 166 eqtrd M N + -2 = 2 M 1
168 167 oveq1d M N + -2 N = 2 M 1 N
169 159 68 69 divrecd M 2 N = -2 1 N
170 155 169 oveq12d M N N + 2 N = 1 + -2 1 N
171 160 168 170 3eqtr3rd M 1 + -2 1 N = 2 M 1 N
172 158 171 oveq12d M π 2 6 1 1 N 1 + -2 1 N = π 2 6 2 M N 2 M 1 N
173 13 nnsqcld M N 2
174 173 nncnd M N 2
175 6cn 6
176 mulcom N 2 6 N 2 6 = 6 N 2
177 174 175 176 sylancl M N 2 6 = 6 N 2
178 177 oveq2d M π 2 2 M 2 M 1 N 2 6 = π 2 2 M 2 M 1 6 N 2
179 110 recni π 2
180 179 a1i M π 2
181 141 145 mulcld M 2 M 2 M 1
182 173 nnne0d M N 2 0
183 174 182 jca M N 2 N 2 0
184 175 113 pm3.2i 6 6 0
185 184 a1i M 6 6 0
186 divmuldiv π 2 2 M 2 M 1 N 2 N 2 0 6 6 0 π 2 N 2 2 M 2 M 1 6 = π 2 2 M 2 M 1 N 2 6
187 180 181 183 185 186 syl22anc M π 2 N 2 2 M 2 M 1 6 = π 2 2 M 2 M 1 N 2 6
188 divmuldiv π 2 2 M 2 M 1 6 6 0 N 2 N 2 0 π 2 6 2 M 2 M 1 N 2 = π 2 2 M 2 M 1 6 N 2
189 180 181 185 183 188 syl22anc M π 2 6 2 M 2 M 1 N 2 = π 2 2 M 2 M 1 6 N 2
190 178 187 189 3eqtr4d M π 2 N 2 2 M 2 M 1 6 = π 2 6 2 M 2 M 1 N 2
191 66 a1i M π
192 191 68 69 sqdivd M π N 2 = π 2 N 2
193 192 oveq1d M π N 2 2 M 2 M 1 6 = π 2 N 2 2 M 2 M 1 6
194 141 68 145 68 69 69 divmuldivd M 2 M N 2 M 1 N = 2 M 2 M 1 N N
195 68 sqvald M N 2 = N N
196 195 oveq2d M 2 M 2 M 1 N 2 = 2 M 2 M 1 N N
197 194 196 eqtr4d M 2 M N 2 M 1 N = 2 M 2 M 1 N 2
198 197 oveq2d M π 2 6 2 M N 2 M 1 N = π 2 6 2 M 2 M 1 N 2
199 190 193 198 3eqtr4d M π N 2 2 M 2 M 1 6 = π 2 6 2 M N 2 M 1 N
200 147 172 199 3eqtr4d M π 2 6 1 1 N 1 + -2 1 N = π N 2 2 M 2 M 1 6
201 eqid x j = 0 M ( N 2 j ) 1 M j x j = x j = 0 M ( N 2 j ) 1 M j x j
202 eqid n 1 M tan n π N 2 = n 1 M tan n π N 2
203 6 201 202 basellem5 M k = 1 M tan k π N 2 = 2 M 2 M 1 6
204 203 oveq2d M π N 2 k = 1 M tan k π N 2 = π N 2 2 M 2 M 1 6
205 200 204 eqtr4d M π 2 6 1 1 N 1 + -2 1 N = π N 2 k = 1 M tan k π N 2
206 27 recnd M k 1 M tan k π N 2
207 7 40 206 fsummulc2 M π N 2 k = 1 M tan k π N 2 = k = 1 M π N 2 tan k π N 2
208 138 205 207 3eqtrd M J M = k = 1 M π N 2 tan k π N 2
209 2 fveq1i F M = seq 1 + n n 2 M
210 oveq1 n = k n 2 = k 2
211 eqid n n 2 = n n 2
212 ovex k 2 V
213 210 211 212 fvmpt k n n 2 k = k 2
214 30 213 syl M k 1 M n n 2 k = k 2
215 id M M
216 nnuz = 1
217 215 216 eleqtrdi M M 1
218 214 217 63 fsumser M k = 1 M k 2 = seq 1 + n n 2 M
219 209 218 eqtr4id M F M = k = 1 M k 2
220 96 208 219 3brtr4d M J M F M
221 80 resincld M k 1 M sin k π N
222 sincosq1sgn k π N 0 π 2 0 < sin k π N 0 < cos k π N
223 18 222 syl M k 1 M 0 < sin k π N 0 < cos k π N
224 223 simpld M k 1 M 0 < sin k π N
225 224 gt0ne0d M k 1 M sin k π N 0
226 221 225 26 reexpclzd M k 1 M sin k π N 2
227 17 226 remulcld M k 1 M π N 2 sin k π N 2
228 sinltx k π N + sin k π N < k π N
229 87 228 syl M k 1 M sin k π N < k π N
230 221 80 229 ltled M k 1 M sin k π N k π N
231 0re 0
232 ltle 0 sin k π N 0 < sin k π N 0 sin k π N
233 231 221 232 sylancr M k 1 M 0 < sin k π N 0 sin k π N
234 224 233 mpd M k 1 M 0 sin k π N
235 221 80 234 88 le2sqd M k 1 M sin k π N k π N sin k π N 2 k π N 2
236 230 235 mpbid M k 1 M sin k π N 2 k π N 2
237 236 78 breqtrrd M k 1 M sin k π N 2 π N 2 k 2
238 221 resqcld M k 1 M sin k π N 2
239 238 17 51 lemuldiv2d M k 1 M k 2 sin k π N 2 π N 2 sin k π N 2 π N 2 k 2
240 221 224 elrpd M k 1 M sin k π N +
241 rpexpcl sin k π N + 2 sin k π N 2 +
242 240 23 241 sylancl M k 1 M sin k π N 2 +
243 33 17 242 lemuldivd M k 1 M k 2 sin k π N 2 π N 2 k 2 π N 2 sin k π N 2
244 239 243 bitr3d M k 1 M sin k π N 2 π N 2 k 2 k 2 π N 2 sin k π N 2
245 237 244 mpbid M k 1 M k 2 π N 2 sin k π N 2
246 221 recnd M k 1 M sin k π N
247 expneg sin k π N 2 0 sin k π N 2 = 1 sin k π N 2
248 246 35 247 sylancl M k 1 M sin k π N 2 = 1 sin k π N 2
249 248 oveq2d M k 1 M π N 2 sin k π N 2 = π N 2 1 sin k π N 2
250 238 recnd M k 1 M sin k π N 2
251 242 rpne0d M k 1 M sin k π N 2 0
252 41 250 251 divrecd M k 1 M π N 2 sin k π N 2 = π N 2 1 sin k π N 2
253 249 252 eqtr4d M k 1 M π N 2 sin k π N 2 = π N 2 sin k π N 2
254 245 253 breqtrrd M k 1 M k 2 π N 2 sin k π N 2
255 7 33 227 254 fsumle M k = 1 M k 2 k = 1 M π N 2 sin k π N 2
256 100 oveq2d n = M 1 + 1 2 n + 1 = 1 + 1 N
257 102 256 oveq12d n = M π 2 6 1 1 2 n + 1 1 + 1 2 n + 1 = π 2 6 1 1 N 1 + 1 N
258 ovexd n 1 + 1 2 n + 1 V
259 107 119 120 122 123 offval2 × 1 + f G = n 1 + 1 2 n + 1
260 107 108 258 126 259 offval2 H × f × 1 + f G = n π 2 6 1 1 2 n + 1 1 + 1 2 n + 1
261 260 mptru H × f × 1 + f G = n π 2 6 1 1 2 n + 1 1 + 1 2 n + 1
262 5 261 eqtri K = n π 2 6 1 1 2 n + 1 1 + 1 2 n + 1
263 ovex π 2 6 1 1 N 1 + 1 N V
264 257 262 263 fvmpt M K M = π 2 6 1 1 N 1 + 1 N
265 peano2cn N N + 1
266 68 265 syl M N + 1
267 266 68 69 divcld M N + 1 N
268 140 142 267 mulassd M π 2 6 2 M N N + 1 N = π 2 6 2 M N N + 1 N
269 68 148 68 69 divdird M N + 1 N = N N + 1 N
270 155 oveq1d M N N + 1 N = 1 + 1 N
271 269 270 eqtr2d M 1 + 1 N = N + 1 N
272 158 271 oveq12d M π 2 6 1 1 N 1 + 1 N = π 2 6 2 M N N + 1 N
273 177 oveq2d M π 2 2 M N + 1 N 2 6 = π 2 2 M N + 1 6 N 2
274 141 266 mulcld M 2 M N + 1
275 divmuldiv π 2 2 M N + 1 N 2 N 2 0 6 6 0 π 2 N 2 2 M N + 1 6 = π 2 2 M N + 1 N 2 6
276 180 274 183 185 275 syl22anc M π 2 N 2 2 M N + 1 6 = π 2 2 M N + 1 N 2 6
277 divmuldiv π 2 2 M N + 1 6 6 0 N 2 N 2 0 π 2 6 2 M N + 1 N 2 = π 2 2 M N + 1 6 N 2
278 180 274 185 183 277 syl22anc M π 2 6 2 M N + 1 N 2 = π 2 2 M N + 1 6 N 2
279 273 276 278 3eqtr4d M π 2 N 2 2 M N + 1 6 = π 2 6 2 M N + 1 N 2
280 80 recoscld M k 1 M cos k π N
281 280 recnd M k 1 M cos k π N
282 281 sqcld M k 1 M cos k π N 2
283 250 282 250 251 divdird M k 1 M sin k π N 2 + cos k π N 2 sin k π N 2 = sin k π N 2 sin k π N 2 + cos k π N 2 sin k π N 2
284 80 recnd M k 1 M k π N
285 sincossq k π N sin k π N 2 + cos k π N 2 = 1
286 284 285 syl M k 1 M sin k π N 2 + cos k π N 2 = 1
287 286 oveq1d M k 1 M sin k π N 2 + cos k π N 2 sin k π N 2 = 1 sin k π N 2
288 250 251 dividd M k 1 M sin k π N 2 sin k π N 2 = 1
289 223 simprd M k 1 M 0 < cos k π N
290 289 gt0ne0d M k 1 M cos k π N 0
291 tanval k π N cos k π N 0 tan k π N = sin k π N cos k π N
292 284 290 291 syl2anc M k 1 M tan k π N = sin k π N cos k π N
293 292 oveq1d M k 1 M tan k π N 2 = sin k π N cos k π N 2
294 246 281 290 sqdivd M k 1 M sin k π N cos k π N 2 = sin k π N 2 cos k π N 2
295 293 294 eqtrd M k 1 M tan k π N 2 = sin k π N 2 cos k π N 2
296 295 oveq2d M k 1 M 1 tan k π N 2 = 1 sin k π N 2 cos k π N 2
297 sqne0 cos k π N cos k π N 2 0 cos k π N 0
298 281 297 syl M k 1 M cos k π N 2 0 cos k π N 0
299 290 298 mpbird M k 1 M cos k π N 2 0
300 250 282 251 299 recdivd M k 1 M 1 sin k π N 2 cos k π N 2 = cos k π N 2 sin k π N 2
301 37 296 300 3eqtrrd M k 1 M cos k π N 2 sin k π N 2 = tan k π N 2
302 288 301 oveq12d M k 1 M sin k π N 2 sin k π N 2 + cos k π N 2 sin k π N 2 = 1 + tan k π N 2
303 283 287 302 3eqtr3d M k 1 M 1 sin k π N 2 = 1 + tan k π N 2
304 addcom 1 tan k π N 2 1 + tan k π N 2 = tan k π N 2 + 1
305 143 206 304 sylancr M k 1 M 1 + tan k π N 2 = tan k π N 2 + 1
306 248 303 305 3eqtrd M k 1 M sin k π N 2 = tan k π N 2 + 1
307 306 sumeq2dv M k = 1 M sin k π N 2 = k = 1 M tan k π N 2 + 1
308 1cnd M k 1 M 1
309 7 206 308 fsumadd M k = 1 M tan k π N 2 + 1 = k = 1 M tan k π N 2 + k = 1 M 1
310 fsumconst 1 M Fin 1 k = 1 M 1 = 1 M 1
311 7 143 310 sylancl M k = 1 M 1 = 1 M 1
312 nnnn0 M M 0
313 hashfz1 M 0 1 M = M
314 312 313 syl M 1 M = M
315 314 oveq1d M 1 M 1 = M 1
316 nncn M M
317 316 mulid1d M M 1 = M
318 311 315 317 3eqtrd M k = 1 M 1 = M
319 203 318 oveq12d M k = 1 M tan k π N 2 + k = 1 M 1 = 2 M 2 M 1 6 + M
320 307 309 319 3eqtrd M k = 1 M sin k π N 2 = 2 M 2 M 1 6 + M
321 3cn 3
322 321 a1i M 3
323 141 145 322 adddid M 2 M 2 M - 1 + 3 = 2 M 2 M 1 + 2 M 3
324 df-3 3 = 2 + 1
325 324 oveq1i 3 1 = 2 + 1 - 1
326 54 143 pncan3oi 2 + 1 - 1 = 2
327 325 326 163 3eqtri 3 1 = 1 + 1
328 327 oveq2i 2 M + 3 - 1 = 2 M + 1 + 1
329 141 148 322 subadd23d M 2 M - 1 + 3 = 2 M + 3 - 1
330 141 148 148 addassd M 2 M + 1 + 1 = 2 M + 1 + 1
331 328 329 330 3eqtr4a M 2 M - 1 + 3 = 2 M + 1 + 1
332 6 oveq1i N + 1 = 2 M + 1 + 1
333 331 332 eqtr4di M 2 M - 1 + 3 = N + 1
334 333 oveq2d M 2 M 2 M - 1 + 3 = 2 M N + 1
335 2cnd M 2
336 335 316 322 mul32d M 2 M 3 = 2 3 M
337 3t2e6 3 2 = 6
338 321 54 mulcomi 3 2 = 2 3
339 337 338 eqtr3i 6 = 2 3
340 339 oveq1i 6 M = 2 3 M
341 336 340 eqtr4di M 2 M 3 = 6 M
342 341 oveq2d M 2 M 2 M 1 + 2 M 3 = 2 M 2 M 1 + 6 M
343 323 334 342 3eqtr3d M 2 M N + 1 = 2 M 2 M 1 + 6 M
344 343 oveq1d M 2 M N + 1 6 = 2 M 2 M 1 + 6 M 6
345 mulcl 6 M 6 M
346 175 316 345 sylancr M 6 M
347 175 a1i M 6
348 113 a1i M 6 0
349 181 346 347 348 divdird M 2 M 2 M 1 + 6 M 6 = 2 M 2 M 1 6 + 6 M 6
350 316 347 348 divcan3d M 6 M 6 = M
351 350 oveq2d M 2 M 2 M 1 6 + 6 M 6 = 2 M 2 M 1 6 + M
352 344 349 351 3eqtrd M 2 M N + 1 6 = 2 M 2 M 1 6 + M
353 320 352 eqtr4d M k = 1 M sin k π N 2 = 2 M N + 1 6
354 192 353 oveq12d M π N 2 k = 1 M sin k π N 2 = π 2 N 2 2 M N + 1 6
355 141 68 266 68 69 69 divmuldivd M 2 M N N + 1 N = 2 M N + 1 N N
356 195 oveq2d M 2 M N + 1 N 2 = 2 M N + 1 N N
357 355 356 eqtr4d M 2 M N N + 1 N = 2 M N + 1 N 2
358 357 oveq2d M π 2 6 2 M N N + 1 N = π 2 6 2 M N + 1 N 2
359 279 354 358 3eqtr4d M π N 2 k = 1 M sin k π N 2 = π 2 6 2 M N N + 1 N
360 268 272 359 3eqtr4d M π 2 6 1 1 N 1 + 1 N = π N 2 k = 1 M sin k π N 2
361 226 recnd M k 1 M sin k π N 2
362 7 40 361 fsummulc2 M π N 2 k = 1 M sin k π N 2 = k = 1 M π N 2 sin k π N 2
363 264 360 362 3eqtrd M K M = k = 1 M π N 2 sin k π N 2
364 255 219 363 3brtr4d M F M K M
365 220 364 jca M J M F M F M K M