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);

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;

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);

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;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 )

then reconsider ep = eval (p,qc) as Integer by A1, A5, Th55;( 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} = <%(1_ F_Complex)%> or f . b_{1} = cyclotomic_poly b_{1} )

assume A8: i in dom f ; :: thesis: ( f . b_{1} = <%(1_ F_Complex)%> or f . b_{1} = cyclotomic_poly b_{1} )

end;assume A8: i in dom f ; :: thesis: ( f . b

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