let n, ni, q be non empty Element of NAT ; :: thesis: ( ni < n & ni divides n implies 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) div ((q |^ ni) - 1) )
assume A1: ( ni < n & ni divides n ) ; :: 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) div ((q |^ ni) - 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) div ((q |^ ni) - 1) )
assume A2: qc = q ; :: thesis: for j being Integer st j = eval (cyclotomic_poly n),qc holds
j divides ((q |^ n) - 1) div ((q |^ ni) - 1)
A3: ( ex y1 being Element of F_Complex st
( y1 = q & eval (unital_poly F_Complex ,n),y1 = (q |^ n) - 1 ) & ex y2 being Element of F_Complex st
( y2 = q & eval (unital_poly F_Complex ,ni),y2 = (q |^ ni) - 1 ) ) by Th48;
let j be Integer; :: thesis: ( j = eval (cyclotomic_poly n),qc implies j divides ((q |^ n) - 1) div ((q |^ ni) - 1) )
assume j = eval (cyclotomic_poly n),qc ; :: thesis: j divides ((q |^ n) - 1) div ((q |^ ni) - 1)
hence j divides ((q |^ n) - 1) div ((q |^ ni) - 1) by A1, A2, A3, Th61; :: thesis: verum