Metamath Proof Explorer


Theorem readdid2

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

Ref Expression
Assertion readdid2
|- ( A e. RR -> ( 0 + A ) = A )

Proof

Step Hyp Ref Expression
1 re0m0e0
 |-  ( 0 -R 0 ) = 0
2 1 oveq1i
 |-  ( ( 0 -R 0 ) + A ) = ( 0 + A )
3 reneg0addid2
 |-  ( A e. RR -> ( ( 0 -R 0 ) + A ) = A )
4 2 3 eqtr3id
 |-  ( A e. RR -> ( 0 + A ) = A )