muladd

Description: Product of two sums. (Contributed by NM, 14-Jan-2006) (Proof shortened by Andrew Salmon, 19-Nov-2011)

		Ref	Expression
	Assertion	muladd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) (C + D) = A C + D B + A D + C B$

Proof

Step	Hyp	Ref	Expression
1		addcl	$⊢ (A \in ℂ \land B \in ℂ) \to A + B \in ℂ$
2		adddi	$⊢ (A + B \in ℂ \land C \in ℂ \land D \in ℂ) \to (A + B) (C + D) = (A + B) C + (A + B) D$
3	2	3expb	$⊢ (A + B \in ℂ \land (C \in ℂ \land D \in ℂ)) \to (A + B) (C + D) = (A + B) C + (A + B) D$
4	1 3	sylan	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) (C + D) = (A + B) C + (A + B) D$
5		adddir	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to (A + B) C = A C + B C$
6	5	3expa	$⊢ ((A \in ℂ \land B \in ℂ) \land C \in ℂ) \to (A + B) C = A C + B C$
7	6	adantrr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) C = A C + B C$
8		adddir	$⊢ (A \in ℂ \land B \in ℂ \land D \in ℂ) \to (A + B) D = A D + B D$
9	8	3expa	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℂ) \to (A + B) D = A D + B D$
10	9	adantrl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) D = A D + B D$
11	7 10	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) C + (A + B) D = A C + B C + A D + B D$
12		mulcl	$⊢ (A \in ℂ \land C \in ℂ) \to A C \in ℂ$
13	12	ad2ant2r	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C \in ℂ$
14		mulcl	$⊢ (B \in ℂ \land C \in ℂ) \to B C \in ℂ$
15	14	ad2ant2lr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C \in ℂ$
16		mulcl	$⊢ (A \in ℂ \land D \in ℂ) \to A D \in ℂ$
17		mulcl	$⊢ (B \in ℂ \land D \in ℂ) \to B D \in ℂ$
18		addcl	$⊢ (A D \in ℂ \land B D \in ℂ) \to A D + B D \in ℂ$
19	16 17 18	syl2an	$⊢ ((A \in ℂ \land D \in ℂ) \land (B \in ℂ \land D \in ℂ)) \to A D + B D \in ℂ$
20	19	anandirs	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℂ) \to A D + B D \in ℂ$
21	20	adantrl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A D + B D \in ℂ$
22	13 15 21	add32d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C + B C + A D + B D = A C + (A D + B D) + B C$
23		mulcom	$⊢ (B \in ℂ \land D \in ℂ) \to B D = D B$
24	23	ad2ant2l	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B D = D B$
25	24	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C + A D + B D = A C + A D + D B$
26	16	ad2ant2rl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A D \in ℂ$
27	17	ad2ant2l	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B D \in ℂ$
28	13 26 27	addassd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C + A D + B D = A C + A D + B D$
29		mulcl	$⊢ (D \in ℂ \land B \in ℂ) \to D B \in ℂ$
30	29	ancoms	$⊢ (B \in ℂ \land D \in ℂ) \to D B \in ℂ$
31	30	ad2ant2l	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D B \in ℂ$
32	13 26 31	add32d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C + A D + D B = A C + D B + A D$
33	25 28 32	3eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C + A D + B D = A C + D B + A D$
34		mulcom	$⊢ (B \in ℂ \land C \in ℂ) \to B C = C B$
35	34	ad2ant2lr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C = C B$
36	33 35	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C + (A D + B D) + B C = (A C + D B) + A D + C B$
37		addcl	$⊢ (A C \in ℂ \land D B \in ℂ) \to A C + D B \in ℂ$
38	12 30 37	syl2an	$⊢ ((A \in ℂ \land C \in ℂ) \land (B \in ℂ \land D \in ℂ)) \to A C + D B \in ℂ$
39	38	an4s	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C + D B \in ℂ$
40		mulcl	$⊢ (C \in ℂ \land B \in ℂ) \to C B \in ℂ$
41	40	ancoms	$⊢ (B \in ℂ \land C \in ℂ) \to C B \in ℂ$
42	41	ad2ant2lr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C B \in ℂ$
43	39 26 42	addassd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A C + D B) + A D + C B = A C + D B + A D + C B$
44	22 36 43	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C + B C + A D + B D = A C + D B + A D + C B$
45	4 11 44	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) (C + D) = A C + D B + A D + C B$

Metamath Proof Explorer

Theorem muladd

Proof