let n, ni be non zero Element of NAT ; 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; ( 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 )
; 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;
let qc be Element of F_Complex; ( 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
; 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; ( 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) )
; 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
;
hence
j divides k div l
; verum