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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 + 𝐵 ) = ( - 𝐴 + - 𝐵 ) )

Proof

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