Metamath Proof Explorer

Theorem mulsub2

Description: Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion mulsub2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A − B ⁢ C − D = B − A ⁢ D − C

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
2 subcl ⊢ C ∈ ℂ ∧ D ∈ ℂ → C − D ∈ ℂ
3 mul2neg ⊢ A − B ∈ ℂ ∧ C − D ∈ ℂ → − A − B ⁢ − C − D = A − B ⁢ C − D
4 1 2 3 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → − A − B ⁢ − C − D = A − B ⁢ C − D
5 negsubdi2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = B − A
6 negsubdi2 ⊢ C ∈ ℂ ∧ D ∈ ℂ → − C − D = D − C
7 5 6 oveqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → − A − B ⁢ − C − D = B − A ⁢ D − C
8 4 7 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A − B ⁢ C − D = B − A ⁢ D − C