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 − 0 ) = 0

Proof

Step Hyp Ref Expression
1 0red ( ⊤ → 0 ∈ ℝ )
2 sn-00id ( 0 + 0 ) = 0
3 2 a1i ( ⊤ → ( 0 + 0 ) = 0 )
4 1 1 3 reladdrsub ( ⊤ → 0 = ( 0 − 0 ) )
5 4 mptru 0 = ( 0 − 0 )
6 5 eqcomi ( 0 − 0 ) = 0