let m be Nat; :: thesis:
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 by NAT_1:14;

suppose m = 0 ; :: thesis:

hence Sum (sqr (cot (x_r-seq m))) = ((2 * m) * ((2 * m) - 1)) / 6 by A2, RVSUM_1:72; :: thesis:

end;

suppose A3: m >= 1 ; :: thesis:

then 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 ; :: thesis:

end;

end;