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

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