let p be Prime; :: thesis: ( p > 2 & ( p mod 8 = 1 or p mod 8 = 7 ) implies 2 is_quadratic_residue_mod p )
assume that
A1: p > 2 and
A2: ( 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 A2;

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)) ;
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:9
.= (1 |^ 2) |^ ((4 * ((p div 8) ^2)) + (p div 8)) by WSIERP_1:1
.= 1 ;
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:233
.= (8 * (((8 * ((p div 8) ^2)) + (14 * (p div 8))) + 6)) div 8
.= 2 * (((4 * ((p div 8) ^2)) + (7 * (p div 8))) + 3) ;
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:9
.= (1 |^ 2) |^ (((4 * ((p div 8) ^2)) + (7 * (p div 8))) + 3) by WSIERP_1:1
.= 1 ;
hence 2 is_quadratic_residue_mod p by Def3; :: thesis: verum

end;

end;