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) by NAT_D:3;

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;

(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) by NAT_D:3;

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 )
;

end;

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;s,p are_coprime by A2, A4, Th14;

hence (a |^ ((p -' 1) div 2)) mod p = 1 by A7, PEPIN:37; :: thesis: verum

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;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