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 A1: ( p > 2 & a gcd p = 1 ) ; :: thesis: Lege a,p,a |^ ((p -' 1) div 2) are_congruent_mod p
A2: p > 1 by INT_2:def 5;
then - p < - 1 by XREAL_1:26;
then A3: (- 1) mod p = p + (- 1) by INT_3:10;

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

suppose A4: 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, Th17;
then (a |^ ((p -' 1) div 2)) mod p = 1 mod p by A2, NAT_D:14;
then (a |^ ((p -' 1) div 2)) mod p = (Lege a,p) mod p by A4, Def3;
hence Lege a,p,a |^ ((p -' 1) div 2) are_congruent_mod p by INT_3:12; :: thesis: verum

end;

suppose A5: 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, Th19
.= (Lege a,p) mod p by A3, A5, Def3 ;
hence Lege a,p,a |^ ((p -' 1) div 2) are_congruent_mod p by INT_3:12; :: thesis: verum

end;

end;