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

Metamath Proof Explorer

Theorem negsubdi

Description: Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion negsubdi ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = - A + B

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 subsub ⊢ 0 ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → 0 − A − B = 0 - A + B
3 1 2 mp3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ → 0 − A − B = 0 - A + B
4 df-neg ⊢ − A − B = 0 − A − B
5 df-neg ⊢ − A = 0 − A
6 5 oveq1i ⊢ - A + B = 0 - A + B
7 3 4 6 3eqtr4g ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = - A + B