theorem :: INT_8:29

for i being Nat
for p being Prime st p > 2 & i,p are_coprime & i is_primitive_root_of p holds
for k being Nat holds not i |^ ((2 * k) + 1) is_quadratic_residue_mod p