theorem Th19: :: INT_5:19

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