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

Proof

Step Hyp Ref Expression
1 0cn 0 ∈ ℂ
2 subsub ( ( 0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 0 − ( 𝐴𝐵 ) ) = ( ( 0 − 𝐴 ) + 𝐵 ) )
3 1 2 mp3an1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 0 − ( 𝐴𝐵 ) ) = ( ( 0 − 𝐴 ) + 𝐵 ) )
4 df-neg - ( 𝐴𝐵 ) = ( 0 − ( 𝐴𝐵 ) )
5 df-neg - 𝐴 = ( 0 − 𝐴 )
6 5 oveq1i ( - 𝐴 + 𝐵 ) = ( ( 0 − 𝐴 ) + 𝐵 )
7 3 4 6 3eqtr4g ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴𝐵 ) = ( - 𝐴 + 𝐵 ) )