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