Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
addsubsd
Next ⟩
sltsubsubbd
Metamath Proof Explorer
Ascii
Unicode
Theorem
addsubsd
Description:
Law for surreal addition and subtraction.
(Contributed by
Scott Fenton
, 4-Mar-2025)
Ref
Expression
Hypotheses
addsubsassd.1
⊢
φ
→
A
∈
No
addsubsassd.2
⊢
φ
→
B
∈
No
addsubsassd.3
⊢
φ
→
C
∈
No
Assertion
addsubsd
⊢
φ
→
A
+
s
B
-
s
C
=
A
-
s
C
+
s
B
Proof
Step
Hyp
Ref
Expression
1
addsubsassd.1
⊢
φ
→
A
∈
No
2
addsubsassd.2
⊢
φ
→
B
∈
No
3
addsubsassd.3
⊢
φ
→
C
∈
No
4
3
negscld
⊢
φ
→
+
s
⁡
C
∈
No
5
1
2
4
adds32d
⊢
φ
→
A
+
s
B
+
s
+
s
⁡
C
=
A
+
s
+
s
⁡
C
+
s
B
6
1
2
addscld
⊢
φ
→
A
+
s
B
∈
No
7
6
3
subsvald
⊢
φ
→
A
+
s
B
-
s
C
=
A
+
s
B
+
s
+
s
⁡
C
8
1
3
subsvald
⊢
φ
→
A
-
s
C
=
A
+
s
+
s
⁡
C
9
8
oveq1d
⊢
φ
→
A
-
s
C
+
s
B
=
A
+
s
+
s
⁡
C
+
s
B
10
5
7
9
3eqtr4d
⊢
φ
→
A
+
s
B
-
s
C
=
A
-
s
C
+
s
B