I have to formalize the following mathematical statement in a predicate logic in a language L = {+, *, 0, 1, <} :
"There are infinitely many prime numbers"
I have found the following formalization but it is not clear to me why there is a necesity to embed another variable $d$ inside the formula. Formalization is the following:
$(\forall x)(\exists y)[x < y \land (\forall d)((\exists p)(p * d = y)\rightarrow (d = 1 \vee d = y))]$
Is it possible to write instead this? If not, why?:
$(\forall x)(\exists y)[x < y \land ((\exists p)(p * x = y)\rightarrow (x = 1 \vee x = y))]$