let n be non empty Element of NAT ; :: thesis: ( 1 < n implies for q being Element of NAT st 1 < q holds
for qc being Element of F_Complex st qc = q holds
for i being Integer st i = eval (cyclotomic_poly n),qc holds
abs i > q - 1 )
assume A1: 1 < n ; :: thesis: for q being Element of NAT st 1 < q holds
for qc being Element of F_Complex st qc = q holds
for i being Integer st i = eval (cyclotomic_poly n),qc holds
abs i > q - 1
set cMGFC = the carrier of (MultGroup F_Complex );
set MGFC = MultGroup F_Complex ;
let q be Element of NAT ; :: thesis: ( 1 < q implies for qc being Element of F_Complex st qc = q holds
for i being Integer st i = eval (cyclotomic_poly n),qc holds
abs i > q - 1 )
assume A2: 1 < q ; :: thesis: for qc being Element of F_Complex st qc = q holds
for i being Integer st i = eval (cyclotomic_poly n),qc holds
abs i > q - 1
let qc be Element of F_Complex ; :: thesis: ( qc = q implies for i being Integer st i = eval (cyclotomic_poly n),qc holds
abs i > q - 1 )
assume A3: qc = q ; :: thesis: for i being Integer st i = eval (cyclotomic_poly n),qc holds
abs i > q - 1
let i be Integer; :: thesis: ( i = eval (cyclotomic_poly n),qc implies abs i > q - 1 )
assume A4: i = eval (cyclotomic_poly n),qc ; :: thesis: abs i > q - 1
reconsider qi = q as Integer ;
1 + 1 <= qi by A2, INT_1:20;
then A5: (1 + 1) + (- 1) <= qi + (- 1) by XREAL_1:9;
consider S being non empty finite Subset of F_Complex such that
A6: S = { y where y is Element of the carrier of (MultGroup F_Complex ) : ord y = n } and
A7: cyclotomic_poly n = poly_with_roots (S,1 -bag ) by Def5;
rng (canFS S) = S by FUNCT_2:def 3;
then reconsider fs = canFS S as FinSequence of F_Complex by FINSEQ_1:def 4;
A8: rng fs = S by FUNCT_2:def 3;
A9: len fs = card S by UPROOTS:5;
consider nth being Element of (MultGroup F_Complex );
B10: fs <> {} by A8;
deffunc H₁( set ) -> Element of REAL = |.(qc - (fs /. $1)).|;
consider p1 being FinSequence such that
A11: ( len p1 = len fs & ( for i being Nat st i in dom p1 holds
p1 . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A13: for i being Element of NAT
for c being Element of F_Complex st i in dom p1 & c = (canFS S) . i holds
p1 . i = |.(qc - c).|

proof

let i be Element of NAT ; :: thesis: for c being Element of F_Complex st i in dom p1 & c = (canFS S) . i holds
p1 . i = |.(qc - c).|
let c be Element of F_Complex ; :: thesis: ( i in dom p1 & c = (canFS S) . i implies p1 . i = |.(qc - c).| )
assume that
A14: i in dom p1 and
A15: c = (canFS S) . i ; :: thesis: p1 . i = |.(qc - c).|
i in dom fs by A11, A14, FINSEQ_3:31;
then fs /. i = (canFS S) . i by PARTFUN1:def 8;
hence p1 . i = |.(qc - c).| by A11, A15, A14; :: thesis: verum

end;

for x being set st x in rng p1 holds
x in REAL

proof

let x be set ; :: thesis: ( x in rng p1 implies x in REAL )
assume A17: x in rng p1 ; :: thesis: x in REAL
consider i being Nat such that
A18: i in dom p1 and
A19: p1 . i = x by A17, FINSEQ_2:11;
i in dom fs by A11, A18, FINSEQ_3:31;
then fs /. i = (canFS S) . i by PARTFUN1:def 8;
then x = |.(qc - (fs /. i)).| by A13, A18, A19;
hence x in REAL ; :: thesis: verum

end;

then rng p1 c= REAL by TARSKI:def 3;
then reconsider ps = p1 as non empty FinSequence of REAL by B10, A11, FINSEQ_1:def 4;
A20: |.(eval (cyclotomic_poly n),qc).| = Product ps by A7, A9, A11, A13, Th4;
for i being Element of NAT st i in dom ps holds
ps . i > q - 1

proof

let i be Element of NAT ; :: thesis: ( i in dom ps implies ps . i > q - 1 )
assume A21: i in dom ps ; :: thesis: ps . i > q - 1
i in dom fs by A11, A21, FINSEQ_3:31;
then fs /. i = (canFS S) . i by PARTFUN1:def 8;
then A22: ps . i = |.([**q,0 **] - (fs /. i)).| by A3, A13, A21;
A23: i in dom fs by A11, A21, FINSEQ_3:31;
then fs . i in rng fs by FUNCT_1:12;
then fs /. i in rng fs by A23, PARTFUN1:def 8;
then consider y being Element of (MultGroup F_Complex ) such that
A24: fs /. i = y and
A25: ord y = n by A6, A8;
fs /. i in n -roots_of_1 by A24, A25, Th37;
then A26: |.(fs /. i).| = 1 by Th26;

now

assume A27: fs /. i = [**1,0 **] ; :: thesis: contradiction
1_ (MultGroup F_Complex ) = [**1,0 **] by Th20, COMPLFLD:10;
hence contradiction by A1, A24, A25, A27, GROUP_1:84; :: thesis: verum

end;

hence ps . i > q - 1 by A2, A22, A26, Th8; :: thesis: verum

end;

hence abs i > q - 1 by A4, A5, A20, Th9; :: thesis: verum