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 ;
then p - 1 is even by HILBERT3:2;
then p -' 1 is even by ;
then 2 divides p -' 1 by PEPIN:22;
then A6: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
s ^2 ,a are_congruent_mod p by ;
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 ;
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 ; :: 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
.= s gcd p by
.= 1 by ;
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
.= (((- s) |^ 2) |^ ((p -' 1) div 2)) mod p by WSIERP_1:1
.= 1 by ;
hence (a |^ ((p -' 1) div 2)) mod p = 1 by A7; :: thesis: verum
end;
end;