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;
A5: p > 1 by INT_2:def 4;
p is odd by A1, PEPIN:17;
then p - 1 is even by HILBERT3:2;
then p -' 1 is even by A5, XREAL_1:233;
then 2 divides p -' 1 by PEPIN:22;
then A6: p -' 1 = 2 * ((p -' 1) div 2) ;
s ^2 ,a are_congruent_mod p by A4, INT_1:62;
then a mod p = (s ^2) mod p by NAT_D:64;
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:81
.= (s |^ (p -' 1)) mod p by A6, NEWTON:9 ;
A8: s,p are_coprime 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:3;
s,p are_coprime by A2, A4, Th14;
hence (a |^ ((p -' 1) div 2)) mod p = 1 by A7, PEPIN:37; :: 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:3;
A10: |.p.| = p by ABSVALUE:def 1;
s9 gcd p = |.s.| gcd p by A9, ABSVALUE:def 1
.= s gcd p by A10, INT_2:34
.= 1 by A8, INT_2:def 3 ;
then s9,p are_coprime by INT_2:def 3;
then A11: (s9 |^ (p -' 1)) mod p = 1 by PEPIN:37;
(s |^ (p -' 1)) mod p = ((s |^ 2) |^ ((p -' 1) div 2)) mod p by A6, NEWTON:9
.= (((- s) |^ 2) |^ ((p -' 1) div 2)) mod p by WSIERP_1:1
.= 1 by A6, A11, NEWTON:9 ;
hence (a |^ ((p -' 1) div 2)) mod p = 1 by A7; :: thesis: verum

end;

end;