The square root of 2 is irrational proof

Step	Using
$(((\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)))))$
$(((\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)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))))))$	Ascendancy
$(((\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)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)))))$	Induction factor
$(((\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)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land factor (2, Y))))$	Induction prime_factor
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y))))$	Induction factor
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0))))$	Inference
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0))))$	Induction magnitude2
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)))))$	Inference
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)))))$	Induction division
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)) \land factor (2, (X * X)))))$	Induction factor
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)) \land factor (2, (X * X)) \land factor (2, X))))$	Induction prime_factor
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land (\exists V3) \land (V3 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)) \land factor (2, (X * X)) \land ((2 * V3) = X))))$	Induction factor
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land (\exists V3) \land (V3 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)) \land factor (2, (X * X)) \land ((2 * V3) = X) \land ((V2 * 2 * V2) = (2 * V3 * 2 * V3)))))$	Inference
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land (\exists V3) \land (V3 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)) \land factor (2, (X * X)) \land ((2 * V3) = X) \land ((V2 * 2 * V2) = (2 * V3 * 2 * V3)) \land (X > V3))))$	Induction magnitude1
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land (\exists V3) \land (V3 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)) \land factor (2, (X * X)) \land ((2 * V3) = X) \land ((V2 * 2 * V2) = (2 * V3 * 2 * V3)) \land (X > V3) \land ((2 * V3) > 0))))$	Inference
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land (\exists V3) \land (V3 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)) \land factor (2, (X * X)) \land ((2 * V3) = X) \land ((V2 * 2 * V2) = (2 * V3 * 2 * V3)) \land (X > V3) \land ((2 * V3) > 0) \land (V3 > 0))))$	Induction magnitude2
$(((\exists X) \land (X \in integers) \land (\exists Y) \land (Y \in integers) \land (\exists V2) \land (V2 \in integers) \land (\exists V3) \land (V3 \in integers) \land \neg ((X > 0) \land (Y > 0) \land ((2 * X * X) = (Y * Y)) \land ((\forall V0) \land (V0 \in integers) \land (\forall V1) \land (V1 \in integers) \land (V0 > 0) \land (V1 > 0) \land ((2 * V0 * V0) = (V1 * V1)) \Rightarrow (\neg (X > V0))) \land factor (2, (Y * Y)) \land ((2 * V2) = Y) \land ((2 * V2) > 0) \land (V2 > 0) \land ((2 * X * X) = (2 * V2 * 2 * V2)) \land ((V2 * 2 * V2) = (X * X)) \land factor (2, (X * X)) \land ((2 * V3) = X) \land ((V2 * 2 * V2) = (2 * V3 * 2 * V3)) \land (X > V3) \land ((2 * V3) > 0) \land (V3 > 0) \land ((V3 * 2 * V3) = (V2 * V2)))))$	Induction division
$true$	Induction local