let n, ni be non empty 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
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 A2: 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
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 that
A3: j = eval (cyclotomic_poly n),qc and
A4: k = eval (unital_poly F_Complex ,n),qc and
A5: l = eval (unital_poly F_Complex ,ni),qc ; :: thesis: 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
A6: p = Product f and
A7: dom f = Seg n and
A8: for i being non empty 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
A9: unital_poly F_Complex ,n = ((unital_poly F_Complex ,ni) *' (cyclotomic_poly n)) *' p by A1, Th58;
A10: eval (unital_poly F_Complex ,n),qc = (eval ((unital_poly F_Complex ,ni) *' (cyclotomic_poly n)),qc) * (eval p,qc) by A9, POLYNOM4:27;

now

let i be non empty Element of NAT ; :: thesis: ( not i in dom f or f . b₁ = <%(1_ F_Complex )%> or f . b₁ = cyclotomic_poly b₁ )
assume A11: 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 A7, A8, A11; :: 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 A7, A8, A11; :: thesis: verum

end;

end;

end;

then eval p,qc is integer by A2, A6, Th59;
then consider m being Integer such that
A12: m = eval p,qc ;
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;
A13: k = (lcf * jcf) * mcf by A3, A4, A5, A10, A12, POLYNOM4:27
.= (l * j) * m ;

now

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

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

k = l * (j * m) by A13;
then l divides k by INT_1:def 9;
then k / l is integer by A14, WSIERP_1:22;
then [\(k / l)/] = k / l by INT_1:47;
then k div l = ((j * m) * l) / l by A13, INT_1:def 7;
then k div l = j * m by A14, XCMPLX_1:90;
hence j divides k div l by INT_1:def 9; :: thesis: verum

end;

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

then k div l = 0 by INT_1:75;
hence j divides k div l by INT_2:16; :: thesis: verum

end;

end;

end;

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