# Does this in complete detail prove $\forall x, y \in N, x + (y + 0) = (x + y) + 0$?

My goal is to prove math theorems without skipping any steps. Is this proof correct?

Question 1 says to prove the following from Peano Axioms: $$\forall x, y \in N, x + (y + 0) = (x + y) + 0$$.

1. Axiom: $$\forall x (x + 0 = x)$$, therefore $$\forall y (y + 0 = y)$$ (substituting $$x$$ for $$y$$).

2. Axiom: $$\forall x (x=x)$$ therefore $$\forall x, y \in N, x + (y + 0) = x + (y + 0)$$. Can you do this in a single step? Or would you need to build up the expression on either side?

3. 2: $$\forall x, y \in N, x + (y + 0) = x + (y + 0)$$ and 1: $$\forall y (y + 0 = y)$$ therefore $$\forall x, y \in N, x + (y + 0) = x + y$$ (substituted the second instance of $$(y + 0)$$ for $$y$$).

4. Axiom: $$\forall x (x + 0 = x)$$, therefore $$\forall x,y ((x + y) + 0 = (x + y))$$ (substituting $$x$$ for $$(x + y)$$). Is this valid?

5. Axiom: $$\forall a,b ((a = b) \implies (b = a))$$ and 4: $$\forall x,y (((x + y) + 0) = (x + y)))$$ therefore $$\forall x,y ((x + y) = ((x + y) + 0))$$ (substituting $$((x + y) + 0)$$ for $$a$$ and $$(x + y)$$ for $$b$$).

6. 3: $$\forall x, y \in N, x + (y + 0) = x + y$$ and $$\forall x,y ((x + y) = ((x + y) + 0))$$ therefore $$\forall x, y \in N, x + (y + 0) = (x + y) + 0$$ (substituting $$((x + y) + 0)$$ for $$(x + y)$$). Question 1 has been proved.

Something that puzzles me - does this mean $$\forall x (x=x)$$ that $$x$$ doesn't have to be used by substituting a constant like $$1$$, $$2$$, etc. but can be an expression like $$a+b$$?

To answer you last question, yes - $$\forall x P(x)$$ lets you substitute any expression for $$x$$, as long as you do it carefully. For example, when you have an expression like $$xy$$ then substituting $$a+b$$ for $$y$$ needs to be protected with parentheses, i.e. you get $$x(a+b)$$ rather than $$xa+b$$ since those are two very different things.
As for your proof, it looks pretty good. At this level of rigor, all of the steps are required, but once you get past the foundational proofs it's standard to leave some of the details as given (e.g. basic algebraic manipulation like swapping $$a=b$$ and $$b=a$$ doesn't require stating an axiom).
"Let $$a$$ and $$b$$ be any numbers. Given the axiom that says that $$\forall x \ x + 0 = 0$$, we can say that $$(a + b) + 0 = a + b$$. ...[bla bla] ... and therefore $$a + (b + 0) = (a + b) + 0$$. Since $$a$$ and $$b$$ were arbitrary, this means $$\forall x \forall y \ x + (y + 0) = (x + y) + 0$$."