Metamath Proof Explorer

Theorem readdlid

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

Ref Expression
Assertion readdlid 
|- ( 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 reneg0addlid 
 |-  ( A e. RR -> ( ( 0 -R 0 ) + A ) = A )
4 2 3 eqtr3id 
 |-  ( A e. RR -> ( 0 + A ) = A )