Database
SURREAL NUMBERS
Conway cut representation
Cuts and Options
new0
Next ⟩
old1
Metamath Proof Explorer
Ascii
Unicode
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