let m be Nat; Sum (sqr (cot (x_r-seq m))) = ((2 * m) * ((2 * m) - 1)) / 6
set C = sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2);
set f = x_r-seq m;
A1:
sqr (cot (x_r-seq m)) is one-to-one
by BASEL_1:28;
A2:
( len (sqr (cot (x_r-seq m))) = len (cot (x_r-seq m)) & len (cot (x_r-seq m)) = len (x_r-seq m) & len (x_r-seq m) = m )
by CARD_1:def 7, BASEL_1:21;
per cases
( m = 0 or m >= 1 )
by NAT_1:14;
suppose A3:
m >= 1
;
Sum (sqr (cot (x_r-seq m))) = ((2 * m) * ((2 * m) - 1)) / 6then A4:
m + 1
>= 1
+ 1
by XREAL_1:7;
then A5:
(m + 1) -' 2
= (m + 1) - 2
by XREAL_1:233;
A6:
len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) = m + 1
by Th25;
A7:
len (sqr (cot (x_r-seq m))) = (len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2))) -' 1
by A6, A2, NAT_D:34;
A8:
Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) = rng (sqr (cot (x_r-seq m)))
by Th27;
then reconsider S =
sqr (cot (x_r-seq m)) as
FinSequence of
F_Complex by FINSEQ_1:def 4;
A9:
(
(len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2))) -' 1
= m &
(len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2))) -' 2
= m - 1 )
by A6, NAT_D:34, A5;
((2 * m) + 1) choose 1
= (2 * m) + 1
by STIRL2_1:51;
then A10:
(sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) . m =
((2 * m) + 1) * i_FC
by Th23
.=
((2 * m) + 1) * <i>
;
then A11:
(sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) . m <> 0. F_Complex
;
(sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) . (m - 1) =
(((2 * m) + 1) choose 3) * (- i_FC)
by Th24, A3
.=
(((2 * m) + 1) choose 3) * (- <i>)
by COMPLFLD:2
;
then A12:
((sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) . ((len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2))) -' 2)) / ((sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) . m) =
((((2 * m) + 1) choose 3) * (- <i>)) / (((2 * m) + 1) * <i>)
by A5, A6, A11, A10, COMPLFLD:6
.=
- (((((2 * m) + 1) choose 3) * <i>) / (((2 * m) + 1) * <i>))
.=
- ((((2 * m) + 1) choose 3) / ((2 * m) + 1))
by XCMPLX_1:91
.=
- ((((((2 * m) + 1) * (((2 * m) + 1) - 1)) * (((2 * m) + 1) - 2)) / 6) / ((2 * m) + 1))
by STIRL2_1:51
.=
- (((((2 * m) * ((2 * m) - 1)) / ((2 * m) + 1)) / 6) * ((2 * m) + 1))
.=
- (((2 * m) * ((2 * m) - 1)) / 6)
by XCMPLX_1:97
;
thus Sum (sqr (cot (x_r-seq m))) =
Sum S
by Th2
.=
SumRoots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2))
by A1, A7, A8, POLYVIE1:31
.=
- (((sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) . ((len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2))) -' 2)) / ((sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * m) + 1)),2)) . m))
by A4, A6, A9, POLYVIE1:32
.=
- (- (((2 * m) * ((2 * m) - 1)) / 6))
by A12, COMPLFLD:2
.=
((2 * m) * ((2 * m) - 1)) / 6
;
verum end;