Metamath Proof Explorer
Description: Real number version of 0m0e0 proven without ax-mulcom . (Contributed by SN, 23-Jan-2024)
|
|
Ref |
Expression |
|
Assertion |
re0m0e0 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
0red |
|
2 |
|
sn-00id |
|
3 |
2
|
a1i |
|
4 |
1 1 3
|
reladdrsub |
|
5 |
4
|
mptru |
|
6 |
5
|
eqcomi |
|