theorem MOP: :: NEWTON06:9

for a being Nat
for p being Prime holds
( (a |^ (p - 1)) mod p = 0 or (a |^ (p - 1)) mod p = 1 )