Metamath Proof Explorer


Theorem hvnegdi

Description: Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

Ref Expression
Assertion hvnegdi A B -1 A - B = B - A

Proof

Step Hyp Ref Expression
1 oveq1 A = if A A 0 A - B = if A A 0 - B
2 1 oveq2d A = if A A 0 -1 A - B = -1 if A A 0 - B
3 oveq2 A = if A A 0 B - A = B - if A A 0
4 2 3 eqeq12d A = if A A 0 -1 A - B = B - A -1 if A A 0 - B = B - if A A 0
5 oveq2 B = if B B 0 if A A 0 - B = if A A 0 - if B B 0
6 5 oveq2d B = if B B 0 -1 if A A 0 - B = -1 if A A 0 - if B B 0
7 oveq1 B = if B B 0 B - if A A 0 = if B B 0 - if A A 0
8 6 7 eqeq12d B = if B B 0 -1 if A A 0 - B = B - if A A 0 -1 if A A 0 - if B B 0 = if B B 0 - if A A 0
9 ifhvhv0 if A A 0
10 ifhvhv0 if B B 0
11 9 10 hvnegdii -1 if A A 0 - if B B 0 = if B B 0 - if A A 0
12 4 8 11 dedth2h A B -1 A - B = B - A