let n, q be non empty 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 Th48;
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, Th60; :: thesis: verum