theorem Th27: :: BASEL_2:27

for n being Nat holds Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = rng (sqr (cot (x_r-seq n)))