peano arithmetic - PA sentences

Question

In using the non-logical axiom sentences of PA, I was trying a practice problem to get the hang of using the PA sentences:

$((S0 * S0) = S0)$

And so my approach was the following:

1. $\forall x_1((x_1 * 0) = 0)$ - Axiom(v)

2. $((S0 * 0) = 0)$ - 1, Universal elimination

3. $\forall x_1 \forall x_2((x_1 * Sx_2) = ((x_1 * x_2) + x_1))$ - Axiom(vi)

4. $\forall x_2((S0 * Sx_2) = ((S0 * x_2) + S0))$ - 3, universal elimination

5. $((S0 * S0) = ((S0 * 0) + S0))$ - 4, universal elimination

6. $((S0 * S0) = (S0))$ - 2, 5, substitution

When I got to #6, I thought that it looked good, but I can see that I have extra brackets at the end (perhaps I screwed up in my bracket management)

Any clue to what I may have missed, forgot during the proof process?

Thanks for reading and helping!

Answer 1

Substitute 2 in 5 to get:

6. $S0*S0 = 0+S0$

Then you will need to use Axiom iv to get:

7. $0 + S0 = S(0+0)$

Use Axiom iii to get:

8. $0+0=0$

Substitute 8 in 7:

9. $0+S0=S0$

And finally substitute 9 in 6:

10. $S0*S0=S0$