2 is prime proof

Step	Using
$(prime (2))$
$((\forall Y) \land (Y \in integers) \land factor (Y, 2) \land (Y > 0) \Rightarrow ((Y = 1) \lor (Y = 2)))$	Deduction prime
$((\forall Y) \land (Y \in integers) \land factor (Y, 2) \land (Y > 0) \land (Y \neq 0) \land (\neg (0 > Y)) \Rightarrow ((Y = 1) \lor (Y = 2)))$	Induction ordering
$(((\forall Y) \land (Y \in integers) \land \neg (factor (Y, 2) \land (Y > 0) \land (Y \neq 0) \land (\neg (0 > Y)) \land (Y \neq 1) \land (Y \neq 2))))$	Inversion
$(((\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land \neg ((Y > 0) \land (Y \neq 0) \land (\neg (0 > Y)) \land (Y \neq 1) \land (Y \neq 2) \land ((Y * V0) = 2))))$	Induction factor
$(((\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land \neg ((Y > 0) \land (Y \neq 0) \land (\neg (0 > Y)) \land (Y \neq 1) \land (Y \neq 2) \land ((Y * V0) = 2) \land (V0 > 0))))$	Induction times_range1
$(((\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land \neg ((Y > 0) \land (Y \neq 0) \land (\neg (0 > Y)) \land (Y \neq 1) \land (Y \neq 2) \land ((Y * V0) = 2) \land (V0 > 0) \land (\neg (Y > 2)))))$	Induction times_range2
$(((\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land \neg ((Y > 0) \land (Y \neq 0) \land (\neg (0 > Y)) \land (Y \neq 1) \land (Y \neq 2) \land ((Y * V0) = 2) \land (V0 > 0) \land (\neg (Y > 2)) \land (\neg (V0 > 2)))))$	Induction times_range2
$true$	Exhaustion