Theorem reneg0addlid

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

	Ref	Expression
Assertion	reneg0addlid	$$⊢A\in ℝ\to \left(0{-}_{ℝ}0\right)+A=A$$

Proof

Step	Hyp	Ref	Expression
1		elre0re	$$⊢A\in ℝ\to 0\in ℝ$$
2		rernegcl	$$⊢0\in ℝ\to 0{-}_{ℝ}0\in ℝ$$
3		elre0re	$$⊢0\in ℝ\to 0\in ℝ$$
4		renegid	$$⊢0\in ℝ\to 0+\left(0{-}_{ℝ}0\right)=0$$
5	2 3 4	readdridaddlidd	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0{-}_{ℝ}0\right)+A=A$$
6	1 5	mpancom	$$⊢A\in ℝ\to \left(0{-}_{ℝ}0\right)+A=A$$