How to prove $\forall x,y\in\mathbb{R} : x^3+x^2y=y^2+xy \Leftrightarrow y=x^2\lor y=-x?$

Question

Let $x,y\in\mathbb{R}$

Assume $x^3+x^2y=y^2+xy$

Then $x^2(x+y)=y(x+y)$

Then either $(x+y)=0$ or $(x+y)\ne0$

Assume $x+y=0$

Then $y=-x$

Assume $(x+y)\ne0$

Then $y=x^2$

Then $x^3+x^2y=y^2+xy \Rightarrow y=x^2\lor y=-x$

Now assume $y=x^2\lor y=-x$

Assume $y=x^2$

Then $(x+y)y=(x+y)x^2$ #By definition

Then $xy+y^2=x^3+yx^2$

Then $x^3+x^2y=y^2+xy$

Assume $y=-x$

Then $y+x=0$

Also $x^2\times 0=y\times 0$ #By definition

Then $x^2(x+y)=y(x+y)$

Then $x^3+x^2y=y^2+xy$

Then $x^3+x^2y=y^2+xy \Leftarrow y=x^2\lor y=-x.$

Then $\forall x,y\in\mathbb{R} : x^3+x^2y=y^2+xy \Leftrightarrow y=x^2\lor y=-x.$

I am not sure if the proof is well structured. Could someone check?

Answer 1

This is not feedback on your proof, but instead an alternative proof, which seems a lot shorter and simpler.$ \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{\equiv}{\Leftrightarrow} \newcommand{\then}{\Rightarrow} \newcommand{\when}{\Leftarrow} \newcommand{\true}{\text{true}} \newcommand{\false}{\text{false}} $

Let's just calculate, for all real $\;x,y\;$: $$\calc x^3+x^2y=y^2+xy \op\equiv\hint{LHS: factor out common $\;x^2\;$; RHS: factor out common $\;y\;$} x^2(x+y) = y(y+x) \op\equiv\hint{simplify: divide by $\;x+y\;$, avoiding division by zero} x^2 = y \;\lor\; x+y=0 \op\equiv\hint{arithmetic -- to achieve the stated goal} y = x^2 \;\lor\; y = -x \endcalc$$ This completes the proof.

Note how this proves both directions at the same time, instead of having to do both $\;\then\;$ and $\;\when\;$.

It looks like you wanted to go more into detail for the middle step. Is this perhaps because you were given a list of real number axioms that you must use?