Theorem muladd 8705

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

Assertion

Ref	Expression
muladd	⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))))

Proof of Theorem muladd

Step	Hyp	Ref	Expression
1		addcl 8298	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
2		adddi 8305	. . . 4 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 + 𝐵) · 𝐶) + ((𝐴 + 𝐵) · 𝐷)))
3	2	3expb 1235	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 + 𝐵) · 𝐶) + ((𝐴 + 𝐵) · 𝐷)))
4	1, 3	sylan 283	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 + 𝐵) · 𝐶) + ((𝐴 + 𝐵) · 𝐷)))
5		adddir 8311	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
6	5	3expa 1234	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
7	6	adantrr 483	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
8		adddir 8311	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐷) = ((𝐴 · 𝐷) + (𝐵 · 𝐷)))
9	8	3expa 1234	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐷 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐷) = ((𝐴 · 𝐷) + (𝐵 · 𝐷)))
10	9	adantrl 482	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · 𝐷) = ((𝐴 · 𝐷) + (𝐵 · 𝐷)))
11	7, 10	oveq12d 6097	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) · 𝐶) + ((𝐴 + 𝐵) · 𝐷)) = (((𝐴 · 𝐶) + (𝐵 · 𝐶)) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))))
12		mulcl 8300	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · 𝐶) ∈ ℂ)
13	12	ad2ant2r 513	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐴 · 𝐶) ∈ ℂ)
14		mulcl 8300	. . . . 5 ⊢ ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 · 𝐶) ∈ ℂ)
15	14	ad2ant2lr 514	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐵 · 𝐶) ∈ ℂ)
16		mulcl 8300	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐴 · 𝐷) ∈ ℂ)
17		mulcl 8300	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐵 · 𝐷) ∈ ℂ)
18		addcl 8298	. . . . . . 7 ⊢ (((𝐴 · 𝐷) ∈ ℂ ∧ (𝐵 · 𝐷) ∈ ℂ) → ((𝐴 · 𝐷) + (𝐵 · 𝐷)) ∈ ℂ)
19	16, 17, 18	syl2an 289	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ (𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐷) + (𝐵 · 𝐷)) ∈ ℂ)
20	19	anandirs 601	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐷 ∈ ℂ) → ((𝐴 · 𝐷) + (𝐵 · 𝐷)) ∈ ℂ)
21	20	adantrl 482	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐷) + (𝐵 · 𝐷)) ∈ ℂ)
22	13, 15, 21	add32d 8488	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 · 𝐶) + (𝐵 · 𝐶)) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))) = (((𝐴 · 𝐶) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))) + (𝐵 · 𝐶)))
23		mulcom 8302	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐵 · 𝐷) = (𝐷 · 𝐵))
24	23	ad2ant2l 512	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐵 · 𝐷) = (𝐷 · 𝐵))
25	24	oveq2d 6095	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 · 𝐶) + (𝐴 · 𝐷)) + (𝐵 · 𝐷)) = (((𝐴 · 𝐶) + (𝐴 · 𝐷)) + (𝐷 · 𝐵)))
26	16	ad2ant2rl 515	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐴 · 𝐷) ∈ ℂ)
27	17	ad2ant2l 512	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐵 · 𝐷) ∈ ℂ)
28	13, 26, 27	addassd 8342	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 · 𝐶) + (𝐴 · 𝐷)) + (𝐵 · 𝐷)) = ((𝐴 · 𝐶) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))))
29		mulcl 8300	. . . . . . . 8 ⊢ ((𝐷 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐷 · 𝐵) ∈ ℂ)
30	29	ancoms 268	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐷 · 𝐵) ∈ ℂ)
31	30	ad2ant2l 512	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐷 · 𝐵) ∈ ℂ)
32	13, 26, 31	add32d 8488	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 · 𝐶) + (𝐴 · 𝐷)) + (𝐷 · 𝐵)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + (𝐴 · 𝐷)))
33	25, 28, 32	3eqtr3d 2279	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐶) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + (𝐴 · 𝐷)))
34		mulcom 8302	. . . . 5 ⊢ ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
35	34	ad2ant2lr 514	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
36	33, 35	oveq12d 6097	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 · 𝐶) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))) + (𝐵 · 𝐶)) = ((((𝐴 · 𝐶) + (𝐷 · 𝐵)) + (𝐴 · 𝐷)) + (𝐶 · 𝐵)))
37		addcl 8298	. . . . . 6 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐷 · 𝐵) ∈ ℂ) → ((𝐴 · 𝐶) + (𝐷 · 𝐵)) ∈ ℂ)
38	12, 30, 37	syl2an 289	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐶) + (𝐷 · 𝐵)) ∈ ℂ)
39	38	an4s 596	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐶) + (𝐷 · 𝐵)) ∈ ℂ)
40		mulcl 8300	. . . . . 6 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 · 𝐵) ∈ ℂ)
41	40	ancoms 268	. . . . 5 ⊢ ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐶 · 𝐵) ∈ ℂ)
42	41	ad2ant2lr 514	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐶 · 𝐵) ∈ ℂ)
43	39, 26, 42	addassd 8342	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((((𝐴 · 𝐶) + (𝐷 · 𝐵)) + (𝐴 · 𝐷)) + (𝐶 · 𝐵)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
44	22, 36, 43	3eqtrd 2275	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 · 𝐶) + (𝐵 · 𝐶)) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
45	4, 11, 44	3eqtrd 2275	1 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   + caddc 8176   · cmul 8178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-addcl 8269  ax-mulcl 8271  ax-addcom 8273  ax-mulcom 8274  ax-addass 8275  ax-distr 8277

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6082

This theorem is referenced by:  mulsub  8722  muladdi  8730  muladdd  8737  sqabsadd  11804  demoivreALT  12524