basellem5

Description: Lemma for basel . Using vieta1 , we can calculate the sum of the roots of P as the quotient of the top two coefficients, and since the function T enumerates the roots, we are left with an equation that sums the cot ^ 2 function at the M different roots. (Contributed by Mario Carneiro, 29-Jul-2014)

	Ref	Expression
Hypotheses	basel.n	$⊢ N = 2 \cdot M + 1$
	basel.p	$⊢ P = (t \in ℂ ⟼ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j})$
	basel.t	$⊢ T = (n \in (1 \dots M) ⟼ {\tan (\frac{n π}{N})}^{- 2})$
Assertion	basellem5	$⊢ M \in ℕ \to \sum_{k = 1}^{M} {\tan (\frac{k π}{N})}^{- 2} = \frac{2 \cdot M (2 \cdot M - 1)}{6}$

Proof

Step	Hyp	Ref	Expression
1		basel.n	$⊢ N = 2 \cdot M + 1$
2		basel.p	$⊢ P = (t \in ℂ ⟼ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j})$
3		basel.t	$⊢ T = (n \in (1 \dots M) ⟼ {\tan (\frac{n π}{N})}^{- 2})$
4		eqid	$⊢ coeff (P) = coeff (P)$
5		eqid	$⊢ \deg (P) = \deg (P)$
6		eqid	$⊢ P^{-1} [\{0\}] = P^{-1} [\{0\}]$
7	1 2	basellem2	$⊢ M \in ℕ \to (P \in Poly (ℂ) \land \deg (P) = M \land coeff (P) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}))$
8	7	simp1d	$⊢ M \in ℕ \to P \in Poly (ℂ)$
9	7	simp2d	$⊢ M \in ℕ \to \deg (P) = M$
10		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
11		hashfz1	$⊢ M \in ℕ_{0} \to \|(1 \dots M)\| = M$
12	10 11	syl	$⊢ M \in ℕ \to \|(1 \dots M)\| = M$
13		fzfid	$⊢ M \in ℕ \to (1 \dots M) \in Fin$
14	1 2 3	basellem4	$⊢ M \in ℕ \to T : (1 \dots M) \underset{1-1 onto}{⟶} P^{-1} [\{0\}]$
15	13 14	hasheqf1od	$⊢ M \in ℕ \to \|(1 \dots M)\| = \|P^{-1} [\{0\}]\|$
16	9 12 15	3eqtr2rd	$⊢ M \in ℕ \to \|P^{-1} [\{0\}]\| = \deg (P)$
17		id	$⊢ M \in ℕ \to M \in ℕ$
18	9 17	eqeltrd	$⊢ M \in ℕ \to \deg (P) \in ℕ$
19	4 5 6 8 16 18	vieta1	$⊢ M \in ℕ \to \sum_{x \in P^{-1} [\{0\}]} x = - \frac{coeff (P) (\deg (P) - 1)}{coeff (P) (\deg (P))}$
20		id	$⊢ x = {\tan (\frac{k π}{N})}^{- 2} \to x = {\tan (\frac{k π}{N})}^{- 2}$
21		oveq1	$⊢ n = k \to n π = k π$
22	21	fvoveq1d	$⊢ n = k \to \tan (\frac{n π}{N}) = \tan (\frac{k π}{N})$
23	22	oveq1d	$⊢ n = k \to {\tan (\frac{n π}{N})}^{- 2} = {\tan (\frac{k π}{N})}^{- 2}$
24		ovex	$⊢ {\tan (\frac{k π}{N})}^{- 2} \in V$
25	23 3 24	fvmpt	$⊢ k \in (1 \dots M) \to T (k) = {\tan (\frac{k π}{N})}^{- 2}$
26	25	adantl	$⊢ (M \in ℕ \land k \in (1 \dots M)) \to T (k) = {\tan (\frac{k π}{N})}^{- 2}$
27		cnvimass	$⊢ P^{-1} [\{0\}] \subseteq dom P$
28		plyf	$⊢ P \in Poly (ℂ) \to P : ℂ ⟶ ℂ$
29		fdm	$⊢ P : ℂ ⟶ ℂ \to dom P = ℂ$
30	8 28 29	3syl	$⊢ M \in ℕ \to dom P = ℂ$
31	27 30	sseqtrid	$⊢ M \in ℕ \to P^{-1} [\{0\}] \subseteq ℂ$
32	31	sselda	$⊢ (M \in ℕ \land x \in P^{-1} [\{0\}]) \to x \in ℂ$
33	20 13 14 26 32	fsumf1o	$⊢ M \in ℕ \to \sum_{x \in P^{-1} [\{0\}]} x = \sum_{k = 1}^{M} {\tan (\frac{k π}{N})}^{- 2}$
34	7	simp3d	$⊢ M \in ℕ \to coeff (P) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n})$
35	9	oveq1d	$⊢ M \in ℕ \to \deg (P) - 1 = M - 1$
36	34 35	fveq12d	$⊢ M \in ℕ \to coeff (P) (\deg (P) - 1) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M - 1)$
37		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
38		oveq2	$⊢ n = M - 1 \to 2 n = 2 (M - 1)$
39	38	oveq2d	$⊢ n = M - 1 \to (\binom{N}{2 n}) = (\binom{N}{2 (M - 1)})$
40		oveq2	$⊢ n = M - 1 \to M - n = M - (M - 1)$
41	40	oveq2d	$⊢ n = M - 1 \to {(- 1)}^{M - n} = {(- 1)}^{M - (M - 1)}$
42	39 41	oveq12d	$⊢ n = M - 1 \to (\binom{N}{2 n}) {(- 1)}^{M - n} = (\binom{N}{2 (M - 1)}) {(- 1)}^{M - (M - 1)}$
43		eqid	$⊢ (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n})$
44		ovex	$⊢ (\binom{N}{2 (M - 1)}) {(- 1)}^{M - (M - 1)} \in V$
45	42 43 44	fvmpt	$⊢ M - 1 \in ℕ_{0} \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M - 1) = (\binom{N}{2 (M - 1)}) {(- 1)}^{M - (M - 1)}$
46	37 45	syl	$⊢ M \in ℕ \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M - 1) = (\binom{N}{2 (M - 1)}) {(- 1)}^{M - (M - 1)}$
47		nncn	$⊢ M \in ℕ \to M \in ℂ$
48		ax-1cn	$⊢ 1 \in ℂ$
49		nncan	$⊢ (M \in ℂ \land 1 \in ℂ) \to M - (M - 1) = 1$
50	47 48 49	sylancl	$⊢ M \in ℕ \to M - (M - 1) = 1$
51	50	oveq2d	$⊢ M \in ℕ \to {(- 1)}^{M - (M - 1)} = {(- 1)}^{1}$
52		neg1cn	$⊢ - 1 \in ℂ$
53		exp1	$⊢ - 1 \in ℂ \to {(- 1)}^{1} = - 1$
54	52 53	ax-mp	$⊢ {(- 1)}^{1} = - 1$
55	51 54	syl6eq	$⊢ M \in ℕ \to {(- 1)}^{M - (M - 1)} = - 1$
56	55	oveq2d	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) {(- 1)}^{M - (M - 1)} = (\binom{N}{2 (M - 1)}) -1$
57		2nn	$⊢ 2 \in ℕ$
58		nnmulcl	$⊢ (2 \in ℕ \land M \in ℕ) \to 2 \cdot M \in ℕ$
59	57 58	mpan	$⊢ M \in ℕ \to 2 \cdot M \in ℕ$
60	59	peano2nnd	$⊢ M \in ℕ \to 2 \cdot M + 1 \in ℕ$
61	1 60	eqeltrid	$⊢ M \in ℕ \to N \in ℕ$
62	61	nnnn0d	$⊢ M \in ℕ \to N \in ℕ_{0}$
63		2z	$⊢ 2 \in ℤ$
64		nnz	$⊢ M \in ℕ \to M \in ℤ$
65		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
66	64 65	syl	$⊢ M \in ℕ \to M - 1 \in ℤ$
67		zmulcl	$⊢ (2 \in ℤ \land M - 1 \in ℤ) \to 2 (M - 1) \in ℤ$
68	63 66 67	sylancr	$⊢ M \in ℕ \to 2 (M - 1) \in ℤ$
69		bccl	$⊢ (N \in ℕ_{0} \land 2 (M - 1) \in ℤ) \to (\binom{N}{2 (M - 1)}) \in ℕ_{0}$
70	62 68 69	syl2anc	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) \in ℕ_{0}$
71	70	nn0cnd	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) \in ℂ$
72		mulcom	$⊢ ((\binom{N}{2 (M - 1)}) \in ℂ \land - 1 \in ℂ) \to (\binom{N}{2 (M - 1)}) -1 = -1 (\binom{N}{2 (M - 1)})$
73	71 52 72	sylancl	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) -1 = -1 (\binom{N}{2 (M - 1)})$
74	71	mulm1d	$⊢ M \in ℕ \to -1 (\binom{N}{2 (M - 1)}) = - (\binom{N}{2 (M - 1)})$
75	56 73 74	3eqtrd	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) {(- 1)}^{M - (M - 1)} = - (\binom{N}{2 (M - 1)})$
76	36 46 75	3eqtrd	$⊢ M \in ℕ \to coeff (P) (\deg (P) - 1) = - (\binom{N}{2 (M - 1)})$
77	71	negcld	$⊢ M \in ℕ \to - (\binom{N}{2 (M - 1)}) \in ℂ$
78	76 77	eqeltrd	$⊢ M \in ℕ \to coeff (P) (\deg (P) - 1) \in ℂ$
79	34 9	fveq12d	$⊢ M \in ℕ \to coeff (P) (\deg (P)) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M)$
80		oveq2	$⊢ n = M \to 2 n = 2 \cdot M$
81	80	oveq2d	$⊢ n = M \to (\binom{N}{2 n}) = (\binom{N}{2 \cdot M})$
82		oveq2	$⊢ n = M \to M - n = M - M$
83	82	oveq2d	$⊢ n = M \to {(- 1)}^{M - n} = {(- 1)}^{M - M}$
84	81 83	oveq12d	$⊢ n = M \to (\binom{N}{2 n}) {(- 1)}^{M - n} = (\binom{N}{2 \cdot M}) {(- 1)}^{M - M}$
85		ovex	$⊢ (\binom{N}{2 \cdot M}) {(- 1)}^{M - M} \in V$
86	84 43 85	fvmpt	$⊢ M \in ℕ_{0} \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M) = (\binom{N}{2 \cdot M}) {(- 1)}^{M - M}$
87	10 86	syl	$⊢ M \in ℕ \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M) = (\binom{N}{2 \cdot M}) {(- 1)}^{M - M}$
88	47	subidd	$⊢ M \in ℕ \to M - M = 0$
89	88	oveq2d	$⊢ M \in ℕ \to {(- 1)}^{M - M} = {(- 1)}^{0}$
90		exp0	$⊢ - 1 \in ℂ \to {(- 1)}^{0} = 1$
91	52 90	ax-mp	$⊢ {(- 1)}^{0} = 1$
92	89 91	syl6eq	$⊢ M \in ℕ \to {(- 1)}^{M - M} = 1$
93	92	oveq2d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) {(- 1)}^{M - M} = (\binom{N}{2 \cdot M}) \cdot 1$
94		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
95	59	nnred	$⊢ M \in ℕ \to 2 \cdot M \in ℝ$
96	95	lep1d	$⊢ M \in ℕ \to 2 \cdot M \leq 2 \cdot M + 1$
97	96 1	breqtrrdi	$⊢ M \in ℕ \to 2 \cdot M \leq N$
98		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
99	59 98	eleqtrdi	$⊢ M \in ℕ \to 2 \cdot M \in ℤ_{\geq 1}$
100	61	nnzd	$⊢ M \in ℕ \to N \in ℤ$
101		elfz5	$⊢ (2 \cdot M \in ℤ_{\geq 1} \land N \in ℤ) \to (2 \cdot M \in (1 \dots N) \leftrightarrow 2 \cdot M \leq N)$
102	99 100 101	syl2anc	$⊢ M \in ℕ \to (2 \cdot M \in (1 \dots N) \leftrightarrow 2 \cdot M \leq N)$
103	97 102	mpbird	$⊢ M \in ℕ \to 2 \cdot M \in (1 \dots N)$
104	94 103	sseldi	$⊢ M \in ℕ \to 2 \cdot M \in (0 \dots N)$
105		bccl2	$⊢ 2 \cdot M \in (0 \dots N) \to (\binom{N}{2 \cdot M}) \in ℕ$
106	104 105	syl	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) \in ℕ$
107	106	nncnd	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) \in ℂ$
108	107	mulid1d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) \cdot 1 = (\binom{N}{2 \cdot M})$
109	93 108	eqtrd	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) {(- 1)}^{M - M} = (\binom{N}{2 \cdot M})$
110	79 87 109	3eqtrd	$⊢ M \in ℕ \to coeff (P) (\deg (P)) = (\binom{N}{2 \cdot M})$
111	110 107	eqeltrd	$⊢ M \in ℕ \to coeff (P) (\deg (P)) \in ℂ$
112	106	nnne0d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) \neq 0$
113	110 112	eqnetrd	$⊢ M \in ℕ \to coeff (P) (\deg (P)) \neq 0$
114	78 111 113	divnegd	$⊢ M \in ℕ \to - \frac{coeff (P) (\deg (P) - 1)}{coeff (P) (\deg (P))} = \frac{- coeff (P) (\deg (P) - 1)}{coeff (P) (\deg (P))}$
115	76	negeqd	$⊢ M \in ℕ \to - coeff (P) (\deg (P) - 1) = - (- (\binom{N}{2 (M - 1)}))$
116	71	negnegd	$⊢ M \in ℕ \to - (- (\binom{N}{2 (M - 1)})) = (\binom{N}{2 (M - 1)})$
117	115 116	eqtrd	$⊢ M \in ℕ \to - coeff (P) (\deg (P) - 1) = (\binom{N}{2 (M - 1)})$
118	117 110	oveq12d	$⊢ M \in ℕ \to \frac{- coeff (P) (\deg (P) - 1)}{coeff (P) (\deg (P))} = \frac{(\binom{N}{2 (M - 1)})}{(\binom{N}{2 \cdot M})}$
119		bcm1k	$⊢ 2 \cdot M \in (1 \dots N) \to (\binom{N}{2 \cdot M}) = (\binom{N}{2 \cdot M - 1}) (\frac{N - (2 \cdot M - 1)}{2 \cdot M})$
120	103 119	syl	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) = (\binom{N}{2 \cdot M - 1}) (\frac{N - (2 \cdot M - 1)}{2 \cdot M})$
121	59	nncnd	$⊢ M \in ℕ \to 2 \cdot M \in ℂ$
122		1cnd	$⊢ M \in ℕ \to 1 \in ℂ$
123	121 122 122	pnncand	$⊢ M \in ℕ \to 2 \cdot M + 1 - (2 \cdot M - 1) = 1 + 1$
124	1	oveq1i	$⊢ N - (2 \cdot M - 1) = 2 \cdot M + 1 - (2 \cdot M - 1)$
125		df-2	$⊢ 2 = 1 + 1$
126	123 124 125	3eqtr4g	$⊢ M \in ℕ \to N - (2 \cdot M - 1) = 2$
127		2nn0	$⊢ 2 \in ℕ_{0}$
128	126 127	eqeltrdi	$⊢ M \in ℕ \to N - (2 \cdot M - 1) \in ℕ_{0}$
129		nnm1nn0	$⊢ 2 \cdot M \in ℕ \to 2 \cdot M - 1 \in ℕ_{0}$
130	59 129	syl	$⊢ M \in ℕ \to 2 \cdot M - 1 \in ℕ_{0}$
131		nn0sub	$⊢ (2 \cdot M - 1 \in ℕ_{0} \land N \in ℕ_{0}) \to (2 \cdot M - 1 \leq N \leftrightarrow N - (2 \cdot M - 1) \in ℕ_{0})$
132	130 62 131	syl2anc	$⊢ M \in ℕ \to (2 \cdot M - 1 \leq N \leftrightarrow N - (2 \cdot M - 1) \in ℕ_{0})$
133	128 132	mpbird	$⊢ M \in ℕ \to 2 \cdot M - 1 \leq N$
134	47	2timesd	$⊢ M \in ℕ \to 2 \cdot M = M + M$
135	134	oveq1d	$⊢ M \in ℕ \to 2 \cdot M - 1 = M + M - 1$
136	47 47 122	addsubd	$⊢ M \in ℕ \to M + M - 1 = M - 1 + M$
137	135 136	eqtrd	$⊢ M \in ℕ \to 2 \cdot M - 1 = M - 1 + M$
138		nn0nnaddcl	$⊢ (M - 1 \in ℕ_{0} \land M \in ℕ) \to M - 1 + M \in ℕ$
139	37 138	mpancom	$⊢ M \in ℕ \to M - 1 + M \in ℕ$
140	137 139	eqeltrd	$⊢ M \in ℕ \to 2 \cdot M - 1 \in ℕ$
141	140 98	eleqtrdi	$⊢ M \in ℕ \to 2 \cdot M - 1 \in ℤ_{\geq 1}$
142		elfz5	$⊢ (2 \cdot M - 1 \in ℤ_{\geq 1} \land N \in ℤ) \to (2 \cdot M - 1 \in (1 \dots N) \leftrightarrow 2 \cdot M - 1 \leq N)$
143	141 100 142	syl2anc	$⊢ M \in ℕ \to (2 \cdot M - 1 \in (1 \dots N) \leftrightarrow 2 \cdot M - 1 \leq N)$
144	133 143	mpbird	$⊢ M \in ℕ \to 2 \cdot M - 1 \in (1 \dots N)$
145		bcm1k	$⊢ 2 \cdot M - 1 \in (1 \dots N) \to (\binom{N}{2 \cdot M - 1}) = (\binom{N}{2 \cdot M - 1 - 1}) (\frac{N - (2 \cdot M - 1 - 1)}{2 \cdot M - 1})$
146	144 145	syl	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M - 1}) = (\binom{N}{2 \cdot M - 1 - 1}) (\frac{N - (2 \cdot M - 1 - 1)}{2 \cdot M - 1})$
147	48	2timesi	$⊢ 2 \cdot 1 = 1 + 1$
148	147	eqcomi	$⊢ 1 + 1 = 2 \cdot 1$
149	148	oveq2i	$⊢ 2 \cdot M - (1 + 1) = 2 \cdot M - 2 \cdot 1$
150	121 122 122	subsub4d	$⊢ M \in ℕ \to 2 \cdot M - 1 - 1 = 2 \cdot M - (1 + 1)$
151		2cnd	$⊢ M \in ℕ \to 2 \in ℂ$
152	151 47 122	subdid	$⊢ M \in ℕ \to 2 (M - 1) = 2 \cdot M - 2 \cdot 1$
153	149 150 152	3eqtr4a	$⊢ M \in ℕ \to 2 \cdot M - 1 - 1 = 2 (M - 1)$
154	153	oveq2d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M - 1 - 1}) = (\binom{N}{2 (M - 1)})$
155	61	nncnd	$⊢ M \in ℕ \to N \in ℂ$
156	140	nncnd	$⊢ M \in ℕ \to 2 \cdot M - 1 \in ℂ$
157	155 156 122	subsubd	$⊢ M \in ℕ \to N - (2 \cdot M - 1 - 1) = N - (2 \cdot M - 1) + 1$
158	126	oveq1d	$⊢ M \in ℕ \to N - (2 \cdot M - 1) + 1 = 2 + 1$
159		df-3	$⊢ 3 = 2 + 1$
160	158 159	syl6eqr	$⊢ M \in ℕ \to N - (2 \cdot M - 1) + 1 = 3$
161	157 160	eqtrd	$⊢ M \in ℕ \to N - (2 \cdot M - 1 - 1) = 3$
162	161	oveq1d	$⊢ M \in ℕ \to \frac{N - (2 \cdot M - 1 - 1)}{2 \cdot M - 1} = \frac{3}{2 \cdot M - 1}$
163	154 162	oveq12d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M - 1 - 1}) (\frac{N - (2 \cdot M - 1 - 1)}{2 \cdot M - 1}) = (\binom{N}{2 (M - 1)}) (\frac{3}{2 \cdot M - 1})$
164	146 163	eqtrd	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M - 1}) = (\binom{N}{2 (M - 1)}) (\frac{3}{2 \cdot M - 1})$
165	126	oveq1d	$⊢ M \in ℕ \to \frac{N - (2 \cdot M - 1)}{2 \cdot M} = \frac{2}{2 \cdot M}$
166	164 165	oveq12d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M - 1}) (\frac{N - (2 \cdot M - 1)}{2 \cdot M}) = (\binom{N}{2 (M - 1)}) (\frac{3}{2 \cdot M - 1}) (\frac{2}{2 \cdot M})$
167		3re	$⊢ 3 \in ℝ$
168		nndivre	$⊢ (3 \in ℝ \land 2 \cdot M - 1 \in ℕ) \to \frac{3}{2 \cdot M - 1} \in ℝ$
169	167 140 168	sylancr	$⊢ M \in ℕ \to \frac{3}{2 \cdot M - 1} \in ℝ$
170	169	recnd	$⊢ M \in ℕ \to \frac{3}{2 \cdot M - 1} \in ℂ$
171		2re	$⊢ 2 \in ℝ$
172		nndivre	$⊢ (2 \in ℝ \land 2 \cdot M \in ℕ) \to \frac{2}{2 \cdot M} \in ℝ$
173	171 59 172	sylancr	$⊢ M \in ℕ \to \frac{2}{2 \cdot M} \in ℝ$
174	173	recnd	$⊢ M \in ℕ \to \frac{2}{2 \cdot M} \in ℂ$
175	71 170 174	mulassd	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) (\frac{3}{2 \cdot M - 1}) (\frac{2}{2 \cdot M}) = (\binom{N}{2 (M - 1)}) (\frac{3}{2 \cdot M - 1}) (\frac{2}{2 \cdot M})$
176	120 166 175	3eqtrd	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) = (\binom{N}{2 (M - 1)}) (\frac{3}{2 \cdot M - 1}) (\frac{2}{2 \cdot M})$
177		3cn	$⊢ 3 \in ℂ$
178	177	a1i	$⊢ M \in ℕ \to 3 \in ℂ$
179	140	nnne0d	$⊢ M \in ℕ \to 2 \cdot M - 1 \neq 0$
180	59	nnne0d	$⊢ M \in ℕ \to 2 \cdot M \neq 0$
181	178 156 151 121 179 180	divmuldivd	$⊢ M \in ℕ \to (\frac{3}{2 \cdot M - 1}) (\frac{2}{2 \cdot M}) = \frac{3 \cdot 2}{(2 \cdot M - 1) 2 \cdot M}$
182		3t2e6	$⊢ 3 \cdot 2 = 6$
183	182	a1i	$⊢ M \in ℕ \to 3 \cdot 2 = 6$
184	156 121	mulcomd	$⊢ M \in ℕ \to (2 \cdot M - 1) 2 \cdot M = 2 \cdot M (2 \cdot M - 1)$
185	183 184	oveq12d	$⊢ M \in ℕ \to \frac{3 \cdot 2}{(2 \cdot M - 1) 2 \cdot M} = \frac{6}{2 \cdot M (2 \cdot M - 1)}$
186	181 185	eqtrd	$⊢ M \in ℕ \to (\frac{3}{2 \cdot M - 1}) (\frac{2}{2 \cdot M}) = \frac{6}{2 \cdot M (2 \cdot M - 1)}$
187	186	oveq2d	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) (\frac{3}{2 \cdot M - 1}) (\frac{2}{2 \cdot M}) = (\binom{N}{2 (M - 1)}) (\frac{6}{2 \cdot M (2 \cdot M - 1)})$
188	176 187	eqtrd	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) = (\binom{N}{2 (M - 1)}) (\frac{6}{2 \cdot M (2 \cdot M - 1)})$
189	188	oveq1d	$⊢ M \in ℕ \to \frac{(\binom{N}{2 \cdot M})}{(\binom{N}{2 (M - 1)})} = \frac{(\binom{N}{2 (M - 1)}) (\frac{6}{2 \cdot M (2 \cdot M - 1)})}{(\binom{N}{2 (M - 1)})}$
190		6re	$⊢ 6 \in ℝ$
191	59 140	nnmulcld	$⊢ M \in ℕ \to 2 \cdot M (2 \cdot M - 1) \in ℕ$
192		nndivre	$⊢ (6 \in ℝ \land 2 \cdot M (2 \cdot M - 1) \in ℕ) \to \frac{6}{2 \cdot M (2 \cdot M - 1)} \in ℝ$
193	190 191 192	sylancr	$⊢ M \in ℕ \to \frac{6}{2 \cdot M (2 \cdot M - 1)} \in ℝ$
194	193	recnd	$⊢ M \in ℕ \to \frac{6}{2 \cdot M (2 \cdot M - 1)} \in ℂ$
195		nnm1nn0	$⊢ 2 \cdot M - 1 \in ℕ \to 2 \cdot M - 1 - 1 \in ℕ_{0}$
196	140 195	syl	$⊢ M \in ℕ \to 2 \cdot M - 1 - 1 \in ℕ_{0}$
197	153 196	eqeltrrd	$⊢ M \in ℕ \to 2 (M - 1) \in ℕ_{0}$
198	197	nn0red	$⊢ M \in ℕ \to 2 (M - 1) \in ℝ$
199	140	nnred	$⊢ M \in ℕ \to 2 \cdot M - 1 \in ℝ$
200	61	nnred	$⊢ M \in ℕ \to N \in ℝ$
201	199	ltm1d	$⊢ M \in ℕ \to 2 \cdot M - 1 - 1 < 2 \cdot M - 1$
202	153 201	eqbrtrrd	$⊢ M \in ℕ \to 2 (M - 1) < 2 \cdot M - 1$
203	198 199 202	ltled	$⊢ M \in ℕ \to 2 (M - 1) \leq 2 \cdot M - 1$
204	198 199 200 203 133	letrd	$⊢ M \in ℕ \to 2 (M - 1) \leq N$
205		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
206	197 205	eleqtrdi	$⊢ M \in ℕ \to 2 (M - 1) \in ℤ_{\geq 0}$
207		elfz5	$⊢ (2 (M - 1) \in ℤ_{\geq 0} \land N \in ℤ) \to (2 (M - 1) \in (0 \dots N) \leftrightarrow 2 (M - 1) \leq N)$
208	206 100 207	syl2anc	$⊢ M \in ℕ \to (2 (M - 1) \in (0 \dots N) \leftrightarrow 2 (M - 1) \leq N)$
209	204 208	mpbird	$⊢ M \in ℕ \to 2 (M - 1) \in (0 \dots N)$
210		bccl2	$⊢ 2 (M - 1) \in (0 \dots N) \to (\binom{N}{2 (M - 1)}) \in ℕ$
211	209 210	syl	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) \in ℕ$
212	211	nnne0d	$⊢ M \in ℕ \to (\binom{N}{2 (M - 1)}) \neq 0$
213	194 71 212	divcan3d	$⊢ M \in ℕ \to \frac{(\binom{N}{2 (M - 1)}) (\frac{6}{2 \cdot M (2 \cdot M - 1)})}{(\binom{N}{2 (M - 1)})} = \frac{6}{2 \cdot M (2 \cdot M - 1)}$
214	189 213	eqtrd	$⊢ M \in ℕ \to \frac{(\binom{N}{2 \cdot M})}{(\binom{N}{2 (M - 1)})} = \frac{6}{2 \cdot M (2 \cdot M - 1)}$
215	214	oveq2d	$⊢ M \in ℕ \to \frac{1}{\frac{(\binom{N}{2 \cdot M})}{(\binom{N}{2 (M - 1)})}} = \frac{1}{\frac{6}{2 \cdot M (2 \cdot M - 1)}}$
216	107 71 112 212	recdivd	$⊢ M \in ℕ \to \frac{1}{\frac{(\binom{N}{2 \cdot M})}{(\binom{N}{2 (M - 1)})}} = \frac{(\binom{N}{2 (M - 1)})}{(\binom{N}{2 \cdot M})}$
217	191	nncnd	$⊢ M \in ℕ \to 2 \cdot M (2 \cdot M - 1) \in ℂ$
218	191	nnne0d	$⊢ M \in ℕ \to 2 \cdot M (2 \cdot M - 1) \neq 0$
219		6cn	$⊢ 6 \in ℂ$
220		6nn	$⊢ 6 \in ℕ$
221	220	nnne0i	$⊢ 6 \neq 0$
222		recdiv	$⊢ ((6 \in ℂ \land 6 \neq 0) \land (2 \cdot M (2 \cdot M - 1) \in ℂ \land 2 \cdot M (2 \cdot M - 1) \neq 0)) \to \frac{1}{\frac{6}{2 \cdot M (2 \cdot M - 1)}} = \frac{2 \cdot M (2 \cdot M - 1)}{6}$
223	219 221 222	mpanl12	$⊢ (2 \cdot M (2 \cdot M - 1) \in ℂ \land 2 \cdot M (2 \cdot M - 1) \neq 0) \to \frac{1}{\frac{6}{2 \cdot M (2 \cdot M - 1)}} = \frac{2 \cdot M (2 \cdot M - 1)}{6}$
224	217 218 223	syl2anc	$⊢ M \in ℕ \to \frac{1}{\frac{6}{2 \cdot M (2 \cdot M - 1)}} = \frac{2 \cdot M (2 \cdot M - 1)}{6}$
225	215 216 224	3eqtr3d	$⊢ M \in ℕ \to \frac{(\binom{N}{2 (M - 1)})}{(\binom{N}{2 \cdot M})} = \frac{2 \cdot M (2 \cdot M - 1)}{6}$
226	114 118 225	3eqtrd	$⊢ M \in ℕ \to - \frac{coeff (P) (\deg (P) - 1)}{coeff (P) (\deg (P))} = \frac{2 \cdot M (2 \cdot M - 1)}{6}$
227	19 33 226	3eqtr3d	$⊢ M \in ℕ \to \sum_{k = 1}^{M} {\tan (\frac{k π}{N})}^{- 2} = \frac{2 \cdot M (2 \cdot M - 1)}{6}$

Metamath Proof Explorer

Theorem basellem5

Proof