muladd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > muladd		Unicode version

Theorem muladd 8146

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 7745	. . 3 $/\$
2		adddi 7752	. . . 4 $/\$ $/\$
3	2	3expb 1182	. . 3 $/\$ $/\$
4	1, 3	sylan 281	. 2 $/\$ $/\$ $/\$
5		adddir 7757	. . . . 5 $/\$ $/\$
6	5	3expa 1181	. . . 4 $/\$ $/\$
7	6	adantrr 470	. . 3 $/\$ $/\$ $/\$
8		adddir 7757	. . . . 5 $/\$ $/\$
9	8	3expa 1181	. . . 4 $/\$ $/\$
10	9	adantrl 469	. . 3 $/\$ $/\$ $/\$
11	7, 10	oveq12d 5792	. 2 $/\$ $/\$ $/\$
12		mulcl 7747	. . . . 5 $/\$
13	12	ad2ant2r 500	. . . 4 $/\$ $/\$ $/\$
14		mulcl 7747	. . . . 5 $/\$
15	14	ad2ant2lr 501	. . . 4 $/\$ $/\$ $/\$
16		mulcl 7747	. . . . . . 7 $/\$
17		mulcl 7747	. . . . . . 7 $/\$
18		addcl 7745	. . . . . . 7 $/\$
19	16, 17, 18	syl2an 287	. . . . . 6 $/\$ $/\$ $/\$
20	19	anandirs 582	. . . . 5 $/\$ $/\$
21	20	adantrl 469	. . . 4 $/\$ $/\$ $/\$
22	13, 15, 21	add32d 7930	. . 3 $/\$ $/\$ $/\$
23		mulcom 7749	. . . . . . 7 $/\$
24	23	ad2ant2l 499	. . . . . 6 $/\$ $/\$ $/\$
25	24	oveq2d 5790	. . . . 5 $/\$ $/\$ $/\$
26	16	ad2ant2rl 502	. . . . . 6 $/\$ $/\$ $/\$
27	17	ad2ant2l 499	. . . . . 6 $/\$ $/\$ $/\$
28	13, 26, 27	addassd 7788	. . . . 5 $/\$ $/\$ $/\$
29		mulcl 7747	. . . . . . . 8 $/\$
30	29	ancoms 266	. . . . . . 7 $/\$
31	30	ad2ant2l 499	. . . . . 6 $/\$ $/\$ $/\$
32	13, 26, 31	add32d 7930	. . . . 5 $/\$ $/\$ $/\$
33	25, 28, 32	3eqtr3d 2180	. . . 4 $/\$ $/\$ $/\$
34		mulcom 7749	. . . . 5 $/\$
35	34	ad2ant2lr 501	. . . 4 $/\$ $/\$ $/\$
36	33, 35	oveq12d 5792	. . 3 $/\$ $/\$ $/\$
37		addcl 7745	. . . . . 6 $/\$
38	12, 30, 37	syl2an 287	. . . . 5 $/\$ $/\$ $/\$
39	38	an4s 577	. . . 4 $/\$ $/\$ $/\$
40		mulcl 7747	. . . . . 6 $/\$
41	40	ancoms 266	. . . . 5 $/\$
42	41	ad2ant2lr 501	. . . 4 $/\$ $/\$ $/\$
43	39, 26, 42	addassd 7788	. . 3 $/\$ $/\$ $/\$
44	22, 36, 43	3eqtrd 2176	. 2 $/\$ $/\$ $/\$
45	4, 11, 44	3eqtrd 2176	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wceq 1331

wcel 1480 (class class class)co 5774

cc 7618

caddc 7623

cmul 7625

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-addcl 7716 ax-mulcl 7718 ax-addcom 7720 ax-mulcom 7721 ax-addass 7722 ax-distr 7724

This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 df-v 2688 df-un 3075 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-br 3930 df-iota 5088 df-fv 5131 df-ov 5777

This theorem is referenced by: mulsub 8163 muladdi 8171 muladdd 8178 sqabsadd 10827 demoivreALT 11480

W3C validator