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 ( p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p ) ; :: thesis: ((a |^ ((p -' 1) div 2)) - 1) mod p = 0
then A1: (a |^ ((p -' 1) div 2)) mod p = 1 by Th17;
p > 1 by INT_2:def 5;
then (a |^ ((p -' 1) div 2)) mod p = 1 mod p by A1, NAT_D:14;
then a |^ ((p -' 1) div 2),1 are_congruent_mod p by INT_3:12;
then p divides (a |^ ((p -' 1) div 2)) - 1 by INT_2:19;
hence ((a |^ ((p -' 1) div 2)) - 1) mod p = 0 by INT_1:89; :: thesis: verum