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 ((),qc) & k = eval ((),qc) holds
j divides k

let j, k, q be Integer; :: thesis: for qc being Element of F_Complex st qc = q & j = eval ((),qc) & k = eval ((),qc) holds
j divides k

let qc be Element of F_Complex; :: thesis: ( qc = q & j = eval ((),qc) & k = eval ((),qc) implies j divides k )
assume that
A1: qc = q and
A2: j = eval ((),qc) and
A3: k = eval ((),qc) ; :: thesis: j divides k
set jfc = eval ((),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 ((),qc);
reconsider eup1 = eval ((),qc) as Integer by ;
consider f being FinSequence of the carrier of , 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 = ) & ( i divides n & not i divides 1 & i <> n implies f . i = cyclotomic_poly i ) ) ) ) and
A7: unital_poly (F_Complex,n) = (() *' ()) *' p by ;
set epfc = eval (p,qc);
now :: thesis: for i being non zero Element of NAT holds
( not i in dom f or f . i = or f . i = cyclotomic_poly i )
let i be non zero Element of NAT ; :: thesis: ( not i in dom f or f . b1 = or f . b1 = cyclotomic_poly b1 )
assume A8: i in dom f ; :: thesis: ( f . b1 = or f . b1 = cyclotomic_poly b1 )
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 . b1 = or f . b1 = cyclotomic_poly b1 )
hence ( f . i = or f . i = cyclotomic_poly i ) by A6, A8; :: thesis: verum
end;
suppose ( i divides n & not i divides 1 & i <> n ) ; :: thesis: ( f . b1 = or f . b1 = cyclotomic_poly b1 )
hence ( f . i = 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 ((() *' ()),qc)) * (eval (p,qc)) by ;
then k = ((eval ((),qc)) * (eval ((),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;