theorem :: INT_8:31

for i, k being Nat
for p being Prime st p > 2 & k >= 2 & i,p are_coprime & i is_primitive_root_of p & (i |^ (p -' 1)) mod (p ^2) <> 1 holds
(i |^ (Euler (p |^ (k -' 1)))) mod (p |^ k) <> 1