Metamath Proof Explorer

Theorem negdi

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

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

Proof

Step Hyp Ref Expression
1 subneg ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − − B = A + B
2 1 negeqd ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − − B = − A + B
3 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
4 negsubdi ⊢ A ∈ ℂ ∧ − B ∈ ℂ → − A − − B = - A + − B
5 3 4 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − − B = - A + − B
6 2 5 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A + B = - A + − B