let a be Integer; :: thesis: for p being Prime st p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p holds
(a |^ ((p -' 1) div 2)) mod p = 1
let p be Prime; :: thesis: ( p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies (a |^ ((p -' 1) div 2)) mod p = 1 )
assume A1: ( p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p ) ; :: thesis: (a |^ ((p -' 1) div 2)) mod p = 1
then consider s being Integer such that
A2: ((s ^2 ) - a) mod p = 0 by Def2;
not p is even by A1, PEPIN:17;
then A3: p - 1 is even by HILBERT3:2;
p > 1 by INT_2:def 5;
then p -' 1 is even by A3, XREAL_1:235;
then 2 divides p -' 1 by PEPIN:22;
then A4: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
A5: s,p are_relative_prime by A1, A2, Th14;
p divides (s ^2 ) - a by A2, INT_1:89;
then s ^2 ,a are_congruent_mod p by INT_2:19;
then a mod p = (s ^2 ) mod p by INT_3:12;
then A6: (a |^ ((p -' 1) div 2)) mod p = ((s ^2 ) |^ ((p -' 1) div 2)) mod p by Th13
.= ((s |^ 2) |^ ((p -' 1) div 2)) mod p by NEWTON:100
.= (s |^ (p -' 1)) mod p by A4, NEWTON:14 ;

per cases ( s >= 0 or s < 0 ) ;

suppose s >= 0 ; :: thesis: (a |^ ((p -' 1) div 2)) mod p = 1

then reconsider s = s as Element of NAT by INT_1:16;
s,p are_relative_prime by A1, A2, Th14;
hence (a |^ ((p -' 1) div 2)) mod p = 1 by A6, PEPIN:38; :: thesis: verum

end;

suppose A7: s < 0 ; :: thesis: (a |^ ((p -' 1) div 2)) mod p = 1

then - s > 0 by XREAL_1:60;
then reconsider s' = - s as Element of NAT by INT_1:16;
A8: abs p = p by ABSVALUE:def 1;
s' gcd p = (abs s) gcd p by A7, ABSVALUE:def 1
.= s gcd p by A8, INT_2:51
.= 1 by A5, INT_2:def 4 ;
then s',p are_relative_prime by INT_2:def 4;
then A9: (s' |^ (p -' 1)) mod p = 1 by PEPIN:38;
(s |^ (p -' 1)) mod p = ((s |^ 2) |^ ((p -' 1) div 2)) mod p by A4, NEWTON:14
.= (((- s) |^ 2) |^ ((p -' 1) div 2)) mod p by WSIERP_1:2
.= 1 by A4, A9, NEWTON:14 ;
hence (a |^ ((p -' 1) div 2)) mod p = 1 by A6; :: thesis: verum

end;

end;