2

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.

Carl Mummert
  • 81,604
Eugene
  • 719

3 Answers3

1

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$.

0

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$.

coldnumber
  • 3,721
0

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$$