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