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)) mod p = p - 1

let p be Prime; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum

(a |^ ((p -' 1) div 2)) mod p = p - 1

let p be Prime; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum