Don't understand theorem $\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 am reading a book on proof-writing techniques. One of the main ideas is that whenever you want to prove a statement starting with existential quantifier, you must choose a particular instance of an object, such that what follows is true. It is called "existential instantiation".
There is a theorem in the exercises that I am given to prove.
$\textbf{Theorem:}$ $\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] $.
$\textbf{Proof:}$ At this point I am already confused. Do I get it right that in this case I must use existential instantiation and proceed to choose a particular value of $z$, let's say $z_0 \in \mathbb{R}$ such that $\forall x \in \mathbb{R}^+ \left[ \exists y \in \mathbb{R} (y - x = y / x) \leftrightarrow x \neq z_0 \right]$?
Then I move on and choose an arbitrary $x \in \mathbb{R}^+$ ("universal instantiation").
So now I have to prove $\exists y \in \mathbb{R} (y - x = y / x) \leftrightarrow x \neq z_0$.
($\rightarrow$) Assume $\exists y \in \mathbb{R} (y - x = y / x)$. Then I must prove that $x \neq z_0$. Again, using existential instantiation, I choose a particular $y$, say $y_0 \in \mathbb{R}$ such that $ (y_0 - x = y_0 / x)$. At this point it gets really interesting. How do I show that $ (y_0 - x = y_0 / x) \rightarrow x \neq z_0$ if the expression on the left does not even have $z_0$?!
($\leftarrow$) I need to prove that $x \neq z_0 \rightarrow \exists y \in \mathbb{R} (y - x = y / x)$. I must show that there does exist a $y$ that works. Consider $y = (x^2 + x) / (x - 1)$. This particular $y$ is going to work. But again, I don't see how that follows from the fact that $x \neq z_0$!
So my idea so far is that this exercise is given to let us understand some point about existential instantiations, and that is exactly the point I don't seem to get. And this tricky $z$ is ruining everything, we could completely throw it away and nothing would have changed.
$\textbf{So my question is:}$ how exactly do we prove this theorem and what am I missing to complete the proof?
 A: To add a bit to the comments: existential instantiation is generally something that you use when you already have an existentially quantified sentence (say, in the premises). Here, what you need is to prove an existentially quantified sentence. In order to do this, the best way is to exhibit the particular $z$ in question. This is easier to see in practice, so I'll prove an easier theorem just to show you what I mean. 
Suppose I want to prove, from the field axioms, that $\forall x \forall z \exists y (x = y + z)$ (i.e. that subtraction is possible). So what do I do? I need to work with arbitrary numbers, which I'll be able to (in this case) universally generalize, and with a specific number that I want to existentially quantify over. Let's go over this in steps.
(1) So let $x$ and $z$ be arbitrary numbers. 
(2) By the field axioms, we know that there is a number, called $-z$, such that $z + (-z) = 0$. 
(3) So choose $y$ such that $y = -z + x$ (which we know to exist, since addition is well defined according to these axioms);
(4) Now consider $z + y$, which, again, we know to be well defined.
(5) By using simple identity laws, plus associativity, $z + y = z + ((-z) + x)  = (z + (-z)) + x = 0 + x = x$.
(6) Since $x$ and $z$ were arbitrary, for every $x$ and $z$, there is a desired $y$ that proves the theorem.
Notice that the crucial step in the above proof is (3), where I deliberately chose a $y$ that I knew would give the desired result. That's generally the trick when your goal is to prove existentially quantified sentences: you don't want to deal with arbitrary objects, but with specifically chosen ones. In your particular case, you have to carefully select a $z$ that will give you the desired result. Obviously, you won't always be able to discover which object is the necessary one; in this case, the only resource we have left to prove an existentially quantified statement is to argue by contradiction (i.e. suppose there is no such $z$; then contradiction ensues).
A: First of all you need to read the sentence as in ordinary language first so that quantifiers are not mind boggling.
The statement is saying that there is a real number z such that 
corresponding to each positive real number x, there exists a real number y such that the equation y-x = y/x holds if and only if x does not take the value z.
Since we need to prove (at the most outside level of logical parantheses) existence of such a z, one way of doing so is actually producing a concrete value for z such that the statement is valid.
Now let's look at the rest of the sentence. corresponding to each positive real x, arguing existence of real y , means that for any positive real value of x outside some specified value(s) z, one can solve the equation for y in terms of x.
Equation "y-x = y /x " holds if and only if  "yx-x^2 = y " (multiplying by nonzero x on both sides) if and only if "y(x-1) = x^2 " (after adding x^2 -y on both sides and factoring on left hand side) if and only if "y = x^2 / (x-1)" where division is justified only when x is not equal to 1. But in this final step we have solved for y in terms of x.
In other words we have evaluated (through logical equivalences said in words) that when x is not equal to 1 ( so z = 1) that when y takes the value  x^2 / (x-1) the said equation  holds.
A: We can try with a simpler example (I'll use only one "direction" of the bi-conditional) :

$\forall x \in \mathbb N [\exists y \in \mathbb N (x \ne 0 \rightarrow (y < x) )]$.

Here a "rough-cut" proof :

Assume : $x \ne 0$
Then, using Peano's axioms :
$x=S(y)$, for some $y$ [where $S$ is the successor function].
Again by axioms :
$x=S(y)+0=S(y+0)=y+S(0)$.
Now we can use the abbreviation : $y < x \leftrightarrow \exists w (x = y + S(w))$ to conlcude with :

$y < x$, for some $y$.

Thus, from $x \ne 0 \vdash \exists y (y < x)$, we have :
$x \ne 0 \rightarrow \exists y (y < x)$
and, by properties of quantifiers [$y$ is not free in $x \ne 0$] :

$\exists y (x \ne 0 \rightarrow (y < x))$.

This is true for $x$ whatever; thus :

$\forall x [\exists y (x \ne 0 \rightarrow (y < x) )]$.

Only now we can use $\exists$-intro [from : $\varphi(t)$, infer : $\exists x \varphi(x)$, with $0$ as the term $t$] to conclude with :


$\exists z\forall x [\exists y (x \ne z \rightarrow (y < x) )]$.


