Description: Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004) (Proof shortened by Mario Carneiro, 27-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | negsubdi | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 − 𝐵 ) = ( - 𝐴 + 𝐵 ) ) |
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 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 − 𝐵 ) = ( - 𝐴 + 𝐵 ) ) |