I am trying to prove that $x^2 - y^2 = (x-y)(x+y)$. Spivak only defines $x$ and $y$ as numbers that obey some set of axioms, so while it seems to me that we can assume they are elements of a field, he doesn't seem to formalize this notion.
Here is what I have so far. I'll start with a simple lemma that $-(yx) = -yx$. We have: $$yx + (-yx) = (y + (-y))x = 0x = 0$$ and, by uniqueness of the additive inverse, we have $-(yx) = -yx$.
We have: \begin{align*} x^2 - y^2 & = (x^2 + 0) - y^2 & & \text{additive identity} \\ & = (x^2 + (xy + (-(xy)))) - y^2 & & \text{additive inverse} \\ & = (x^2 + (xy + (-(yx)))) - y^2 & & \text{commutativity of mult} \\ & = (x^2 + xy) + (-(yx) - y^2) & & \text{associativity of addition} \\ & = (x^2 + xy) + (-yx - y^2) & & \text{lemma} \\ & = x(x + y) + (-y(x + y)) & & \text{distributivity} \\ & = (x-y)(x+y) & & \text{distributivity} \end{align*} How does this proof look?
Alternate proof based on a comment suggesting that I start from the right-hand side: \begin{align*} (x - y)(x + y) & = x(x + y) + (-y(x+y)) & & \text{distributive law} \\ & = (xx + xy) + ((-yx) - yy) & & \text{distributive law} \\ & = (x^2 + xy) + ((-yx) - y^2) & & \text{definition of square} \\ & = x^2 + (xy + (-yx)) - y^2 & & \text{associativity of addition} \\ & = x^2 + (yx + (-yx)) - y^2 & & \text{commutativity of multiplication} \\ & = x^2 + 0 - y^2 & & \text{additive inverse} \\ & = (x^2 + 0) - y^2 & & \text{associativity of addition} \\ & = x^2 - y^2 & & \text{additive identity} \end{align*} How does this look?