let n, q be non zero Element of NAT ; :: thesis: for qc being Element of F_Complex st qc = q holds
for j being Integer st j = eval ((cyclotomic_poly n),qc) holds
j divides (q |^ n) - 1
let qc be Element of F_Complex; :: thesis: ( qc = q implies for j being Integer st j = eval ((cyclotomic_poly n),qc) holds
j divides (q |^ n) - 1 )
assume A1: qc = q ; :: thesis: for j being Integer st j = eval ((cyclotomic_poly n),qc) holds
j divides (q |^ n) - 1
A2: ex y1 being Element of F_Complex st
( y1 = q & eval ((unital_poly (F_Complex,n)),y1) = (q |^ n) - 1 ) by Th44;
let j be Integer; :: thesis: ( j = eval ((cyclotomic_poly n),qc) implies j divides (q |^ n) - 1 )
assume j = eval ((cyclotomic_poly n),qc) ; :: thesis: j divides (q |^ n) - 1
hence j divides (q |^ n) - 1 by A1, A2, Th56; :: thesis: verum