let p be natural prime 2 _greater number ; for a being integer number st a gcd p = 1 holds
a |^ ((p - 1) / 2), LegendreSymbol (a,p) are_congruent_mod p
let a be integer number ; ( a gcd p = 1 implies a |^ ((p - 1) / 2), LegendreSymbol (a,p) are_congruent_mod p )
p - 1 > 2 - 1
by Def1, XREAL_1:9;
then A1:
p -' 1 = p - 1
by NAT_D:39;
assume
a gcd p = 1
; a |^ ((p - 1) / 2), LegendreSymbol (a,p) are_congruent_mod p
then
Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p
by Def1, INT_5:28;
then A2:
Lege (a,p),a |^ ((p - 1) / 2) are_congruent_mod p
by A1, Th4;
Leg (a,p) = Lege (a,p)
by Lm4;
hence
a |^ ((p - 1) / 2), LegendreSymbol (a,p) are_congruent_mod p
by A2, INT_1:14; verum