Description: Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | neg2sub | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 − - 𝐵 ) = ( 𝐵 − 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negcl | ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ ) | |
2 | subneg | ⊢ ( ( - 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 − - 𝐵 ) = ( - 𝐴 + 𝐵 ) ) | |
3 | 1 2 | sylan | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 − - 𝐵 ) = ( - 𝐴 + 𝐵 ) ) |
4 | negsubdi | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 − 𝐵 ) = ( - 𝐴 + 𝐵 ) ) | |
5 | negsubdi2 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) ) | |
6 | 3 4 5 | 3eqtr2d | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 − - 𝐵 ) = ( 𝐵 − 𝐴 ) ) |