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)) - 1) mod p = 0
let p be Prime; :: thesis: ( p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies ((a |^ ((p -' 1) div 2)) - 1) mod p = 0 )
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)) - 1) mod p = 0
A4: p > 1 by INT_2:def 4;
(a |^ ((p -' 1) div 2)) mod p = 1 by A1, A2, A3, Th17;
then (a |^ ((p -' 1) div 2)) mod p = 1 mod p by A4, NAT_D:14;
then a |^ ((p -' 1) div 2),1 are_congruent_mod p by NAT_D:64;
hence ((a |^ ((p -' 1) div 2)) - 1) mod p = 0 by INT_1:62; :: thesis: verum