Metamath Proof Explorer

Theorem reneg0addid2

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

Ref Expression
Assertion reneg0addid2 
|- ( A e. RR -> ( ( 0 -R 0 ) + A ) = A )

Proof

Step Hyp Ref Expression
1 elre0re 
 |-  ( A e. RR -> 0 e. RR )
2 rernegcl 
 |-  ( 0 e. RR -> ( 0 -R 0 ) e. RR )
3 elre0re 
 |-  ( 0 e. RR -> 0 e. RR )
4 renegid 
 |-  ( 0 e. RR -> ( 0 + ( 0 -R 0 ) ) = 0 )
5 2 3 4 readdid1addid2d 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( ( 0 -R 0 ) + A ) = A )
6 1 5 mpancom 
 |-  ( A e. RR -> ( ( 0 -R 0 ) + A ) = A )