Database
SURREAL NUMBERS
Surreal arithmetic
Addition
adds4d
Next ⟩
adds42d
Metamath Proof Explorer
Ascii
Unicode
Theorem
adds4d
Description:
Rearrangement of four terms in a surreal sum.
(Contributed by
Scott Fenton
, 5-Feb-2025)
Ref
Expression
Hypotheses
adds4d.1
⊢
φ
→
A
∈
No
adds4d.2
⊢
φ
→
B
∈
No
adds4d.3
⊢
φ
→
C
∈
No
adds4d.4
⊢
φ
→
D
∈
No
Assertion
adds4d
⊢
φ
→
A
+
s
B
+
s
C
+
s
D
=
A
+
s
C
+
s
B
+
s
D
Proof
Step
Hyp
Ref
Expression
1
adds4d.1
⊢
φ
→
A
∈
No
2
adds4d.2
⊢
φ
→
B
∈
No
3
adds4d.3
⊢
φ
→
C
∈
No
4
adds4d.4
⊢
φ
→
D
∈
No
5
1
2
3
adds32d
⊢
φ
→
A
+
s
B
+
s
C
=
A
+
s
C
+
s
B
6
5
oveq1d
⊢
φ
→
A
+
s
B
+
s
C
+
s
D
=
A
+
s
C
+
s
B
+
s
D
7
1
2
addscld
⊢
φ
→
A
+
s
B
∈
No
8
7
3
4
addsassd
⊢
φ
→
A
+
s
B
+
s
C
+
s
D
=
A
+
s
B
+
s
C
+
s
D
9
1
3
addscld
⊢
φ
→
A
+
s
C
∈
No
10
9
2
4
addsassd
⊢
φ
→
A
+
s
C
+
s
B
+
s
D
=
A
+
s
C
+
s
B
+
s
D
11
6
8
10
3eqtr3d
⊢
φ
→
A
+
s
B
+
s
C
+
s
D
=
A
+
s
C
+
s
B
+
s
D