Metamath Proof Explorer

Theorem re0m0e0

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

Ref Expression
Assertion re0m0e0 
|- ( 0 -R 0 ) = 0

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( T. -> 0 e. RR )
2 sn-00id 
 |-  ( 0 + 0 ) = 0
3 2 a1i 
 |-  ( T. -> ( 0 + 0 ) = 0 )
4 1 1 3 reladdrsub 
 |-  ( T. -> 0 = ( 0 -R 0 ) )
5 4 mptru 
 |-  0 = ( 0 -R 0 )
6 5 eqcomi 
 |-  ( 0 -R 0 ) = 0