This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem negsubdii

Description: Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999)

Ref Expression
Hypotheses negidi.1 ⊢ A ∈ ℂ
pncan3i.2 ⊢ B ∈ ℂ
Assertion negsubdii ⊢ − A − B = - A + B

Proof

Step Hyp Ref Expression
1 negidi.1 ⊢ A ∈ ℂ
2 pncan3i.2 ⊢ B ∈ ℂ
3 2 negcli ⊢ − B ∈ ℂ
4 1 3 negdii ⊢ − A + − B = - A + − − B
5 1 2 negsubi ⊢ A + − B = A − B
6 5 negeqi ⊢ − A + − B = − A − B
7 2 negnegi ⊢ − − B = B
8 7 oveq2i ⊢ - A + − − B = - A + B
9 4 6 8 3eqtr3i ⊢ − A − B = - A + B