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 \in ℕ ⟼ \frac{1}{2 n + 1})$
	basel.f	$⊢ F = seq 1 (+ (n \in ℕ ⟼ n^{- 2}))$
	basel.h	$⊢ H = (ℕ \times \{\frac{π^{2}}{6}\}) \times_{f} ((ℕ \times \{1\}) -_{f} G)$
	basel.j	$⊢ J = H \times_{f} ((ℕ \times \{1\}) +_{f} ((ℕ \times \{- 2\}) \times_{f} G))$
	basel.k	$⊢ K = H \times_{f} ((ℕ \times \{1\}) +_{f} G)$
	basellem8.n	$⊢ N = 2 \cdot M + 1$
Assertion	basellem8	$⊢ M \in ℕ \to (J (M) \leq F (M) \land F (M) \leq K (M))$

Proof

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

Metamath Proof Explorer

Theorem basellem8

Proof