let p be Prime; :: thesis: ( p > 2 & ( p mod 8 = 3 or p mod 8 = 5 ) implies not 2 is_quadratic_residue_mod p )
assume that
A1: p > 2 and
A2: ( p mod 8 = 3 or p mod 8 = 5 ) ; :: thesis: not 2 is_quadratic_residue_mod p
set nn = p div 8;

per cases ( p mod 8 = 3 or p mod 8 = 5 ) by A2;

suppose p mod 8 = 3 ; :: thesis: not 2 is_quadratic_residue_mod p

then p = (8 * (p div 8)) + 3 by NAT_D:2;
then ((p ^2) -' 1) div 8 = ((((8 * (8 * ((p div 8) ^2))) + (8 * (6 * (p div 8)))) + (3 * 3)) - 1) div 8 by NAT_1:12, XREAL_1:233
.= (8 * (((8 * ((p div 8) ^2)) + (6 * (p div 8))) + 1)) div 8
.= ((8 * ((p div 8) ^2)) + (6 * (p div 8))) + 1 ;
then Lege (2,p) = (- 1) |^ (((8 * ((p div 8) ^2)) + (6 * (p div 8))) + 1) by A1, Th42
.= ((- 1) |^ (2 * ((4 * ((p div 8) ^2)) + (3 * (p div 8))))) * (- 1) by NEWTON:6
.= (((- 1) |^ 2) |^ ((4 * ((p div 8) ^2)) + (3 * (p div 8)))) * (- 1) by NEWTON:9
.= ((1 |^ 2) |^ ((4 * ((p div 8) ^2)) + (3 * (p div 8)))) * (- 1) by WSIERP_1:1
.= - 1 ;
then ( ( not 2 is_quadratic_residue_mod p or not 2 mod p <> 0 ) & ( not 2 is_quadratic_residue_mod p or not 2 mod p = 0 ) ) by Def3;
hence not 2 is_quadratic_residue_mod p ; :: thesis: verum

end;

suppose p mod 8 = 5 ; :: thesis: not 2 is_quadratic_residue_mod p

then p = (8 * (p div 8)) + 5 by NAT_D:2;
then ((p ^2) -' 1) div 8 = ((((8 * (8 * ((p div 8) ^2))) + (8 * (10 * (p div 8)))) + 25) - 1) div 8 by NAT_1:12, XREAL_1:233
.= (8 * (((8 * ((p div 8) ^2)) + (10 * (p div 8))) + 3)) div 8
.= ((8 * ((p div 8) ^2)) + (10 * (p div 8))) + 3 ;
then Lege (2,p) = (- 1) |^ ((((2 * (4 * ((p div 8) ^2))) + (2 * (5 * (p div 8)))) + (2 * 1)) + 1) by A1, Th42
.= ((- 1) |^ (2 * (((4 * ((p div 8) ^2)) + (5 * (p div 8))) + 1))) * (- 1) by NEWTON:6
.= (((- 1) |^ 2) |^ (((4 * ((p div 8) ^2)) + (5 * (p div 8))) + 1)) * (- 1) by NEWTON:9
.= ((1 |^ 2) |^ (((4 * ((p div 8) ^2)) + (5 * (p div 8))) + 1)) * (- 1) by WSIERP_1:1
.= - 1 ;
then ( ( not 2 is_quadratic_residue_mod p or not 2 mod p <> 0 ) & ( not 2 is_quadratic_residue_mod p or not 2 mod p = 0 ) ) by Def3;
hence not 2 is_quadratic_residue_mod p ; :: thesis: verum

end;

end;