Metamath Proof Explorer


Theorem new0

Description: The only surreal new on day (/) is 0s . (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion new0 N = 0 s

Proof

Step Hyp Ref Expression
1 newval N = M Old
2 made0 M = 0 s
3 old0 Old =
4 2 3 difeq12i M Old = 0 s
5 dif0 0 s = 0 s
6 1 4 5 3eqtri N = 0 s