Description: Distribution of negative over addition. (Contributed by NM, 1-Jan-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | negdi2 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 + 𝐵 ) = ( - 𝐴 − 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negdi | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 + 𝐵 ) = ( - 𝐴 + - 𝐵 ) ) | |
2 | negcl | ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ ) | |
3 | negsub | ⊢ ( ( - 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 + - 𝐵 ) = ( - 𝐴 − 𝐵 ) ) | |
4 | 2 3 | sylan | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 + - 𝐵 ) = ( - 𝐴 − 𝐵 ) ) |
5 | 1 4 | eqtrd | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 + 𝐵 ) = ( - 𝐴 − 𝐵 ) ) |