Metamath Proof Explorer


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