I have the following problem from the book "How to Prove it" by Daniel J.Velleman.
Prove that $$ \exists z\in \mathbb{R} \forall x \in \mathbb{R}^+ \left[\exists y \in \mathbb{R} (y-x=y/x) \leftrightarrow x \neq z \right]. $$
I have no idea how to deal with the existential quantifier at the beginning. I tried to negate it, but the rest is too complicated. Do you have strategic hints how to proceed? Allowed is first-order logic.
EDIT
Based and the response, I would propose the following proof and kindly ask the community to check if it is correct.
Proof: Let $z=1$, and let x be some arbitrary real number.
$(\rightarrow)$ Suppose $\exists y \in \mathbb{R} (y-x=y/x)$ and choose $y_0$ to be some real number such that $(y_0-x=y_0/x)$. Suppose $x=z$. Since $x=z$ and $z=1$, $x=1$. However, plugging $x=1$ into $y_0-x=y_0/x$ yields a contradiction, and thus, $x\neq z$. Hence, $\exists y \in \mathbb{R} (y-x=y/x) \rightarrow x \neq z$. Since $x$ was arbitrary, it follows that $\forall x \in \mathbb{R}^+ \left[\exists y \in \mathbb{R} (y-x=y/x) \rightarrow x \neq z \right]$.
($\leftarrow$) Suppose $x \neq z$. Since $z=1$, $x \neq 1$. Let $y_0=\frac{x^2}{x-1}$, which is defined because $x \neq 1$. Plugging into the equation $y_0-x=y_0/x$, we can verify that the equation holds for this particular value $y_0$. Hence, $x \neq z \rightarrow \exists y \in \mathbb{R} (y-x=y/x)$. Since x was arbitrary, it follows that $\forall x \in \mathbb{R}^+ \left[\exists y \in \mathbb{R} (y-x=y/x) \leftarrow x \neq z \right]$.
Therefore, the theorem follows.
The way to prove $\exists z\in \mathbb R\,\cdots $ is always to show a particular number $z$ with the given property. So before you can start writing down a proof, you will need to find such a number.
More precisely, the statement to be proved has the form $$ \exists z.\forall x.(P(x)\leftrightarrow x\ne z) $$ which says that all $x$ except exactly one have the property $P(x)$. -- Or, since $x$ is restricted to positive numbers, perhaps all $x$ do have the property $P(x)$, in which case $z=-42$ will work.
So you're looking for the unique $x$ such that the equation $y-x=y/x$ does not have a solution for $y$, or for a proof that $y-x=y/x$ has a solution for every positive $x$.