Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
subsf
Next ⟩
subsfo
Metamath Proof Explorer
Ascii
Unicode
Theorem
subsf
Description:
Function statement for surreal subtraction.
(Contributed by
Scott Fenton
, 17-May-2025)
Ref
Expression
Assertion
subsf
⊢
-
s
:
No
×
No
⟶
No
Proof
Step
Hyp
Ref
Expression
1
negscl
⊢
y
∈
No
→
+
s
⁡
y
∈
No
2
addscl
⊢
x
∈
No
∧
+
s
⁡
y
∈
No
→
x
+
s
+
s
⁡
y
∈
No
3
1
2
sylan2
⊢
x
∈
No
∧
y
∈
No
→
x
+
s
+
s
⁡
y
∈
No
4
3
rgen2
⊢
∀
x
∈
No
∀
y
∈
No
x
+
s
+
s
⁡
y
∈
No
5
df-subs
⊢
-
s
=
x
∈
No
,
y
∈
No
⟼
x
+
s
+
s
⁡
y
6
5
fmpo
⊢
∀
x
∈
No
∀
y
∈
No
x
+
s
+
s
⁡
y
∈
No
↔
-
s
:
No
×
No
⟶
No
7
4
6
mpbi
⊢
-
s
:
No
×
No
⟶
No