set MGFC = MultGroup F_Complex;
set cMGFC = the carrier of (MultGroup F_Complex);
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 ((cyclotomic_poly n),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 ((cyclotomic_poly n),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 (MultGroup F_Complex) : ord y = n } and
A3: 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;
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
|.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 ((cyclotomic_poly n),qc) holds
|.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
|.i.| > q - 1 )
assume A5: qc = q ; :: thesis: for i being Integer st i = eval ((cyclotomic_poly n),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 FINSEQ_1:sch 2();
 A7: 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
A8: i in dom p1 and
A9: c = (canFS S) . i ; :: thesis: p1 . i = |.(qc - c).|
i in dom fs by A6, A8, FINSEQ_3:29;
then fs /. i = (canFS S) . 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: x in REAL
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 A6, A10, FINSEQ_3:29;
then fs /. i = (canFS S) . 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 A6, FINSEQ_1:def 4;
len fs = card S by FINSEQ_1:93;
then A12: |.(eval ((cyclotomic_poly n),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 A6, A15, FINSEQ_3:29;
then fs /. i = (canFS S) . i by PARTFUN1:def 6;
then A16: ps . i = |.([**q,0**] - (fs /. i)).| by A5, A7, A15;
A17: i in dom fs by A6, A15, FINSEQ_3:29;
then fs . i in rng fs by FUNCT_1:3;
then fs /. i in rng fs by A17, PARTFUN1:def 6;
then A18: ex y being Element of (MultGroup F_Complex) st
( fs /. i = y & ord y = n ) by A2, A13;
A19: now :: thesis: not fs /. i = [**1,0**]
assume A20: fs /. i = [**1,0**] ; :: thesis: contradiction
1_ (MultGroup F_Complex) = [**1,0**] by Th17, COMPLFLD:8;
hence contradiction by A1, A18, A20, GROUP_1:42; :: thesis: verum
end;
fs /. i in n -roots_of_1 by A18, Th34;
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 A4, INT_1:7;
then A21: (1 + 1) + (- 1) <= qi + (- 1) by XREAL_1:7;
let i be Integer; :: thesis: ( i = eval ((cyclotomic_poly n),qc) implies |.i.| > q - 1 )
reconsider x = q - 1 as Real ;
assume i = eval ((cyclotomic_poly n),qc) ; :: thesis: |.i.| > q - 1
then |.i.| > x by A21, A12, A14, Th7;
hence |.i.| > q - 1 ; :: thesis: verum