Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
pncan2s
Next ⟩
npcans
Metamath Proof Explorer
Ascii
Unicode
Theorem
pncan2s
Description:
Cancellation law for surreal subtraction.
(Contributed by
Scott Fenton
, 16-Apr-2025)
Ref
Expression
Assertion
pncan2s
⊢
A
∈
No
∧
B
∈
No
→
A
+
s
B
-
s
A
=
B
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
A
+
s
B
=
A
+
s
B
2
addscl
⊢
A
∈
No
∧
B
∈
No
→
A
+
s
B
∈
No
3
simpl
⊢
A
∈
No
∧
B
∈
No
→
A
∈
No
4
simpr
⊢
A
∈
No
∧
B
∈
No
→
B
∈
No
5
2
3
4
subaddsd
⊢
A
∈
No
∧
B
∈
No
→
A
+
s
B
-
s
A
=
B
↔
A
+
s
B
=
A
+
s
B
6
1
5
mpbiri
⊢
A
∈
No
∧
B
∈
No
→
A
+
s
B
-
s
A
=
B