Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
negsubsdi2d
Next ⟩
addsubsassd
Metamath Proof Explorer
Ascii
Unicode
Theorem
negsubsdi2d
Description:
Distribution of negative over subtraction.
(Contributed by
Scott Fenton
, 5-Feb-2025)
Ref
Expression
Hypotheses
negsubsdi2d.1
⊢
φ
→
A
∈
No
negsubsdi2d.2
⊢
φ
→
B
∈
No
Assertion
negsubsdi2d
⊢
φ
→
+
s
⁡
A
-
s
B
=
B
-
s
A
Proof
Step
Hyp
Ref
Expression
1
negsubsdi2d.1
⊢
φ
→
A
∈
No
2
negsubsdi2d.2
⊢
φ
→
B
∈
No
3
2
negscld
⊢
φ
→
+
s
⁡
B
∈
No
4
negsdi
⊢
A
∈
No
∧
+
s
⁡
B
∈
No
→
+
s
⁡
A
+
s
+
s
⁡
B
=
+
s
⁡
A
+
s
+
s
⁡
+
s
⁡
B
5
1
3
4
syl2anc
⊢
φ
→
+
s
⁡
A
+
s
+
s
⁡
B
=
+
s
⁡
A
+
s
+
s
⁡
+
s
⁡
B
6
negnegs
⊢
B
∈
No
→
+
s
⁡
+
s
⁡
B
=
B
7
2
6
syl
⊢
φ
→
+
s
⁡
+
s
⁡
B
=
B
8
7
oveq2d
⊢
φ
→
+
s
⁡
A
+
s
+
s
⁡
+
s
⁡
B
=
+
s
⁡
A
+
s
B
9
1
negscld
⊢
φ
→
+
s
⁡
A
∈
No
10
9
2
addscomd
⊢
φ
→
+
s
⁡
A
+
s
B
=
B
+
s
+
s
⁡
A
11
5
8
10
3eqtrd
⊢
φ
→
+
s
⁡
A
+
s
+
s
⁡
B
=
B
+
s
+
s
⁡
A
12
1
2
subsvald
⊢
φ
→
A
-
s
B
=
A
+
s
+
s
⁡
B
13
12
fveq2d
⊢
φ
→
+
s
⁡
A
-
s
B
=
+
s
⁡
A
+
s
+
s
⁡
B
14
2
1
subsvald
⊢
φ
→
B
-
s
A
=
B
+
s
+
s
⁡
A
15
11
13
14
3eqtr4d
⊢
φ
→
+
s
⁡
A
-
s
B
=
B
-
s
A