Metamath Proof Explorer


Theorem subsubs4d

Description: Law for double surreal subtraction. (Contributed by Scott Fenton, 9-Mar-2025)

Ref Expression
Hypotheses subsubs4d.1 φ A No
subsubs4d.2 φ B No
subsubs4d.3 φ C No
Assertion subsubs4d φ A - s B - s C = A - s B + s C

Proof

Step Hyp Ref Expression
1 subsubs4d.1 φ A No
2 subsubs4d.2 φ B No
3 subsubs4d.3 φ C No
4 2 negscld φ + s B No
5 3 negscld φ + s C No
6 1 4 5 addsassd φ A + s + s B + s + s C = A + s + s B + s + s C
7 1 2 subsvald φ A - s B = A + s + s B
8 7 oveq1d φ A - s B - s C = A + s + s B - s C
9 1 4 addscld φ A + s + s B No
10 9 3 subsvald φ A + s + s B - s C = A + s + s B + s + s C
11 8 10 eqtrd φ A - s B - s C = A + s + s B + s + s C
12 2 3 addscld φ B + s C No
13 1 12 subsvald φ A - s B + s C = A + s + s B + s C
14 negsdi B No C No + s B + s C = + s B + s + s C
15 2 3 14 syl2anc φ + s B + s C = + s B + s + s C
16 15 oveq2d φ A + s + s B + s C = A + s + s B + s + s C
17 13 16 eqtrd φ A - s B + s C = A + s + s B + s + s C
18 6 11 17 3eqtr4d φ A - s B - s C = A - s B + s C