set MGFC = MultGroup F_Complex;
set cMGFC = the carrier of ;
let n be non zero 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 ((),qc) holds
|.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 ((),qc) holds
|.i.| > q - 1

consider S being non empty finite Subset of F_Complex such that
A2: S = { y where y is Element of the carrier of : ord y = n } and
A3: cyclotomic_poly n = poly_with_roots ((S,1) -bag) by Def5;
rng () = S by FUNCT_2:def 3;
then reconsider fs = canFS S as FinSequence of F_Complex by FINSEQ_1:def 4;
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 ((),qc) holds
|.i.| > q - 1 )

assume A4: 1 < q ; :: thesis: for qc being Element of F_Complex st qc = q holds
for i being Integer st i = eval ((),qc) holds
|.i.| > q - 1

let qc be Element of F_Complex; :: thesis: ( qc = q implies for i being Integer st i = eval ((),qc) holds
|.i.| > q - 1 )

assume A5: qc = q ; :: thesis: for i being Integer st i = eval ((),qc) holds
|.i.| > q - 1

deffunc H1( set ) -> object = |.(qc - (fs /. \$1)).|;
consider p1 being FinSequence such that
A6: ( len p1 = len fs & ( for i being Nat st i in dom p1 holds
p1 . i = H1(i) ) ) from A7: for i being Element of NAT
for c being Element of F_Complex st i in dom p1 & c = () . 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 = () . i holds
p1 . i = |.(qc - c).|

let c be Element of F_Complex; :: thesis: ( i in dom p1 & c = () . i implies p1 . i = |.(qc - c).| )
assume that
A8: i in dom p1 and
A9: c = () . i ; :: thesis: p1 . i = |.(qc - c).|
i in dom fs by ;
then fs /. i = () . i by PARTFUN1:def 6;
hence p1 . i = |.(qc - c).| by A6, A8, A9; :: thesis: verum
end;
for x being object st x in rng p1 holds
x in REAL
proof
let x be object ; :: thesis: ( x in rng p1 implies x in REAL )
assume x in rng p1 ; :: thesis:
then consider i being Nat such that
A10: i in dom p1 and
A11: p1 . i = x by FINSEQ_2:10;
i in dom fs by ;
then fs /. i = () . i by PARTFUN1:def 6;
then x = H1(i) by A7, A10, A11;
hence x in REAL by XREAL_0:def 1; :: thesis: verum
end;
then rng p1 c= REAL ;
then reconsider ps = p1 as non empty FinSequence of REAL by ;
len fs = card S by FINSEQ_1:93;
then A12: |.(eval ((),qc)).| = Product ps by A3, A6, A7, Th3;
A13: rng fs = S by FUNCT_2:def 3;
A14: 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 A15: i in dom ps ; :: thesis: ps . i > q - 1
i in dom fs by ;
then fs /. i = () . i by PARTFUN1:def 6;
then A16: ps . i = |.([**q,0**] - (fs /. i)).| by A5, A7, A15;
A17: i in dom fs by ;
then fs . i in rng fs by FUNCT_1:3;
then fs /. i in rng fs by ;
then A18: ex y being Element of st
( fs /. i = y & ord y = n ) by ;
A19: now :: thesis: not fs /. i = [**1,0**]end;
fs /. i in n -roots_of_1 by ;
then |.(fs /. i).| = 1 by Th23;
hence ps . i > q - 1 by A4, A16, A19, Th6; :: thesis: verum
end;
reconsider qi = q as Integer ;
1 + 1 <= qi by ;
then A21: (1 + 1) + (- 1) <= qi + (- 1) by XREAL_1:7;
let i be Integer; :: thesis: ( i = eval ((),qc) implies |.i.| > q - 1 )
reconsider x = q - 1 as Real ;
assume i = eval ((),qc) ; :: thesis: |.i.| > q - 1
then |.i.| > x by A21, A12, A14, Th7;
hence |.i.| > q - 1 ; :: thesis: verum