deffunc H₁( non zero Nat) -> Polynomial of F_Complex = cyclotomic_poly $1;
set cPRFC = the carrier of (Polynom-Ring F_Complex);
set cFC = the carrier of F_Complex;
defpred S₁[ non zero Element of NAT ] means ( ( H₁($1) . 0 = 1 or H₁($1) . 0 = - 1 ) & ( for i being Element of NAT holds H₁($1) . i is integer ) );
A1: - (1_ F_Complex) = - 1 by COMPLFLD:2, COMPLFLD:8;

let k be non zero Element of NAT ; :: thesis:
assume A3: for n being non zero Element of NAT st n < k holds
S₁[n] ; :: thesis:
A4: 1 <= k by Lm1;

per cases by A4, XXREAL_0:1;

suppose A5: k = 1 ; :: thesis:

now :: thesis:

let i be Element of NAT ; :: thesis:

per cases by NAT_1:23;

suppose i = 0 ; :: thesis:

hence H₁(k) . i is integer by A1, A5, Th48, POLYNOM5:38; :: thesis:

end;

suppose i = 1 ; :: thesis:

hence H₁(k) . i is integer by A5, Th48, COMPLFLD:8, POLYNOM5:38; :: thesis:

end;

suppose i >= 2 ; :: thesis:

hence H₁(k) . i is integer by A5, Th48, COMPLFLD:7, POLYNOM5:38; :: thesis:

end;

hence S₁[k] by A1, A5, Th48, POLYNOM5:38; :: thesis:

end;

suppose A6: k > 1 ; :: thesis:

consider f being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that
A7: p = Product f and
A8: dom f = Seg k and
A9: for i being non zero Element of NAT st i in Seg k holds
( ( ( not i divides k or i = k ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides k & i <> k implies f . i = H₁(i) ) ) and
A10: unital_poly (F_Complex,k) = (cyclotomic_poly k) *' p by Th50;
defpred S₂[ Nat, object ] means ex g being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st
( g = f | (Seg $1) & p = Product g & $2 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) );
defpred S₃[ Nat] means ( $1 in Seg (len f) implies ex x being object st S₂[$1,x] );
A11: k = len f by A8, FINSEQ_1:def 3;
A12: for l being Nat st S₃[l] holds
S₃[l + 1]

proof

let l be Nat; :: thesis:
assume A13: S₃[l] ; :: thesis:
assume A14: l + 1 in Seg (len f) ; :: thesis:

per cases ;

suppose A15: l = 0 ; :: thesis:

