The square root of 2 is irrational test

Prove:

$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)))))$

Given:

Axiom	Definition
identity0	$((\forall X) \land (X \in integers) \land ((X + 0) = X) \land ((X * 0) = 0))$
identity1	$((\forall X) \land (X \in integers) \land ((X * 1) = X))$
division	$((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\forall Z) \land (Z \in integers) \land (X \neq 0) \land ((X * Y) = (X * Z)) \Rightarrow (Y = Z))$
ordering	$((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land ((X > Y) ⊻ (X = Y) ⊻ (Y > X)))$
magnitude1	$((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\forall Z) \land (Z \in integers) \land ((X * Y) = Z) \land (X > 1) \land (Z > 0) \Rightarrow (Z > Y))$
magnitude2	$((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land ((X * Y) > 0) \land (X > 0) \Rightarrow (Y > 0))$
range_finite	$((\exists X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\exists Z) \land (Z \in integers) \land (X > Y) \land (Y > Z) \Rightarrow finite (Y))$
factor	$(\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land factor (X, Y) \Leftrightarrow (\exists Z) \land (Z \in integers) \land ((X * Z) = Y)$
prime	$((\forall X) \land (X \in integers) \land prime (X) \Rightarrow (X > 1) \land ((\forall Y) \land (Y \in integers) \land factor (Y, X) \land (Y > 0) \Rightarrow ((Y = 1) \lor (Y = X))))$
prime_factor	$((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\forall Z) \land (Z \in integers) \land prime (X) \land factor (X, (Y * Z)) \Rightarrow (factor (X, Y) \lor factor (X, Z)))$
prime2	$prime (2)$