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 H_{1}( 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 = H_{1}(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).|

x in 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

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

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 H

consider p1 being FinSequence such that

A6: ( len p1 = len fs & ( for i being Nat st i in dom p1 holds

p1 . i = H

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

for x being object st x in rng p1 holds
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;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

x in REAL

proof

then
rng p1 c= REAL
;
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 = H_{1}(i)
by A7, A10, A11;

hence x in REAL by XREAL_0:def 1; :: thesis: verum

end;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 = H

hence x in REAL by XREAL_0:def 1; :: thesis: verum

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

reconsider qi = q as Integer ;
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;

then |.(fs /. i).| = 1 by Th23;

hence ps . i > q - 1 by A4, A16, A19, Th6; :: thesis: verum

end;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**]

fs /. i in n -roots_of_1
by A18, Th34;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;1_ (MultGroup F_Complex) = [**1,0**] by Th17, COMPLFLD:8;

hence contradiction by A1, A18, A20, GROUP_1:42; :: thesis: verum

then |.(fs /. i).| = 1 by Th23;

hence ps . i > q - 1 by A4, A16, A19, Th6; :: thesis: verum

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