let n be non empty Element of NAT ; :: thesis: for j, k, q being Integer
for qc being Element of F_Complex st qc = q & j = eval (cyclotomic_poly n),qc & k = eval (unital_poly F_Complex ,n),qc holds
j divides k
let j, k, q be Integer; :: thesis: for qc being Element of F_Complex st qc = q & j = eval (cyclotomic_poly n),qc & k = eval (unital_poly F_Complex ,n),qc holds
j divides k
let qc be Element of F_Complex ; :: thesis: ( qc = q & j = eval (cyclotomic_poly n),qc & k = eval (unital_poly F_Complex ,n),qc implies j divides k )
assume that
A1: qc = q and
A2: j = eval (cyclotomic_poly n),qc and
A3: k = eval (unital_poly F_Complex ,n),qc ; :: thesis: j divides k
set jfc = eval (cyclotomic_poly n),qc;

per cases ( n = 1 or n > 1 ) by NAT_1:54;

suppose n = 1 ; :: thesis: j divides k

hence j divides k by A2, A3, Th52, POLYNOM5:def 4; :: thesis: verum

end;

suppose A4: n > 1 ; :: thesis: j divides k

set eup1fc = eval (unital_poly F_Complex ,1),qc;
reconsider eup1 = eval (unital_poly F_Complex ,1),qc as Integer by A1, Th51;
consider f being FinSequence of the carrier of (Polynom-Ring F_Complex ), p being Polynomial of F_Complex such that
A5: p = Product f and
A6: ( dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds
( ( ( not i divides n or i divides 1 or i = n ) implies f . i = <%(1_ F_Complex )%> ) & ( i divides n & not i divides 1 & i <> n implies f . i = cyclotomic_poly i ) ) ) ) and
A7: unital_poly F_Complex ,n = ((unital_poly F_Complex ,1) *' (cyclotomic_poly n)) *' p by A4, Th58, NAT_D:6;
set epfc = eval p,qc;

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 A8: 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 1 or i = n or ( i divides n & not i divides 1 & i <> n ) ) ;

suppose ( not i divides n or i divides 1 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 A6, A8; :: thesis: verum

end;

suppose ( i divides n & not i divides 1 & 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 A6, A8; :: thesis: verum

end;

end;

end;

then reconsider ep = eval p,qc as Integer by A1, A5, Th59;
k = (eval ((unital_poly F_Complex ,1) *' (cyclotomic_poly n)),qc) * (eval p,qc) by A3, A7, POLYNOM4:27;
then k = ((eval (unital_poly F_Complex ,1),qc) * (eval (cyclotomic_poly n),qc)) * (eval p,qc) by POLYNOM4:27;
then k = (eup1 * ep) * j by A2;
hence j divides k by INT_1:def 9; :: thesis: verum

end;

end;