Proof strategy involving first order logic for existential quantification at very beginning 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.
 A: 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$.
A: Velleman provides a template for these. For example (broadly paraphrased):

To prove $\exists z (\ldots)$, write:
  Let $z =$ [some value you decide on]. [Then prove $\ldots$]
To prove $\forall x (\ldots)$, write:
  Let $x$ be arbitrary. [Then prove $\ldots$]
To prove $P \leftrightarrow Q$, prove $P \rightarrow Q$ and $Q \rightarrow P$.
To prove $P \rightarrow Q$, write: Suppose $P$. [Then prove $Q$.]
To use $\exists y (\ldots)$, use the fact that there's some $y_0$ which satisfies $\ldots$

So the structure of your proof is going to be:

Let $z =$ [some real number you decide on]. Let $x$ be an arbitrary positive real number.
Suppose $\exists y\in\mathbb{R}(y-x = y/x)$. Consider $y_0$ which satisfies this. Thus $y_0 - x = y_0/x$. [Now prove $x \neq z$.]
Suppose $x \neq z$. Let $y =$ [some real number you decide on, possibly depending on $x$]. [Now prove $y-x=y/x$.]

So you can see what you need to do. You need to find a value $z$ such that you'll be able to complete the rest of the proof. For the second paragraph, you'll need to be able to use $y_0-x = y_0/x$ to prove $x$ is not equal to $z$. And in the third paragraph you'll need to use $x \neq z$ to prove that you can find $y$ such that $y-x=y/x$.
So to figure out a $z$ that will work (i.e. let you complete the proof), you need to see for what values of $x$ you can solve $y-x = y/x$ (for $y$, with $x$ fixed). If there's one value of $x$ that gives you trouble, set $z$ to be that, then fill in the details for the proof.
