let n be Nat; 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 ; TARSKI:def 3 ( 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)))
; 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
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;
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
;
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; verum