Theorem readdlid

Description: Real number version of addlid . (Contributed by SN, 23-Jan-2024)

	Ref	Expression
Assertion	readdlid	$$⊢A\in ℝ\to 0+A=A$$

Proof

Step	Hyp	Ref	Expression
1		re0m0e0	$$⊢0{-}_{ℝ}0=0$$
2	1	oveq1i	$$⊢\left(0{-}_{ℝ}0\right)+A=0+A$$
3		reneg0addlid	$$⊢A\in ℝ\to \left(0{-}_{ℝ}0\right)+A=A$$
4	2 3	eqtr3id	$$⊢A\in ℝ\to 0+A=A$$