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

Metamath Proof Explorer

Theorem basellem8

Proof