let x, y, z be Nat; :: thesis: ((x ^2) - (2 * (y ^2))) + (8 * z) <> 3
assume A1: ((x ^2) - (2 * (y ^2))) + (8 * z) = 3 ; :: thesis: contradiction

per cases ( y is even or y is odd ) ;

suppose y is even ; :: thesis: contradiction

then consider k being Nat such that
A2: y = 2 * k ;
A3: ((x ^2) - ((2 * (2 * k)) * (2 * k))) + (8 * z) = 3 by A1, A2;
((8 * ((k ^2) - z)) + 3) mod 8 = 3 mod 8 by NAT_D:61
.= 3 by NAT_D:24 ;
hence contradiction by A3, Th51; :: thesis: verum

end;

suppose y is odd ; :: thesis: contradiction

then consider k being Nat such that
A4: y = (2 * k) + 1 by ABIAN:9;
A5: ((x ^2) - ((2 * ((2 * k) + 1)) * ((2 * k) + 1))) + (8 * z) = 3 by A1, A4;
((8 * (((k ^2) + k) - z)) + 5) mod 8 = 5 mod 8 by NAT_D:61
.= 5 by NAT_D:24 ;
hence contradiction by A5, Th51; :: thesis: verum

end;

end;