Metamath Proof Explorer

Theorem mulsub

Description: Product of two differences. (Contributed by NM, 14-Jan-2006)

Ref Expression
Assertion mulsub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A − B ⁢ C − D = A ⁢ C + D ⁢ B - A ⁢ D + C ⁢ B

Proof

Step Hyp Ref Expression
1 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
2 negsub ⊢ C ∈ ℂ ∧ D ∈ ℂ → C + − D = C − D
3 1 2 oveqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + − B ⁢ C + − D = A − B ⁢ C − D
4 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
5 negcl ⊢ D ∈ ℂ → − D ∈ ℂ
6 muladd ⊢ A ∈ ℂ ∧ − B ∈ ℂ ∧ C ∈ ℂ ∧ − D ∈ ℂ → A + − B ⁢ C + − D = A ⁢ C + − D ⁢ − B + A ⁢ − D + C ⁢ − B
7 5 6 sylanr2 ⊢ A ∈ ℂ ∧ − B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + − B ⁢ C + − D = A ⁢ C + − D ⁢ − B + A ⁢ − D + C ⁢ − B
8 4 7 sylanl2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + − B ⁢ C + − D = A ⁢ C + − D ⁢ − B + A ⁢ − D + C ⁢ − B
9 mul2neg ⊢ D ∈ ℂ ∧ B ∈ ℂ → − D ⁢ − B = D ⁢ B
10 9 ancoms ⊢ B ∈ ℂ ∧ D ∈ ℂ → − D ⁢ − B = D ⁢ B
11 10 oveq2d ⊢ B ∈ ℂ ∧ D ∈ ℂ → A ⁢ C + − D ⁢ − B = A ⁢ C + D ⁢ B
12 11 ad2ant2l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ C + − D ⁢ − B = A ⁢ C + D ⁢ B
13 mulneg2 ⊢ A ∈ ℂ ∧ D ∈ ℂ → A ⁢ − D = − A ⁢ D
14 mulneg2 ⊢ C ∈ ℂ ∧ B ∈ ℂ → C ⁢ − B = − C ⁢ B
15 13 14 oveqan12d ⊢ A ∈ ℂ ∧ D ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A ⁢ − D + C ⁢ − B = - A ⁢ D + − C ⁢ B
16 mulcl ⊢ A ∈ ℂ ∧ D ∈ ℂ → A ⁢ D ∈ ℂ
17 mulcl ⊢ C ∈ ℂ ∧ B ∈ ℂ → C ⁢ B ∈ ℂ
18 negdi ⊢ A ⁢ D ∈ ℂ ∧ C ⁢ B ∈ ℂ → − A ⁢ D + C ⁢ B = - A ⁢ D + − C ⁢ B
19 16 17 18 syl2an ⊢ A ∈ ℂ ∧ D ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → − A ⁢ D + C ⁢ B = - A ⁢ D + − C ⁢ B
20 15 19 eqtr4d ⊢ A ∈ ℂ ∧ D ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A ⁢ − D + C ⁢ − B = − A ⁢ D + C ⁢ B
21 20 ancom2s ⊢ A ∈ ℂ ∧ D ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ − D + C ⁢ − B = − A ⁢ D + C ⁢ B
22 21 an42s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ − D + C ⁢ − B = − A ⁢ D + C ⁢ B
23 12 22 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ C + − D ⁢ − B + A ⁢ − D + C ⁢ − B = A ⁢ C + D ⁢ B + − A ⁢ D + C ⁢ B
24 mulcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C ∈ ℂ
25 mulcl ⊢ D ∈ ℂ ∧ B ∈ ℂ → D ⁢ B ∈ ℂ
26 25 ancoms ⊢ B ∈ ℂ ∧ D ∈ ℂ → D ⁢ B ∈ ℂ
27 addcl ⊢ A ⁢ C ∈ ℂ ∧ D ⁢ B ∈ ℂ → A ⁢ C + D ⁢ B ∈ ℂ
28 24 26 27 syl2an ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A ⁢ C + D ⁢ B ∈ ℂ
29 28 an4s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ C + D ⁢ B ∈ ℂ
30 17 ancoms ⊢ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ B ∈ ℂ
31 addcl ⊢ A ⁢ D ∈ ℂ ∧ C ⁢ B ∈ ℂ → A ⁢ D + C ⁢ B ∈ ℂ
32 16 30 31 syl2an ⊢ A ∈ ℂ ∧ D ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ D + C ⁢ B ∈ ℂ
33 32 an42s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ D + C ⁢ B ∈ ℂ
34 29 33 negsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ C + D ⁢ B + − A ⁢ D + C ⁢ B = A ⁢ C + D ⁢ B - A ⁢ D + C ⁢ B
35 8 23 34 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + − B ⁢ C + − D = A ⁢ C + D ⁢ B - A ⁢ D + C ⁢ B
36 3 35 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A − B ⁢ C − D = A ⁢ C + D ⁢ B - A ⁢ D + C ⁢ B