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