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