let a be Integer; :: thesis: for p being Prime st p > 2 & a gcd p = 1 & not 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 & not 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: not a is_quadratic_residue_mod p ; :: thesis: ((a |^ ((p -' 1) div 2)) + 1) mod p = 0
A4: p - 1 < p by XREAL_1:146;
(a |^ ((p -' 1) div 2)) mod p = p - 1 by A1, A2, A3, Th19;
then (a |^ ((p -' 1) div 2)) mod p = (p - 1) mod p by A4, NAT_D:63;
then a |^ ((p -' 1) div 2),p - 1 are_congruent_mod p by NAT_D:64;
then p divides - (((a |^ ((p -' 1) div 2)) + 1) - p) by INT_2:10;
then p divides p - ((a |^ ((p -' 1) div 2)) + 1) ;
then p divides (a |^ ((p -' 1) div 2)) + 1 by Th2;
hence ((a |^ ((p -' 1) div 2)) + 1) mod p = 0 by INT_1:62; :: thesis: verum