let p be Prime; :: thesis: ( p > 2 & ( p mod 8 = 1 or p mod 8 = 7 ) implies 2 is_quadratic_residue_mod p )
assume A1: ( p > 2 & ( p mod 8 = 1 or p mod 8 = 7 ) ) ; :: thesis: 2 is_quadratic_residue_mod p
set nn = p div 8;

per cases ( p mod 8 = 1 or p mod 8 = 7 ) by A1;

suppose p mod 8 = 1 ; :: thesis: 2 is_quadratic_residue_mod p

then p = (8 * (p div 8)) + 1 by NAT_D:2;
then ((p ^2 ) -' 1) div 8 = (((((8 * (p div 8)) ^2 ) + (2 * (8 * (p div 8)))) + 1) -' 1) div 8
.= (8 * ((8 * ((p div 8) ^2 )) + (2 * (p div 8)))) div 8 by NAT_D:34
.= 2 * ((4 * ((p div 8) ^2 )) + (p div 8)) by NAT_D:18 ;
then Lege 2,p = (- 1) |^ (2 * ((4 * ((p div 8) ^2 )) + (p div 8))) by A1, Th42
.= ((- 1) |^ 2) |^ ((4 * ((p div 8) ^2 )) + (p div 8)) by NEWTON:14
.= (1 |^ 2) |^ ((4 * ((p div 8) ^2 )) + (p div 8)) by WSIERP_1:2
.= 1 |^ ((4 * ((p div 8) ^2 )) + (p div 8)) by NEWTON:15
.= 1 by NEWTON:15 ;
hence 2 is_quadratic_residue_mod p by Def3; :: thesis: verum

end;

suppose p mod 8 = 7 ; :: thesis: 2 is_quadratic_residue_mod p

then p = (8 * (p div 8)) + 7 by NAT_D:2;
then ((p ^2 ) -' 1) div 8 = ((((8 * (8 * ((p div 8) ^2 ))) + (8 * (14 * (p div 8)))) + 49) - 1) div 8 by NAT_1:12, XREAL_1:235
.= (8 * (((8 * ((p div 8) ^2 )) + (14 * (p div 8))) + 6)) div 8
.= 2 * (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3) by NAT_D:18 ;
then Lege 2,p = (- 1) |^ (2 * (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3)) by A1, Th42
.= ((- 1) |^ 2) |^ (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3) by NEWTON:14
.= (1 |^ 2) |^ (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3) by WSIERP_1:2
.= 1 |^ (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3) by NEWTON:15
.= 1 by NEWTON:15 ;
hence 2 is_quadratic_residue_mod p by Def3; :: thesis: verum

end;

end;