# 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}=\left({n}\in ℕ⟼\frac{1}{2{n}+1}\right)$
basel.f ${⊢}{F}=seq1\left(+,\left({n}\in ℕ⟼{{n}}^{-2}\right)\right)$
basel.h ${⊢}{H}=\left(ℕ×\left\{\frac{{\mathrm{\pi }}^{2}}{6}\right\}\right){×}_{f}\left(\left(ℕ×\left\{1\right\}\right){-}_{f}{G}\right)$
basel.j ${⊢}{J}={H}{×}_{f}\left(\left(ℕ×\left\{1\right\}\right){+}_{f}\left(\left(ℕ×\left\{-2\right\}\right){×}_{f}{G}\right)\right)$
basel.k ${⊢}{K}={H}{×}_{f}\left(\left(ℕ×\left\{1\right\}\right){+}_{f}{G}\right)$
basellem8.n ${⊢}{N}=2\cdot {M}+1$
Assertion basellem8 ${⊢}{M}\in ℕ\to \left({J}\left({M}\right)\le {F}\left({M}\right)\wedge {F}\left({M}\right)\le {K}\left({M}\right)\right)$

### Proof

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