Database
SURREAL NUMBERS
Conway cut representation
Zero and One
sgt0ne0
Next ⟩
sgt0ne0d
Metamath Proof Explorer
Ascii
Unicode
Theorem
sgt0ne0
Description:
A positive surreal is not equal to zero.
(Contributed by
Scott Fenton
, 12-Mar-2025)
Ref
Expression
Assertion
sgt0ne0
⊢
0
s
<
s
A
→
A
≠
0
s
Proof
Step
Hyp
Ref
Expression
1
0sno
⊢
0
s
∈
No
2
sltne
⊢
0
s
∈
No
∧
0
s
<
s
A
→
A
≠
0
s
3
1
2
mpan
⊢
0
s
<
s
A
→
A
≠
0
s