for n being non zero Element of NAT st 1 < n holds
for q being Element of NAT st 1 < q holds
for qc being Element of F_Complex st qc = q holds
for i being Integer st i = eval ((cyclotomic_poly n),qc) holds
|.i.| > q - 1