reconsider fl1 = f . (l + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A8, A11, A14, FINSEQ_2:11;
reconsider g = f | (Seg (l + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
reconsider p = Product g as Polynomial of F_Complex by POLYNOM3:def 10;
<*> the carrier of (Polynom-Ring F_Complex) = f | (Seg 0) ;
then g = (<*> the carrier of (Polynom-Ring F_Complex)) ^ <*(f . (l + 1))*> by A8, A11, A14, A15, FINSEQ_5:10
.= <*(f . (l + 1))*> by FINSEQ_1:34 ;
then A16: p = fl1 by FINSOP_1:11;
take p ; :: thesis:
take g ; :: thesis:
take p ; :: thesis:
thus ( g = f | (Seg (l + 1)) & p = Product g & p = p ) ; :: thesis:
1 divides k by NAT_D:6;
then A17: f . 1 = H₁(1) by A6, A9, A11, A14, A15;
hence ( p . 0 = 1 or p . 0 = - 1 ) by A1, A15, A16, Th48, POLYNOM5:38; :: thesis:
let j be Element of NAT ; :: thesis:
thus p . j is integer :: thesis:

proof

per cases by NAT_1:23;

suppose j = 0 ; :: thesis:

hence p . j is integer by A1, A15, A16, A17, Th48, POLYNOM5:38; :: thesis:

end;

suppose j = 1 ; :: thesis:

hence p . j is integer by A15, A16, A17, Th48, COMPLFLD:8, POLYNOM5:38; :: thesis:

end;

suppose j >= 2 ; :: thesis:

hence p . j is integer by A15, A16, A17, Th48, COMPLFLD:7, POLYNOM5:38; :: thesis:

end;

suppose A18: 0 < l ; :: thesis:

( l + 1 <= len f & l <= l + 1 ) by A14, FINSEQ_1:1, NAT_1:12;
then A19: l <= len f by XXREAL_0:2;
0 + 1 <= l by A18, NAT_1:13;
then consider x being set such that
A20: S₂[l,x] by A13, A19, FINSEQ_1:1;
reconsider fl1 = f . (l + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A8, A11, A14, FINSEQ_2:11;
reconsider g1 = f | (Seg (l + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
reconsider p1 = Product g1 as Polynomial of F_Complex by POLYNOM3:def 10;
take p1 ; :: thesis:
take g1 ; :: thesis:
take p1 ; :: thesis:
thus ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 ) ; :: thesis:
reconsider fl1p = fl1 as Polynomial of F_Complex by POLYNOM3:def 10;
reconsider m1 = - 1 as Element of COMPLEX by XCMPLX_0:def 2;
consider g being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that
A21: g = f | (Seg l) and
A22: p = Product g and
x = p and
A23: ( p . 0 = 1 or p . 0 = - 1 ) and
A24: for j being Element of NAT holds p . j is integer by A20;
g1 = g ^ <*fl1*> by A8, A11, A14, A21, FINSEQ_5:10;
then Product g1 = (Product g) * fl1 by GROUP_4:6;
then A25: p1 = p *' fl1p by A22, POLYNOM3:def 10;
thus ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) :: thesis:

proof

per cases ;

suppose ( not l + 1 divides k or l + 1 = k ) ; :: thesis:

then A26: fl1p = <%(1_ F_Complex)%> by A9, A11, A14;
consider r being FinSequence of F_Complex such that
A27: len r = 0 + 1 and
A28: p1 . 0 = Sum r and
A29: for m being Element of NAT st m in dom r holds
r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by A25, POLYNOM3:def 9;
1 in dom r by A27, FINSEQ_3:25;
then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11;
r = <*r1*> by A27, FINSEQ_1:40;
then A30: p1 . 0 = r1 by A28, RLVECT_1:44;
1 in dom r by A27, FINSEQ_3:25;
then A31: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by A29, A30
.= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34
.= (p . 0) * (fl1p . 0) by NAT_D:34
.= (p . 0) * (1_ F_Complex) by A26, POLYNOM5:32 ;
thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) :: thesis:

proof

per cases by A23;

suppose p . 0 = 1 ; :: thesis:

hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A31; :: thesis:

end;

suppose p . 0 = - 1 ; :: thesis:

hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A31; :: thesis:

end;

let j be Element of NAT ; :: thesis:
consider r being FinSequence of F_Complex such that
len r = j + 1 and
A32: p1 . j = Sum r and
A33: for m being Element of NAT st m in dom r holds
r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by A25, POLYNOM3:def 9;
for i being Element of NAT st i in dom r holds
r . i is integer

proof

let i be Element of NAT ; :: thesis:
reconsider pi1 = p . (i -' 1) as Integer by A24;
set j1i = (j + 1) -' i;

now :: thesis:

A34: ( (j + 1) -' i = 0 or (j + 1) -' i >= 0 + 1 ) by NAT_1:13;

per cases ) -' i = 0 or (j + 1) -' i >= 1 ) by A34;

case (j + 1) -' i = 0 ; :: thesis:

hence fl1p . ((j + 1) -' i) = 1 by A26, COMPLFLD:8, POLYNOM5:32; :: thesis:

end;

case (j + 1) -' i >= 1 ; :: thesis:

hence fl1p . ((j + 1) -' i) = 0 by A26, COMPLFLD:7, POLYNOM5:32; :: thesis:

end;

then reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer ;
assume i in dom r ; :: thesis:
then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A33
.= pi1 * fl1pj1i ;
hence r . i is integer ; :: thesis:

end;

hence p1 . j is integer by A32, Th4; :: thesis:

end;

suppose A35: ( l + 1 divides k & l + 1 <> k ) ; :: thesis:

consider r being FinSequence of F_Complex such that
A36: len r = 0 + 1 and
A37: p1 . 0 = Sum r and
A38: for m being Element of NAT st m in dom r holds
r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by A25, POLYNOM3:def 9;
1 in dom r by A36, FINSEQ_3:25;
then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11;
r = <*r1*> by A36, FINSEQ_1:40;
then A39: p1 . 0 = r1 by A37, RLVECT_1:44;
1 in dom r by A36, FINSEQ_3:25;
then A40: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by A38, A39
.= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34
.= (p . 0) * (fl1p . 0) by NAT_D:34 ;
l + 1 <= k by A35, NAT_D:7;
then A41: l + 1 < k by A35, XXREAL_0:1;
A42: l + 1 in NAT by ORDINAL1:def 12;
A43: fl1p = H₁(l + 1) by A9, A11, A14, A35;
then reconsider fl1p0 = fl1p . 0 as Integer by A3, A41, A42;
A44: ( fl1p0 = 1 or fl1p0 = m1 ) by A3, A43, A41, A42;
thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) :: thesis:

proof

per cases by A23;

suppose p . 0 = 1 ; :: thesis:

hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A3, A43, A41, A40; :: thesis:

end;

suppose p . 0 = - 1 ; :: thesis:

hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A40, A44; :: thesis:

end;

let j be Element of NAT ; :: thesis:
consider r being FinSequence of F_Complex such that
len r = j + 1 and
A45: p1 . j = Sum r and
A46: for m being Element of NAT st m in dom r holds
r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by A25, POLYNOM3:def 9;
for i being Element of NAT st i in dom r holds
r . i is integer

proof

let i be Element of NAT ; :: thesis:
l + 1 in NAT by ORDINAL1:def 12;
then reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer by A3, A43, A41;
reconsider pi1 = p . (i -' 1) as Integer by A24;
assume i in dom r ; :: thesis:
then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A46
.= pi1 * fl1pj1i ;
hence r . i is integer ; :: thesis:

end;

hence p1 . j is integer by A45, Th4; :: thesis:

end;

defpred S₄[ Nat] means H₁(k) . $1 is integer ;
A47: (0 + 1) -' 1 = 0 by NAT_D:34;
A48: S₃[ 0 ] by FINSEQ_1:1;
for l being Nat holds S₃[l] from NAT_1:sch 2(A48, A12);
then A49: for l being Nat st l in Seg (len f) holds
ex x being object st S₂[l,x] ;
consider F being FinSequence such that
dom F = Seg (len f) and
A50: for i being Nat st i in Seg (len f) holds
S₂[i,F . i] from FINSEQ_1:sch 1(A49);
consider g being FinSequence of the carrier of (Polynom-Ring F_Complex), p1 being Polynomial of F_Complex such that
A51: ( g = f | (Seg k) & p1 = Product g ) and
F . k = p1 and
A52: ( p1 . 0 = 1 or p1 . 0 = - 1 ) and
A53: for j being Element of NAT holds p1 . j is integer by A11, A50, FINSEQ_1:3;
A54: p = p1 by A7, A11, A51, FINSEQ_3:49;

A55: now :: thesis:

let m be Nat; :: thesis:
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
consider r being FinSequence of the carrier of F_Complex such that
A56: len r = m + 1 and
A57: (unital_poly (F_Complex,k)) . m = Sum r and
A58: for l being Element of NAT st l in dom r holds
r . l = (p . (l -' 1)) * (H₁(k) . ((m1 + 1) -' l)) by A10, POLYNOM3:def 9;
reconsider Src = Sum r as Element of COMPLEX by COMPLFLD:def 1;

now :: thesis:

per cases ;

suppose m1 = 0 ; :: thesis:

hence Src is integer by A1, A57, Th38; :: thesis:

end;

suppose m1 = k ; :: thesis:

hence Src is integer by A57, Th38, COMPLFLD:8; :: thesis:

end;

suppose ( m1 <> 0 & m1 <> k ) ; :: thesis:

hence Src is integer by A57, Th39, COMPLFLD:7; :: thesis:

end;

then reconsider Sr = Src as Integer ;
A59: ((1,1) -cut r) ^ (((1 + 1),(len r)) -cut r) = r by A56, FINSEQ_6:135, NAT_1:11;
set s = ((1 + 1),(len r)) -cut r;
reconsider Ssc = Sum (((1 + 1),(len r)) -cut r) as Element of COMPLEX by COMPLFLD:def 1;
assume A60: for n being Nat st n < m holds
S₄[n] ; :: thesis:

now :: thesis:

let i be Element of NAT ; :: thesis:
assume A61: i in dom (((1 + 1),(len r)) -cut r) ; :: thesis:

per cases ;

suppose len r < 2 ; :: thesis:

then ((1 + 1),(len r)) -cut r = {} by FINSEQ_6:def 4;
hence (((1 + 1),(len r)) -cut r) . i is integer ; :: thesis:

end;

suppose A62: 1 + 1 <= len r ; :: thesis:

then A63: (len (((1 + 1),(len r)) -cut r)) + (1 + 1) = (len r) + 1 by FINSEQ_6:def 4;

per cases ;

suppose m = 0 ; :: thesis:

hence (((1 + 1),(len r)) -cut r) . i is integer by A56, A62; :: thesis:

end;

suppose A64: m > 0 ; :: thesis:

i <> 0 by A61, FINSEQ_3:25;
then reconsider cpkmi = H₁(k) . (m -' i) as Integer by A60, A64, NAT_2:9;
reconsider ppi = p . i as Integer by A53, A54;
i <> 0 by A61, FINSEQ_3:25;
then consider i1 being Nat such that
A65: i = i1 + 1 by NAT_1:6;
A66: i <= len (((1 + 1),(len r)) -cut r) by A61, FINSEQ_3:25;
then ( 1 <= i + 1 & i + 1 <= (len (((1 + 1),(len r)) -cut r)) + 1 ) by NAT_1:11, XREAL_1:6;
then 1 + i in dom r by A63, FINSEQ_3:25;
then A67: r . (1 + i) = (p . ((1 + i) -' 1)) * (H₁(k) . ((m + 1) -' (1 + i))) by A58
.= (p . ((i + 1) -' 1)) * (H₁(k) . (((m + 1) -' 1) -' i)) by NAT_2:30
.= (p . i) * (H₁(k) . (((m + 1) -' 1) -' i)) by NAT_D:34
.= ppi * cpkmi by NAT_D:34 ;
i1 < len (((1 + 1),(len r)) -cut r) by A66, A65, NAT_1:13;
then (((1 + 1),(len r)) -cut r) . i = r . ((1 + 1) + i1) by A62, A65, FINSEQ_6:def 4
.= r . (1 + i) by A65 ;
hence (((1 + 1),(len r)) -cut r) . i is integer by A67; :: thesis:

end;

then reconsider Ss = Ssc as Integer by Th4;
A68: 1 <= len r by A56, NAT_1:11;
then A69: 1 in dom r by FINSEQ_3:25;
then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11;
reconsider r1c = r1 as Element of COMPLEX by COMPLFLD:def 1;
(1,1) -cut r = <*r1*> by A68, FINSEQ_6:132;
then Sum r = r1 + (Sum (((1 + 1),(len r)) -cut r)) by A59, FVSUM_1:72;
then r1c = Sr - Ss ;
then reconsider r1i = r1 as Integer ;
A70: r1i = (p . (1 -' 1)) * (H₁(k) . ((m + 1) -' 1)) by A58, A69
.= (p . 0) * (H₁(k) . m1) by A47, NAT_D:34 ;

per cases by A7, A11, A51, A52, FINSEQ_3:49;

suppose p . 0 = 1 ; :: thesis:

hence S₄[m] by A70; :: thesis:

end;

suppose p . 0 = - 1 ; :: thesis:

then r1 = (- (1_ F_Complex)) * (H₁(k) . m1) by A70, COMPLFLD:2, COMPLFLD:8
.= - ((1_ F_Complex) * (H₁(k) . m1)) by VECTSP_1:9
.= - (H₁(k) . m1) ;
then 0. F_Complex = (- (H₁(k) . m1)) + (- r1) by RLVECT_1:def 10
.= (- r1) - (H₁(k) . m1) ;
then - r1 = H₁(k) . m by VECTSP_1:19;
then - r1i = H₁(k) . m by COMPLFLD:2;
hence S₄[m] ; :: thesis:

end;

A71: for i being Nat holds S₄[i] from NAT_1:sch 4(A55);
consider r being FinSequence of the carrier of F_Complex such that
A72: len r = 0 + 1 and
A73: (unital_poly (F_Complex,k)) . 0 = Sum r and
A74: for l being Element of NAT st l in dom r holds
r . l = (p . (l -' 1)) * (H₁(k) . ((0 + 1) -' l)) by A10, POLYNOM3:def 9;
A75: 1 in dom r by A72, FINSEQ_3:25;
then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11;
r = <*r1*> by A72, FINSEQ_1:40;
then A76: Sum r = r . 1 by RLVECT_1:44
.= (p . 0) * (H₁(k) . 0) by A74, A47, A75 ;
( H₁(k) . 0 = 1 or H₁(k) . 0 = - 1 )

proof

per cases by A7, A11, A51, A52, FINSEQ_3:49;

suppose p . 0 = 1 ; :: thesis:

hence ( H₁(k) . 0 = 1 or H₁(k) . 0 = - 1 ) by A1, A73, A76, Th38; :: thesis:

end;

suppose p . 0 = - 1 ; :: thesis:

then - (1_ F_Complex) = (- (1_ F_Complex)) * (H₁(k) . 0) by A1, A73, A76, Th38
.= - ((1_ F_Complex) * (H₁(k) . 0)) by VECTSP_1:9
.= - (H₁(k) . 0) ;
hence ( H₁(k) . 0 = 1 or H₁(k) . 0 = - 1 ) by COMPLFLD:8, RLVECT_1:18; :: thesis:

end;

hence S₁[k] by A71; :: thesis:

end;

for d being non zero Element of NAT holds S₁[d] from UNIROOTS:sch 1(A2);
hence for d being non zero Element of NAT
for i being Element of NAT holds
( ( (cyclotomic_poly d) . 0 = 1 or (cyclotomic_poly d) . 0 = - 1 ) & (cyclotomic_poly d) . i is integer ) ; :: thesis: