Description: Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | reneg0addid2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elre0re | |
|
2 | rernegcl | |
|
3 | elre0re | |
|
4 | renegid | |
|
5 | 2 3 4 | readdid1addid2d | |
6 | 1 5 | mpancom | |