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 9849

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 9846	. 2
2		vx	. . 3
3		vy	. . 3
4		cxr 8060	. . 3
5	2	cv 1363	. . . . . 6
6		cc0 7879	. . . . . 6
7	5, 6	wceq 1364	. . . . 5
8	3	cv 1363	. . . . . 6
9	8, 6	wceq 1364	. . . . 5
10	7, 9	wo 709	. . . 4 $\/$
11		clt 8061	. . . . . . . . 9
12	6, 8, 11	wbr 4033	. . . . . . . 8
13		cpnf 8058	. . . . . . . . 9
14	5, 13	wceq 1364	. . . . . . . 8
15	12, 14	wa 104	. . . . . . 7 $/\$
16	8, 6, 11	wbr 4033	. . . . . . . 8
17		cmnf 8059	. . . . . . . . 9
18	5, 17	wceq 1364	. . . . . . . 8
19	16, 18	wa 104	. . . . . . 7 $/\$
20	15, 19	wo 709	. . . . . 6 $/\$ $\/$ $/\$
21	6, 5, 11	wbr 4033	. . . . . . . 8
22	8, 13	wceq 1364	. . . . . . . 8
23	21, 22	wa 104	. . . . . . 7 $/\$
24	5, 6, 11	wbr 4033	. . . . . . . 8
25	8, 17	wceq 1364	. . . . . . . 8
26	24, 25	wa 104	. . . . . . 7 $/\$
27	23, 26	wo 709	. . . . . 6 $/\$ $\/$ $/\$
28	20, 27	wo 709	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
29	12, 18	wa 104	. . . . . . . 8 $/\$
30	16, 14	wa 104	. . . . . . . 8 $/\$
31	29, 30	wo 709	. . . . . . 7 $/\$ $\/$ $/\$
32	21, 25	wa 104	. . . . . . . 8 $/\$
33	24, 22	wa 104	. . . . . . . 8 $/\$
34	32, 33	wo 709	. . . . . . 7 $/\$ $\/$ $/\$
35	31, 34	wo 709	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
36		cmul 7884	. . . . . . 7
37	5, 8, 36	co 5922	. . . . . 6
38	35, 17, 37	cif 3561	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
39	28, 13, 38	cif 3561	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
40	10, 6, 39	cif 3561	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
41	2, 3, 4, 4, 40	cmpo 5924	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
42	1, 41	wceq 1364	1 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

This definition is referenced by: (None)

W3C validator