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 A1: ( p > 2 & ( 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 A1;

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:235
.= (8 * (((8 * ((p div 8) ^2 )) + (6 * (p div 8))) + 1)) div 8
.= ((8 * ((p div 8) ^2 )) + (6 * (p div 8))) + 1 by NAT_D:18 ;
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:11
.= (((- 1) |^ 2) |^ ((4 * ((p div 8) ^2 )) + (3 * (p div 8)))) * (- 1) by NEWTON:14
.= ((1 |^ 2) |^ ((4 * ((p div 8) ^2 )) + (3 * (p div 8)))) * (- 1) by WSIERP_1:2
.= (1 |^ ((4 * ((p div 8) ^2 )) + (3 * (p div 8)))) * (- 1) by NEWTON:15
.= 1 * (- 1) by NEWTON:15
.= - 1 ;
hence not 2 is_quadratic_residue_mod p by Def3; :: 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:235
.= (8 * (((8 * ((p div 8) ^2 )) + (10 * (p div 8))) + 3)) div 8
.= ((8 * ((p div 8) ^2 )) + (10 * (p div 8))) + 3 by NAT_D:18 ;
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:11
.= (((- 1) |^ 2) |^ (((4 * ((p div 8) ^2 )) + (5 * (p div 8))) + 1)) * (- 1) by NEWTON:14
.= ((1 |^ 2) |^ (((4 * ((p div 8) ^2 )) + (5 * (p div 8))) + 1)) * (- 1) by WSIERP_1:2
.= (1 |^ (((4 * ((p div 8) ^2 )) + (5 * (p div 8))) + 1)) * (- 1) by NEWTON:15
.= 1 * (- 1) by NEWTON:15
.= - 1 ;
hence not 2 is_quadratic_residue_mod p by Def3; :: thesis: verum

end;

end;