Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
subsid
Next ⟩
subadds
Metamath Proof Explorer
Ascii
Unicode
Theorem
subsid
Description:
Subtraction of a surreal from itself.
(Contributed by
Scott Fenton
, 3-Feb-2025)
Ref
Expression
Assertion
subsid
⊢
A
∈
No
→
A
-
s
A
=
0
s
Proof
Step
Hyp
Ref
Expression
1
subsval
⊢
A
∈
No
∧
A
∈
No
→
A
-
s
A
=
A
+
s
+
s
⁡
A
2
1
anidms
⊢
A
∈
No
→
A
-
s
A
=
A
+
s
+
s
⁡
A
3
negsid
⊢
A
∈
No
→
A
+
s
+
s
⁡
A
=
0
s
4
2
3
eqtrd
⊢
A
∈
No
→
A
-
s
A
=
0
s