[carloswilson]

> You literally cannot prove this fact from the Peano axioms because Peano arithmetic operates on natural numbers, not integers.

Sure you can. With definitions! Define integers from natural numbers. Define rationals from integers. And so on. And so on.

> The number -2 is an entity that exists by itself regardless of whether you've defined an additive inverse.

I see a serious misunderstanding of this topic. Please read upon the field axioms and ring axioms if you haven't so already. Then please check https://math.stackexchange.com/a/878844 which is arguably more rigorous than this post. But the essence is the same. This is more rigorous because the subtraction operator is not used anywhere. Only addition, multiplication and additive inverses have been used. Like another commenter said, if you just replace subtraction with addition with an additive inverse in the OP's post, things fall in place.