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