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 that
A1: p > 2 and
A2: a gcd p = 1 and
A3: a is_quadratic_residue_mod p ; :: thesis: (a |^ ((p -' 1) div 2)) mod p = 1
consider s being Integer such that
A4: ((s ^2 ) - a) mod p = 0 by A3, Def2;
A5: p > 1 by INT_2:def 5;
not p is even by A1, PEPIN:17;
then p - 1 is even by HILBERT3:2;
then p -' 1 is even by A5, XREAL_1:235;
then 2 divides p -' 1 by PEPIN:22;
then A6: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
p divides (s ^2 ) - a by A4, 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 A7: (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 A6, NEWTON:14 ;
A8: s,p are_relative_prime by A2, A4, Th14;

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 A2, A4, Th14;
hence (a |^ ((p -' 1) div 2)) mod p = 1 by A7, PEPIN:38; :: thesis: verum

end;

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

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

end;

end;