Description: Real number version of addid2 . (Contributed by SN, 23-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | readdid2 | |- ( A e. RR -> ( 0 + A ) = A ) |
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 ) |