let p be natural prime 2 _greater number ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum