let n be Nat; :: thesis: rng (sqr (cot (x_r-seq n))) c= Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2))
set f = x_r-seq n;
set f1 = sqr (cot (x_r-seq n));
set PPn = <%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1);
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (sqr (cot (x_r-seq n))) or y in Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) )
assume y in rng (sqr (cot (x_r-seq n))) ; :: thesis: y in Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2))
then consider x being object such that
A1: ( x in dom (sqr (cot (x_r-seq n))) & (sqr (cot (x_r-seq n))) . x = y ) by FUNCT_1:def 3;
A2: len (sqr (cot (x_r-seq n))) = len (cot (x_r-seq n)) by CARD_1:def 7;
then A3: dom (sqr (cot (x_r-seq n))) = dom (cot (x_r-seq n)) by FINSEQ_3:29;
A4: dom (cot (x_r-seq n)) = dom (x_r-seq n) by BASEL_1:def 3;
reconsider x = x as Nat by A1;
A5: (cot (x_r-seq n)) . x = cot ((x_r-seq n) . x) by BASEL_1:def 3, A1, A3, A4;
cot ((x_r-seq n) . x) is Element of COMPLEX by XCMPLX_0:def 2;
then reconsider c = cot ((x_r-seq n) . x) as Element of F_Complex by COMPLFLD:def 1;
A6: c * c = ((cot (x_r-seq n)) . x) ^2 by A5
.= y by VALUED_1:11, A1 ;
set N = (2 * n) + 1;
A7: ((cot ((x_r-seq n) . x)) + <i>) |^ ((2 * n) + 1) is real

proof

( x in dom (x_r-seq n) & len (x_r-seq n) = n ) by BASEL_1:21, A2, FINSEQ_3:29, A4, A1;
then A8: ( 1 <= x & x <= n ) by FINSEQ_3:25;
then ( 0 < (x_r-seq n) . x & (x_r-seq n) . x < PI / 2 & PI / 2 < PI ) by BASEL_1:23, COMPTRIG:5;
then ( 0 < (x_r-seq n) . x & (x_r-seq n) . x < PI ) by XXREAL_0:2;
then (x_r-seq n) . x in ].0,PI.[ by XXREAL_1:4;
then sin . ((x_r-seq n) . x) > 0 by COMPTRIG:7;
then (<i> * (sin ((x_r-seq n) . x))) / (sin ((x_r-seq n) . x)) = <i> by XCMPLX_1:89;
then ((cot ((x_r-seq n) . x)) + <i>) |^ ((2 * n) + 1) = (((cos ((x_r-seq n) . x)) + (<i> * (sin ((x_r-seq n) . x)))) / (sin ((x_r-seq n) . x))) |^ ((2 * n) + 1)
.= (((cos ((x_r-seq n) . x)) + (<i> * (sin ((x_r-seq n) . x)))) |^ ((2 * n) + 1)) / ((sin ((x_r-seq n) . x)) |^ ((2 * n) + 1)) by PREPOWER:8
.= ((cos (((2 * n) + 1) * ((x_r-seq n) . x))) + (<i> * (sin (((2 * n) + 1) * ((x_r-seq n) . x))))) / ((sin ((x_r-seq n) . x)) |^ ((2 * n) + 1)) by COMPTRIG:53
.= ((cos (((2 * n) + 1) * ((x_r-seq n) . x))) + (<i> * (sin (x * PI)))) / ((sin ((x_r-seq n) . x)) |^ ((2 * n) + 1)) by A8, BASEL_1:25
.= ((cos (((2 * n) + 1) * ((x_r-seq n) . x))) + (<i> * 0)) / ((sin ((x_r-seq n) . x)) |^ ((2 * n) + 1)) by BASEL_1:13 ;
hence ((cot ((x_r-seq n) . x)) + <i>) |^ ((2 * n) + 1) is real ; :: thesis: verum

end;

A9: eval ((even_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c) = 0

proof

A10: (power F_Complex) . ((c + i_FC),((2 * n) + 1)) = ((cot ((x_r-seq n) . x)) + <i>) |^ ((2 * n) + 1) by COMPLFLD:74;
A11: 1. F_Complex is real by COMPLEX1:6, COMPLFLD:8;
even_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)) is imaginary by A11, Th17;
then A12: eval ((even_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c) is imaginary by Th14;
odd_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)) is real by Th17, A11;
then eval ((odd_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c) is real by Th15;
then A13: Im (eval ((odd_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c)) = 0 ;
A14: eval (<%i_FC,(1. F_Complex)%>,c) = i_FC + ((1. F_Complex) * c) by POLYNOM5:44
.= c + i_FC ;
A15: Im (eval ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),c)) = Im (((cot ((x_r-seq n) . x)) + <i>) |^ ((2 * n) + 1)) by A14, A10, POLYNOM5:22
.= 0 by A7 ;
Im (eval ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),c)) = (Im (eval ((odd_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c))) + (Im (eval ((even_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c)))

proof

reconsider ppn = <%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1) as Polynomial of F_Complex ;
<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1) = (odd_part ppn) + (even_part ppn) by HURWITZ2:10;
then eval ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),c) = (eval ((odd_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c)) + (eval ((even_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c)) by POLYNOM4:19;
hence Im (eval ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),c)) = (Im (eval ((odd_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c))) + (Im (eval ((even_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c))) by COMPLEX1:8; :: thesis: verum

end;

hence eval ((even_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1))),c) = 0 + (0 * <i>) by A15, A13, A12, COMPLEX1:13
.= 0 ;
:: thesis: verum

end;

set X2 = <%(0. F_Complex),(0. F_Complex),(1_ F_Complex)%>;
reconsider z1 = 0. F_Complex as Element of F_Complex ;
A16: eval (<%(0. F_Complex),(0. F_Complex),(1_ F_Complex)%>,c) = ((0. F_Complex) + (z1 * c)) + (((1_ F_Complex) * c) * c) by NIVEN:38
.= c * c ;
even_part (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)) = Subst ((sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)),<%(0. F_Complex),(0. F_Complex),(1_ F_Complex)%>) by Th22;
then eval ((sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)),(c * c)) = 0. F_Complex by A9, A16, POLYNOM5:53;
then c * c is_a_root_of sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2) by POLYNOM5:def 7;
hence y in Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) by A6, POLYNOM5:def 10; :: thesis: verum