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