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
proof
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;
hence eval ((cyclotomic_poly d),z) is Integer by A2, Th14; :: thesis: verum