Metamath Proof Explorer


Theorem reneg0addid2

Description: Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion reneg0addid2 A0-0+A=A

Proof

Step Hyp Ref Expression
1 elre0re A0
2 rernegcl 00-0
3 elre0re 00
4 renegid 00+0-0=0
5 2 3 4 readdid1addid2d 0A0-0+A=A
6 1 5 mpancom A0-0+A=A