Prove that $\exists z \in \mathbb R\forall x \in \mathbb R^+[\exists y \in \mathbb R(y-x=y/x) \iff x \neq z]$ This is Velleman's exercise 3.4.13: 

Prove that $\exists z \in \mathbb R\forall x \in \mathbb R^+[\exists y \in \mathbb R(y-x=y/x) \iff x \neq z]$. 

I am am stuck on that one. Seems like I am missing something. Besides I am having issues using the first term, i.e. $ z \in \mathbb R$. A proof in real Velleman expository style would be highly appreciated. Thanks in advance. 
 A: Try looking at it from the inside out, and see what consequences follow from $y-x=y/x$. One is $y=x^2/(x-1)$ provided $x\not=1$.But what if $x=1$? Then $y-x=y/x$ implies $y-1=y$,which is absurd.So $y$ exists iff $x\not=1$.Reading further outward we should now have: "$y$ exists" iff $x\not=1$ iff $x\not=z$.This must hold for all $x$, so obviously $z=1$.
A: You want to prove a statement of existence, so you want to find a number $z$ satisfying the conditions. 
To do this, you can move things around in the $y-x=y/x$ expression; solving for $y$, you get $$y=\frac{x^2}{x-1}$$
This form encourages us to look at what happens when $x=1$.
 When $x=1$, the initial expression $y-x=y/x$ becomes $$y-1=y/1 \\y-1=y \\ -1=0$$
We have found a value of $x$ such that there does not exist $y \in \Bbb R$ satisfying the expression. (This is actually the proof of the forward direction.)

So taking $z=1$, we could write the proof as follows:
Let $z=1$. We want to show that $\forall x \in \Bbb R^+$ there exists $y \in \Bbb R$ such that $y-x=\frac yx$ if and only if $x\neq 1$.
We showed above that $x=1$ implies that no such $y$ exists (because assuming it exists leads to the contradiction that $-1=0$), and in that way we proved the forward direction by contrapositive (and we proved the contrapositive by contradiction).
Now we show that backwards direction: Suppose $x\neq 1$. We want to find a number $y \in \Bbb R$ such that $y-x=\frac yx$. 
But solving the expresion for $y$ we get $y=\dfrac{x^2}{x-1}$, which works, because $x\neq 1$.
A: For comparison, here is a proof in a different style than you asked for: the calculational and equational style of Dijkstra/Feijen/Gries/Schneider (see, e.g., EWD1300).  To reduce visual clutter, we will let all variables range over $\;\mathbb R\;$.$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\Ref}[1]{\text{(#1)}}
\newcommand{\then}{\Longrightarrow}
\newcommand{\when}{\Longleftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$
Looking at the shape of our goal, it looks like we should try to simplify $\;\exists y (y−x = y/x)\;$ into something of the form $\;x \not= \ldots\;$.  So let's calculate:
$$\calc
    \exists y (y−x = y/x)
\op\iff\hint{multiply by $\;x\;$; rearrange to get a single $\;y\;$}
    \exists y (y(x-1) = x^2)
\op\iff\hint{divide by $\;x-1\;$, special case $\;x-1=0\;$}
    \exists y ((x-1 = 0 \land 0 = 1^2) \;\lor\; (x-1 \not= 0 \land y = x^2/(x-1))))
\op\iff\hint{left side of $\;\lor\;$ is false; simplify right side of $\;\lor\;$}
    \exists y (x \not= 1 \;\land\; y = x^2/(x-1))
\op\iff\hint{extract conjunct not containing $\;y\;$ out of $\;\exists y\;$}
    x \not= 1 \;\land\; \exists y (y = x^2/(x-1))
\op\iff\hint{right side of $\;\land\;$ is true by one-point rule}
    x \not= 1
\endcalc$$
Now to formally wrap up, we've proven $\Ref{*}$ which we can weaken to achieve our goal:
$$\calc
    \tag{*}
    \forall x [\exists y (y−x = y/x) \;\iff\; x \not= 1]
\op\then\hint{limit range of $\;x\;$ from $\;\mathbb R\;$ to $\;\mathbb R^+\;$}
    \forall x \in \mathbb R^+ [\exists y (y−x = y/x) \;\iff\; x \not= 1]
\op\then\hint{choose $\;z := 1\;$}
    \exists z \forall x \in \mathbb R^+ [\exists y (y−x = y/x) \;\iff\; x \not= z]
\endcalc$$
