let a be Integer; :: thesis: for p being Prime st p > 2 & a gcd p = 1 holds
Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p
let p be Prime; :: thesis: ( p > 2 & a gcd p = 1 implies Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p )
assume that
A1: p > 2 and
A2: a gcd p = 1 ; :: thesis: Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p
not p divides a by Lm3, A2;
then A3: a mod p <> 0 by INT_1:62;
A4: p > 1 by INT_2:def 4;
then - p < - 1 by XREAL_1:24;
then A5: (- 1) mod p = p + (- 1) by NAT_D:63;

per cases ( a is_quadratic_residue_mod p or not a is_quadratic_residue_mod p ) ;

suppose A6: a is_quadratic_residue_mod p ; :: thesis: Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p

then (a |^ ((p -' 1) div 2)) mod p = 1 by A1, A2, Th17;
then (a |^ ((p -' 1) div 2)) mod p = 1 mod p by A4, NAT_D:14;
then (a |^ ((p -' 1) div 2)) mod p = (Lege (a,p)) mod p by A6, Def3, A3;
hence Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p by NAT_D:64; :: thesis: verum

end;

suppose A7: not a is_quadratic_residue_mod p ; :: thesis: Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p

then (a |^ ((p -' 1) div 2)) mod p = p - 1 by A1, A2, Th19
.= (Lege (a,p)) mod p by A5, A7, Def3 ;
hence Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p by NAT_D:64; :: thesis: verum

end;

end;