Factor of is transitive proof

Step	Using
$((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\forall Z) \land (Z \in integers) \land factor (X, Y) \land factor (Y, Z) \Rightarrow factor (X, Z))$
$(((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\forall Z) \land (Z \in integers) \land \neg (factor (X, Y) \land factor (Y, Z) \land (\neg factor (X, Z)))))$	Inversion
$(((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land (\forall Z) \land (Z \in integers) \land \neg (factor (X, Y) \land (\neg factor (X, Z)) \land ((Y * V0) = Z))))$	Induction factor
$(((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land (\forall Z) \land (Z \in integers) \land \neg (factor (X, Y) \land (\neg factor (X, Z)) \land ((Y * V0) = Z) \land (\neg factor (X, (Y * V0))))))$	Inference
$(((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land (\forall Z) \land (Z \in integers) \land \neg (factor (X, Y) \land (\neg factor (X, Z)) \land ((Y * V0) = Z) \land (\neg factor (X, (Y * V0))) \land factor (Y, Z))))$	Induction factor
$(((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land (\forall Z) \land (Z \in integers) \land \neg (factor (X, Y) \land (\neg factor (X, Z)) \land ((Y * V0) = Z) \land (\neg factor (X, (Y * V0))) \land factor (Y, Z) \land factor (Y, (Y * V0)))))$	Inference
$(((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land (\forall Z) \land (Z \in integers) \land (\exists V1) \land (V1 \in integers) \land \neg ((\neg factor (X, Z)) \land ((Y * V0) = Z) \land (\neg factor (X, (Y * V0))) \land factor (Y, Z) \land factor (Y, (Y * V0)) \land ((X * V1) = Y))))$	Induction factor
$(((\forall X) \land (X \in integers) \land (\forall Y) \land (Y \in integers) \land (\exists V0) \land (V0 \in integers) \land (\forall Z) \land (Z \in integers) \land (\exists V1) \land (V1 \in integers) \land \neg ((\neg factor (X, Z)) \land ((Y * V0) = Z) \land (\neg factor (X, (Y * V0))) \land factor (Y, Z) \land factor (Y, (Y * V0)) \land ((X * V1) = Y) \land ((X * V1 * V0) = Z))))$	Inference
$true$	Induction factor