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)
let j be Integer; :: thesis: ( j = eval (cyclotomic_poly n),qc implies j divides ((q |^ n) - 1) div ((q |^ ni) - 1) )
assume A3: j = eval (cyclotomic_poly n),qc ; :: thesis: j divides ((q |^ n) - 1) div ((q |^ ni) - 1)
consider y1 being Element of F_Complex such that
A4: ( y1 = q & eval (unital_poly F_Complex ,n),y1 = (q |^ n) - 1 ) by Th48;
consider y2 being Element of F_Complex such that
A5: ( y2 = q & eval (unital_poly F_Complex ,ni),y2 = (q |^ ni) - 1 ) by Th48;
thus j divides ((q |^ n) - 1) div ((q |^ ni) - 1) by A1, A2, A3, A4, A5, Th61; :: thesis: verum