theorem Th20: :: INT_5:20

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