2 is prime test

Prove:

$(prime (2))$

Given:

Axiom	Definition
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))$
times_range1	$((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (X > 0) \land ((X * Y) > 0) \Rightarrow (Y > 0))$
times_range2	$((\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 > 0) \land (Z > 0) \Rightarrow (\neg (Y > Z)))$
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) \Leftrightarrow (X > 1) \land ((\forall Y) \land (Y \in integers) \land factor (Y, X) \land (Y > 0) \Rightarrow ((Y = 1) \lor (Y = X)))$