let a be Integer; for p being Prime st p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p holds
(a |^ ((p -' 1) div 2)) mod p = p - 1
let p be Prime; ( p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p implies (a |^ ((p -' 1) div 2)) mod p = p - 1 )
assume that
A1:
p > 2
and
A2:
a gcd p = 1
and
A3:
not a is_quadratic_residue_mod p
; (a |^ ((p -' 1) div 2)) mod p = p - 1
set l = a mod p;
reconsider l = a mod p as Element of NAT by INT_1:3, INT_1:57;
A4:
l mod p = a mod p
by NAT_D:65;
then A5:
l,a are_congruent_mod p
by NAT_D:64;
then
l gcd p = 1
by A2, WSIERP_1:43;
then
(l |^ ((p -' 1) div 2)) mod p = p - 1
by A1, A3, A5, Th11, Th18;
hence
(a |^ ((p -' 1) div 2)) mod p = p - 1
by A4, Th13; verum