theorem Th31: :: NAT_6:31

for p being 2 _greater Prime
for a being Integer st a gcd p = 1 holds
a |^ ((p - 1) / 2), LegendreSymbol (a,p) are_congruent_mod p