Theorem readdlid

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

	Ref	Expression
Assertion	readdlid	⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		re0m0e0	⊢ ( 0 −ℝ 0 ) = 0
2	1	oveq1i	⊢ ( ( 0 −ℝ 0 ) + 𝐴 ) = ( 0 + 𝐴 )
3		reneg0addlid	⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 0 ) + 𝐴 ) = 𝐴 )
4	2 3	eqtr3id	⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 )