let n, ni be non zero Element of NAT ; :: thesis: for q being Integer st ni < n & ni divides n holds
for qc being Element of F_Complex st qc = q holds
for j, k, l being Integer st j = eval ((),qc) & k = eval ((),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds
j divides k div l

let q be Integer; :: thesis: ( ni < n & ni divides n implies for qc being Element of F_Complex st qc = q holds
for j, k, l being Integer st j = eval ((),qc) & k = eval ((),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds
j divides k div l )

assume A1: ( ni < n & ni divides n ) ; :: thesis: for qc being Element of F_Complex st qc = q holds
for j, k, l being Integer st j = eval ((),qc) & k = eval ((),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds
j divides k div l

set ttt = (unital_poly (F_Complex,ni)) *' ();
consider f being FinSequence of the carrier of , p being Polynomial of F_Complex such that
A2: p = Product f and
A3: ( dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) ) and
A4: unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' ()) *' p by ;
A5: now :: thesis: for i being non zero Element of NAT holds
( not i in dom f or f . i = or f . i = cyclotomic_poly i )
let i be non zero Element of NAT ; :: thesis: ( not i in dom f or f . b1 = or f . b1 = cyclotomic_poly b1 )
assume A6: i in dom f ; :: thesis: ( f . b1 = or f . b1 = cyclotomic_poly b1 )
per cases ( not i divides n or i divides ni or i = n or ( i divides n & not i divides ni & i <> n ) ) ;
suppose ( not i divides n or i divides ni or i = n ) ; :: thesis: ( f . b1 = or f . b1 = cyclotomic_poly b1 )
hence ( f . i = or f . i = cyclotomic_poly i ) by A3, A6; :: thesis: verum
end;
suppose ( i divides n & not i divides ni & i <> n ) ; :: thesis: ( f . b1 = or f . b1 = cyclotomic_poly b1 )
hence ( f . i = or f . i = cyclotomic_poly i ) by A3, A6; :: thesis: verum
end;
end;
end;
let qc be Element of F_Complex; :: thesis: ( qc = q implies for j, k, l being Integer st j = eval ((),qc) & k = eval ((),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds
j divides k div l )

assume qc = q ; :: thesis: for j, k, l being Integer st j = eval ((),qc) & k = eval ((),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds
j divides k div l

then eval (p,qc) is integer by A2, A5, Th55;
then consider m being Integer such that
A7: m = eval (p,qc) ;
let j, k, l be Integer; :: thesis: ( j = eval ((),qc) & k = eval ((),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) implies j divides k div l )
assume A8: ( j = eval ((),qc) & k = eval ((),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) ) ; :: thesis: j divides k div l
reconsider jc = j, lc = l, mc = m as Element of COMPLEX by XCMPLX_0:def 2;
reconsider jcf = jc, lcf = lc, mcf = mc as Element of F_Complex by COMPLFLD:def 1;
eval ((),qc) = (eval (((unital_poly (F_Complex,ni)) *' ()),qc)) * (eval (p,qc)) by ;
then A9: k = (lcf * jcf) * mcf by
.= (l * j) * m ;
now :: thesis: j divides k div lend;
hence j divides k div l ; :: thesis: verum