theorem Th18: :: INT_5:18

for p being Prime
for b being Nat st p > 2 & b gcd p = 1 & not b is_quadratic_residue_mod p holds
(b |^ ((p -' 1) div 2)) mod p = p - 1