Metamath Proof Explorer


Theorem readdid1

Description: Real number version of addid1 , without ax-mulcom . (Contributed by SN, 23-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 resubid
 |-  ( A e. RR -> ( A -R A ) = 0 )
2 id
 |-  ( A e. RR -> A e. RR )
3 elre0re
 |-  ( A e. RR -> 0 e. RR )
4 2 2 3 resubaddd
 |-  ( A e. RR -> ( ( A -R A ) = 0 <-> ( A + 0 ) = A ) )
5 1 4 mpbid
 |-  ( A e. RR -> ( A + 0 ) = A )