Theorem reneg0addlid

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

	Ref	Expression
Assertion	reneg0addlid	⊢ ( 𝐴 ∈ ℝ → ( ( 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	readdridaddlidd	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 −ℝ 0 ) + 𝐴 ) = 𝐴 )
6	1 5	mpancom	⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 0 ) + 𝐴 ) = 𝐴 )