let d be non zero Element of NAT ; :: thesis: for z being Element of F_Complex st z is Integer holds

eval ((cyclotomic_poly d),z) is Integer

let z be Element of F_Complex; :: thesis: ( z is Integer implies eval ((cyclotomic_poly d),z) is Integer )

assume A1: z is Integer ; :: thesis: eval ((cyclotomic_poly d),z) is Integer

set phi = cyclotomic_poly d;

consider F being FinSequence of F_Complex such that

A2: eval ((cyclotomic_poly d),z) = Sum F and

len F = len (cyclotomic_poly d) and

A3: for i being Element of NAT st i in dom F holds

F . i = ((cyclotomic_poly d) . (i -' 1)) * ((power F_Complex) . (z,(i -' 1))) by POLYNOM4:def 2;

for i being Element of NAT st i in dom F holds

F . i is Integer

eval ((cyclotomic_poly d),z) is Integer

let z be Element of F_Complex; :: thesis: ( z is Integer implies eval ((cyclotomic_poly d),z) is Integer )

assume A1: z is Integer ; :: thesis: eval ((cyclotomic_poly d),z) is Integer

set phi = cyclotomic_poly d;

consider F being FinSequence of F_Complex such that

A2: eval ((cyclotomic_poly d),z) = Sum F and

len F = len (cyclotomic_poly d) and

A3: for i being Element of NAT st i in dom F holds

F . i = ((cyclotomic_poly d) . (i -' 1)) * ((power F_Complex) . (z,(i -' 1))) by POLYNOM4:def 2;

for i being Element of NAT st i in dom F holds

F . i is Integer

proof

hence
eval ((cyclotomic_poly d),z) is Integer
by A2, Th14; :: thesis: verum
let i be Element of NAT ; :: thesis: ( i in dom F implies F . i is Integer )

assume i in dom F ; :: thesis: F . i is Integer

then A4: F . i = ((cyclotomic_poly d) . (i -' 1)) * ((power F_Complex) . (z,(i -' 1))) by A3;

reconsider i2 = (power F_Complex) . (z,(i -' 1)) as Integer by A1, Th13;

reconsider i1 = (cyclotomic_poly d) . (i -' 1) as Integer by Th51;

F . i = i1 * i2 by A4;

hence F . i is Integer ; :: thesis: verum

end;assume i in dom F ; :: thesis: F . i is Integer

then A4: F . i = ((cyclotomic_poly d) . (i -' 1)) * ((power F_Complex) . (z,(i -' 1))) by A3;

reconsider i2 = (power F_Complex) . (z,(i -' 1)) as Integer by A1, Th13;

reconsider i1 = (cyclotomic_poly d) . (i -' 1) as Integer by Th51;

F . i = i1 * i2 by A4;

hence F . i is Integer ; :: thesis: verum