Prove:

integer(X) and exists(X) and integer(Y) and exists(Y) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y)

Given:

AxiomDefinition
identity0 integer(X) and any(X) and true=> X + 0 = X and X * 0 = 0 ;
identity1 integer(X) and any(X) and true=> X * 1 = X ;
division integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and true and true and true and not X = 0 and X * Y = X * Z=> Y = Z ;
ordering integer(X) and any(X) and integer(Y) and any(Y) and true and true=> X > Y xor X = Y xor Y > X ;
magnitude1 integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and true and true and true and X * Y = Z and X > 1 and Z > 0=> Z > Y ;
magnitude2 integer(X) and any(X) and integer(Y) and any(Y) and true and true and X * Y > 0 and X > 0=> Y > 0 ;
range_finite integer(X) and exists(X) and integer(Y) and any(Y) and integer(Z) and exists(Z) and true and true and true and true and true and X > Y and Y > Z=> finite(Y) ;
factor factor(X,Y)<=> (true) and (true) and (true) and (true) and (X * Z = Y) ;
prime integer(X) and any(X) and integer(Y) and any(Y) and prime(X)=> true and X > 1 and ( (factor(Y,X)) and Y > 0=> Y = 1 or Y = X ) ;
prime_factor integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and (prime(X)) and (factor(X,Y * Z))=> (factor(X,Y)) or (factor(X,Z)) ;
prime2 prime(2);