Metamath Proof Explorer


Theorem readdid2

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

Ref Expression
Assertion readdid2 A 0 + A = A

Proof

Step Hyp Ref Expression
1 re0m0e0 0 - 0 = 0
2 1 oveq1i 0 - 0 + A = 0 + A
3 reneg0addid2 A 0 - 0 + A = A
4 2 3 eqtr3id A 0 + A = A