Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
npcans
Next ⟩
sltsub1
Metamath Proof Explorer
Ascii
Unicode
Theorem
npcans
Description:
Cancellation law for surreal subtraction.
(Contributed by
Scott Fenton
, 4-Feb-2025)
Ref
Expression
Assertion
npcans
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
+
s
B
=
A
Proof
Step
Hyp
Ref
Expression
1
subscl
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
∈
No
2
simpr
⊢
A
∈
No
∧
B
∈
No
→
B
∈
No
3
1
2
addscomd
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
+
s
B
=
B
+
s
A
-
s
B
4
pncan3s
⊢
B
∈
No
∧
A
∈
No
→
B
+
s
A
-
s
B
=
A
5
4
ancoms
⊢
A
∈
No
∧
B
∈
No
→
B
+
s
A
-
s
B
=
A
6
3
5
eqtrd
⊢
A
∈
No
∧
B
∈
No
→
A
-
s
B
+
s
B
=
A