Description: Real number version of addid2 . (Contributed by SN, 23-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | readdid2 | ⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | re0m0e0 | ⊢ ( 0 −ℝ 0 ) = 0 | |
2 | 1 | oveq1i | ⊢ ( ( 0 −ℝ 0 ) + 𝐴 ) = ( 0 + 𝐴 ) |
3 | reneg0addid2 | ⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 0 ) + 𝐴 ) = 𝐴 ) | |
4 | 2 3 | eqtr3id | ⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 ) |