df-xmul - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-xmul		Structured version Visualization version Unicode version

Definition df-xmul 11948

Description: Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)

**Assertion**
Ref	Expression
df-xmul	$\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-xmul**
Step	Hyp	Ref	Expression
1		cxmu 11945	. 2
2		vx	. . 3
3		vy	. . 3
4		cxr 10073	. . 3
5	2	cv 1482	. . . . . 6
6		cc0 9936	. . . . . 6
7	5, 6	wceq 1483	. . . . 5
8	3	cv 1482	. . . . . 6
9	8, 6	wceq 1483	. . . . 5
10	7, 9	wo 383	. . . 4 $\/$
11		clt 10074	. . . . . . . . 9
12	6, 8, 11	wbr 4653	. . . . . . . 8
13		cpnf 10071	. . . . . . . . 9
14	5, 13	wceq 1483	. . . . . . . 8
15	12, 14	wa 384	. . . . . . 7 $/\$
16	8, 6, 11	wbr 4653	. . . . . . . 8
17		cmnf 10072	. . . . . . . . 9
18	5, 17	wceq 1483	. . . . . . . 8
19	16, 18	wa 384	. . . . . . 7 $/\$
20	15, 19	wo 383	. . . . . 6 $/\$ $\/$ $/\$
21	6, 5, 11	wbr 4653	. . . . . . . 8
22	8, 13	wceq 1483	. . . . . . . 8
23	21, 22	wa 384	. . . . . . 7 $/\$
24	5, 6, 11	wbr 4653	. . . . . . . 8
25	8, 17	wceq 1483	. . . . . . . 8
26	24, 25	wa 384	. . . . . . 7 $/\$
27	23, 26	wo 383	. . . . . 6 $/\$ $\/$ $/\$
28	20, 27	wo 383	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
29	12, 18	wa 384	. . . . . . . 8 $/\$
30	16, 14	wa 384	. . . . . . . 8 $/\$
31	29, 30	wo 383	. . . . . . 7 $/\$ $\/$ $/\$
32	21, 25	wa 384	. . . . . . . 8 $/\$
33	24, 22	wa 384	. . . . . . . 8 $/\$
34	32, 33	wo 383	. . . . . . 7 $/\$ $\/$ $/\$
35	31, 34	wo 383	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
36		cmul 9941	. . . . . . 7
37	5, 8, 36	co 6650	. . . . . 6
38	35, 17, 37	cif 4086	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
39	28, 13, 38	cif 4086	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
40	10, 6, 39	cif 4086	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
41	2, 3, 4, 4, 40	cmpt2 6652	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
42	1, 41	wceq 1483	1 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: xmulval 12056 xmulf 12102

W3C validator