let n be non zero 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:53;

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

hence j divides k by A2, A3, Th48; :: 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, Th47;
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 zero 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, Th54, NAT_D:6;
set epfc = eval (p,qc);

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 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, Th55;
k = (eval (((unital_poly (F_Complex,1)) *' (cyclotomic_poly n)),qc)) * (eval (p,qc)) by A3, A7, POLYNOM4:24;
then k = ((eval ((unital_poly (F_Complex,1)),qc)) * (eval ((cyclotomic_poly n),qc))) * (eval (p,qc)) by POLYNOM4:24;
then k = (eup1 * ep) * j by A2;
hence j divides k by INT_1:def 3; :: thesis: verum

end;

end;