let n, ni, q be non zero 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 Th44;
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, Th57; :: thesis: verum