Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
subsval
Next ⟩
subsvald
Metamath Proof Explorer
Ascii
Unicode
Theorem
subsval
Description:
The value of surreal subtraction.
(Contributed by
Scott Fenton
, 3-Feb-2025)
Ref
Expression
Assertion
subsval
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
=
A
+
s
+
s
⁡
B
Proof
Step
Hyp
Ref
Expression
1
oveq1
⊢
x
=
A
→
x
+
s
+
s
⁡
y
=
A
+
s
+
s
⁡
y
2
fveq2
⊢
y
=
B
→
+
s
⁡
y
=
+
s
⁡
B
3
2
oveq2d
⊢
y
=
B
→
A
+
s
+
s
⁡
y
=
A
+
s
+
s
⁡
B
4
df-subs
⊢
-
s
=
x
∈
No
,
y
∈
No
⟼
x
+
s
+
s
⁡
y
5
ovex
⊢
A
+
s
+
s
⁡
B
∈
V
6
1
3
4
5
ovmpo
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
=
A
+
s
+
s
⁡
B