Yes, you can prove it with "usual" proof systems : Resolution, Tableaux or with Natural Deduction :
1) $∀z∀x∃y(R(z,y)∨¬P(x))$ --- premise
2) $∃xP(x)$ --- assumed [a]
3) $P(w)$ --- assumed [b] for $\exists$-elimination
4) $∃y(R(z,y)∨¬P(w))$ --- from 1) by $\forall$-elimination twice
5) $R(z,y)∨¬P(w)$ --- assumed [c] for $\exists$-elimination
6) $P(w) \to R(z,y)$ --- from 5) by tautological equivalence : $(p \to q) \leftrightarrow (\lnot p \lor q)$
7) $R(z,y)$ --- from 3) and 6) by $\to$-elimination
8) $\exists yR(z,y)$ --- from 7) by $\exists$-introduction
9) $\forall x \exists yR(x,y)$ --- from 8) by $\forall$-introduction : $x$ is not free in any "open" assumptions
$y$ is not free in 9); thus, we can apply $\exists$-elimination with 4), 5) and 9) and conclude with :
10) $\forall x \exists yR(x,y)$, discharging assumption [c].
In the same way, from 2), 3) and 10), discharging assumption [b] and concluding with :
11) $\forall x \exists yR(x,y)$.
Finally :
$∃xP(x) \to \forall x \exists yR(x,y)$ --- from 2) and 11) by $\to$-introduction, discharging assumption [a].
With a final application of $\to$-introduction we conclude with :
$∀z∀x∃y(R(z,y)∨¬P(x)) \to (∃xP(x) \to ∀x∃yR(x,y))$.
Best Answer
The challenge here is that there is no a priori bound on the number of factors. So, to express the fundamental theorem of arithmetic in a first-order theory such as Peano arithmetic, you first need to show that the theory is able to express the idea of quantifying over finite sequences. The machinery to do this is well understood; one commonly used method is the $\beta$ function introduced by Kurt Gödel.
The general idea is that the final sentence will say "for every $n > 1$ there is a finite sequence $\sigma$ such that (1) each number appearing in $\sigma$ is prime, and (2) $n$ is the product of the numbers appearing in $\sigma$."