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 A1: ( p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p ) ; :: thesis: ((a |^ ((p -' 1) div 2)) + 1) mod p = 0
then A2: (a |^ ((p -' 1) div 2)) mod p = p - 1 by Th19;
( p - 1 > 2 - 1 & p - 1 < p ) by A1, XREAL_1:11, XREAL_1:148;
then (a |^ ((p -' 1) div 2)) mod p = (p - 1) mod p by A2, INT_3:10;
then a |^ ((p -' 1) div 2),p - 1 are_congruent_mod p by INT_3:12;
then p divides (a |^ ((p -' 1) div 2)) - (p - 1) by INT_2:19;
then p divides - (((a |^ ((p -' 1) div 2)) + 1) - p) by INT_2:14;
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:89; :: thesis: verum