Definition df-xmul 11349

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 11346	. 2
2		vx	. . 3
3		vy	. . 3
4		cxr 9648	. . 3
5	2	cv 1394	. . . . . 6
6		cc0 9513	. . . . . 6
7	5, 6	wceq 1395	. . . . 5
8	3	cv 1394	. . . . . 6
9	8, 6	wceq 1395	. . . . 5
10	7, 9	wo 368	. . . 4
11		clt 9649	. . . . . . . . 9
12	6, 8, 11	wbr 4452	. . . . . . . 8
13		cpnf 9646	. . . . . . . . 9
14	5, 13	wceq 1395	. . . . . . . 8
15	12, 14	wa 369	. . . . . . 7
16	8, 6, 11	wbr 4452	. . . . . . . 8
17		cmnf 9647	. . . . . . . . 9
18	5, 17	wceq 1395	. . . . . . . 8
19	16, 18	wa 369	. . . . . . 7
20	15, 19	wo 368	. . . . . 6
21	6, 5, 11	wbr 4452	. . . . . . . 8
22	8, 13	wceq 1395	. . . . . . . 8
23	21, 22	wa 369	. . . . . . 7
24	5, 6, 11	wbr 4452	. . . . . . . 8
25	8, 17	wceq 1395	. . . . . . . 8
26	24, 25	wa 369	. . . . . . 7
27	23, 26	wo 368	. . . . . 6
28	20, 27	wo 368	. . . . 5
29	12, 18	wa 369	. . . . . . . 8
30	16, 14	wa 369	. . . . . . . 8
31	29, 30	wo 368	. . . . . . 7
32	21, 25	wa 369	. . . . . . . 8
33	24, 22	wa 369	. . . . . . . 8
34	32, 33	wo 368	. . . . . . 7
35	31, 34	wo 368	. . . . . 6
36		cmul 9518	. . . . . . 7
37	5, 8, 36	co 6296	. . . . . 6
38	35, 17, 37	cif 3941	. . . . 5
39	28, 13, 38	cif 3941	. . . 4
40	10, 6, 39	cif 3941	. . 3
41	2, 3, 4, 4, 40	cmpt2 6298	. 2
42	1, 41	wceq 1395	1

This definition is referenced by:  xmulval  11453  xmulf  11493