This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem readdlid

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

Ref Expression
Assertion readdlid ⊢ A ∈ ℝ → 0 + A = A

Proof

Step Hyp Ref Expression
1 re0m0e0 ⊢ 0 - ℝ 0 = 0
2 1 oveq1i ⊢ 0 - ℝ 0 + A = 0 + A
3 reneg0addlid ⊢ A ∈ ℝ → 0 - ℝ 0 + A = A
4 2 3 eqtr3id ⊢ A ∈ ℝ → 0 + A = A