Metamath Proof Explorer


Theorem reneg0addid2

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

Ref Expression
Assertion reneg0addid2 ( 𝐴 ∈ ℝ → ( ( 0 − 0 ) + 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 elre0re ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
2 rernegcl ( 0 ∈ ℝ → ( 0 − 0 ) ∈ ℝ )
3 elre0re ( 0 ∈ ℝ → 0 ∈ ℝ )
4 renegid ( 0 ∈ ℝ → ( 0 + ( 0 − 0 ) ) = 0 )
5 2 3 4 readdid1addid2d ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 − 0 ) + 𝐴 ) = 𝐴 )
6 1 5 mpancom ( 𝐴 ∈ ℝ → ( ( 0 − 0 ) + 𝐴 ) = 𝐴 )