Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
subscl
Next ⟩
subscld
Metamath Proof Explorer
Ascii
Unicode
Theorem
subscl
Description:
Closure law for surreal subtraction.
(Contributed by
Scott Fenton
, 3-Feb-2025)
Ref
Expression
Assertion
subscl
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
∈
No
Proof
Step
Hyp
Ref
Expression
1
subsval
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
=
A
+
s
+
s
⁡
B
2
negscl
⊢
B
∈
No
→
+
s
⁡
B
∈
No
3
addscl
⊢
A
∈
No
∧
+
s
⁡
B
∈
No
→
A
+
s
+
s
⁡
B
∈
No
4
2
3
sylan2
⊢
A
∈
No
∧
B
∈
No
→
A
+
s
+
s
⁡
B
∈
No
5
1
4
eqeltrd
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
∈
No