df-xmul - Intuitionistic Logic Explorer

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

Definition df-xmul 9731

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 9728	. 2
2		vx	. . 3
3		vy	. . 3
4		cxr 7953	. . 3
5	2	cv 1347	. . . . . 6
6		cc0 7774	. . . . . 6
7	5, 6	wceq 1348	. . . . 5
8	3	cv 1347	. . . . . 6
9	8, 6	wceq 1348	. . . . 5
10	7, 9	wo 703	. . . 4 $\/$
11		clt 7954	. . . . . . . . 9
12	6, 8, 11	wbr 3989	. . . . . . . 8
13		cpnf 7951	. . . . . . . . 9
14	5, 13	wceq 1348	. . . . . . . 8
15	12, 14	wa 103	. . . . . . 7 $/\$
16	8, 6, 11	wbr 3989	. . . . . . . 8
17		cmnf 7952	. . . . . . . . 9
18	5, 17	wceq 1348	. . . . . . . 8
19	16, 18	wa 103	. . . . . . 7 $/\$
20	15, 19	wo 703	. . . . . 6 $/\$ $\/$ $/\$
21	6, 5, 11	wbr 3989	. . . . . . . 8
22	8, 13	wceq 1348	. . . . . . . 8
23	21, 22	wa 103	. . . . . . 7 $/\$
24	5, 6, 11	wbr 3989	. . . . . . . 8
25	8, 17	wceq 1348	. . . . . . . 8
26	24, 25	wa 103	. . . . . . 7 $/\$
27	23, 26	wo 703	. . . . . 6 $/\$ $\/$ $/\$
28	20, 27	wo 703	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
29	12, 18	wa 103	. . . . . . . 8 $/\$
30	16, 14	wa 103	. . . . . . . 8 $/\$
31	29, 30	wo 703	. . . . . . 7 $/\$ $\/$ $/\$
32	21, 25	wa 103	. . . . . . . 8 $/\$
33	24, 22	wa 103	. . . . . . . 8 $/\$
34	32, 33	wo 703	. . . . . . 7 $/\$ $\/$ $/\$
35	31, 34	wo 703	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
36		cmul 7779	. . . . . . 7
37	5, 8, 36	co 5853	. . . . . 6
38	35, 17, 37	cif 3526	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
39	28, 13, 38	cif 3526	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
40	10, 6, 39	cif 3526	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
41	2, 3, 4, 4, 40	cmpo 5855	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
42	1, 41	wceq 1348	1 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

This definition is referenced by: (None)

W3C validator