Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
pncan3s
Next ⟩
pncan2s
Metamath Proof Explorer
Ascii
Unicode
Theorem
pncan3s
Description:
Subtraction and addition of equals.
(Contributed by
Scott Fenton
, 4-Feb-2025)
Ref
Expression
Assertion
pncan3s
⊢
A
∈
No
∧
B
∈
No
→
A
+
s
B
-
s
A
=
B
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
B
-
s
A
=
B
-
s
A
2
simpr
⊢
A
∈
No
∧
B
∈
No
→
B
∈
No
3
simpl
⊢
A
∈
No
∧
B
∈
No
→
A
∈
No
4
2
3
subscld
⊢
A
∈
No
∧
B
∈
No
→
B
-
s
A
∈
No
5
2
3
4
subaddsd
⊢
A
∈
No
∧
B
∈
No
→
B
-
s
A
=
B
-
s
A
↔
A
+
s
B
-
s
A
=
B
6
1
5
mpbii
⊢
A
∈
No
∧
B
∈
No
→
A
+
s
B
-
s
A
=
B