let p be Prime; :: thesis: ( p > 2 & p mod 4 = 1 implies - 1 is_quadratic_residue_mod p )
assume that
A1: p > 2 and
A2: p mod 4 = 1 ; :: thesis: - 1 is_quadratic_residue_mod p
p > 1 by INT_2:def 4;
then A3: p -' 1 = p - 1 by XREAL_1:233;
p = ((p div 4) * 4) + 1 by A2, NAT_D:2;
then p -' 1 = 2 * (2 * (p div 4)) by A3;
then (- 1) |^ ((p -' 1) div 2) = (- 1) |^ (2 * (p div 4)) by NAT_D:18
.= ((- 1) |^ 2) |^ (p div 4) by NEWTON:9
.= (1 |^ 2) |^ (p div 4) by WSIERP_1:1
.= 1 ;
then Lege ((- 1),p) = 1 by A1, Th36;
hence - 1 is_quadratic_residue_mod p by Def3; :: thesis: verum