Metamath Proof Explorer


Theorem readdid2

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

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

Proof

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