let p be Prime; :: thesis: ( p > 2 & p mod 4 = 3 implies not - 1 is_quadratic_residue_mod p )
assume that
A1: p > 2 and
A2: p mod 4 = 3 ; :: thesis: not - 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) + 3 by A2, NAT_D:2;
then p -' 1 = 2 * ((2 * (p div 4)) + 1) by A3;
then (- 1) |^ ((p -' 1) div 2) = (- 1) |^ ((2 * (p div 4)) + 1)
.= ((- 1) |^ (2 * (p div 4))) * (- 1) by NEWTON:6
.= (((- 1) |^ 2) |^ (p div 4)) * (- 1) by NEWTON:9
.= ((1 |^ 2) |^ (p div 4)) * (- 1) by WSIERP_1:1
.= 1 * (- 1) ;
then Lege ((- 1),p) = - 1 by A1, Th36;
then ( ( not - 1 is_quadratic_residue_mod p or not (- 1) mod p <> 0 ) & ( not - 1 is_quadratic_residue_mod p or not (- 1) mod p = 0 ) ) by Def3;
hence not - 1 is_quadratic_residue_mod p ; :: thesis: verum