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 ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),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 ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),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 ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds
j divides k div l
set ttt = (unital_poly (F_Complex,ni)) *' (cyclotomic_poly n);
consider f being FinSequence of the carrier of (Polynom-Ring F_Complex), 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 = <%(1_ F_Complex)%> ) & ( 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)) *' (cyclotomic_poly n)) *' p by A1, Th54;

A5: now :: thesis: for i being non zero Element of NAT holds
( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i )

let i be non zero Element of NAT ; :: thesis: ( not i in dom f or f . b₁ = <%(1_ F_Complex)%> or f . b₁ = cyclotomic_poly b₁ )
assume A6: i in dom f ; :: thesis: ( f . b₁ = <%(1_ F_Complex)%> or f . b₁ = cyclotomic_poly b₁ )

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 . b₁ = <%(1_ F_Complex)%> or f . b₁ = cyclotomic_poly b₁ )

hence ( f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) by A3, A6; :: thesis: verum

end;

suppose ( i divides n & not i divides ni & i <> n ) ; :: thesis: ( f . b₁ = <%(1_ F_Complex)%> or f . b₁ = cyclotomic_poly b₁ )

hence ( f . i = <%(1_ F_Complex)%> 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 ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),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 ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),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 ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) implies j divides k div l )
assume A8: ( j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),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 ((unital_poly (F_Complex,n)),qc) = (eval (((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)),qc)) * (eval (p,qc)) by A4, POLYNOM4:24;
then A9: k = (lcf * jcf) * mcf by A8, A7, POLYNOM4:24
.= (l * j) * m ;

now :: thesis: j divides k div l

per cases ( l <> 0 or l = 0 ) ;

suppose A10: l <> 0 ; :: thesis: j divides k div l

k = l * (j * m) by A9;
then l divides k by INT_1:def 3;
then k / l is integer by A10, WSIERP_1:17;
then [\(k / l)/] = k / l ;
then k div l = ((j * m) * l) / l by A9, INT_1:def 9;
then k div l = j * m by A10, XCMPLX_1:89;
hence j divides k div l by INT_1:def 3; :: thesis: verum

end;

suppose l = 0 ; :: thesis: j divides k div l

then k div l = 0 ;
hence j divides k div l by INT_2:12; :: thesis: verum

end;

end;

end;

hence j divides k div l ; :: thesis: verum