Definition df-xmul 12779

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

Assertion

Ref	Expression
df-xmul	⊢ ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-xmul

Step	Hyp	Ref	Expression
1		cxmu 12776	. 2 class ·e
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10939	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		cc0 10802	. . . . . 6 class 0
7	5, 6	wceq 1539	. . . . 5 wff 𝑥 = 0
8	3	cv 1538	. . . . . 6 class 𝑦
9	8, 6	wceq 1539	. . . . 5 wff 𝑦 = 0
10	7, 9	wo 843	. . . 4 wff (𝑥 = 0 ∨ 𝑦 = 0)
11		clt 10940	. . . . . . . . 9 class <
12	6, 8, 11	wbr 5070	. . . . . . . 8 wff 0 < 𝑦
13		cpnf 10937	. . . . . . . . 9 class +∞
14	5, 13	wceq 1539	. . . . . . . 8 wff 𝑥 = +∞
15	12, 14	wa 395	. . . . . . 7 wff (0 < 𝑦 ∧ 𝑥 = +∞)
16	8, 6, 11	wbr 5070	. . . . . . . 8 wff 𝑦 < 0
17		cmnf 10938	. . . . . . . . 9 class -∞
18	5, 17	wceq 1539	. . . . . . . 8 wff 𝑥 = -∞
19	16, 18	wa 395	. . . . . . 7 wff (𝑦 < 0 ∧ 𝑥 = -∞)
20	15, 19	wo 843	. . . . . 6 wff ((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞))
21	6, 5, 11	wbr 5070	. . . . . . . 8 wff 0 < 𝑥
22	8, 13	wceq 1539	. . . . . . . 8 wff 𝑦 = +∞
23	21, 22	wa 395	. . . . . . 7 wff (0 < 𝑥 ∧ 𝑦 = +∞)
24	5, 6, 11	wbr 5070	. . . . . . . 8 wff 𝑥 < 0
25	8, 17	wceq 1539	. . . . . . . 8 wff 𝑦 = -∞
26	24, 25	wa 395	. . . . . . 7 wff (𝑥 < 0 ∧ 𝑦 = -∞)
27	23, 26	wo 843	. . . . . 6 wff ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))
28	20, 27	wo 843	. . . . 5 wff (((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞)))
29	12, 18	wa 395	. . . . . . . 8 wff (0 < 𝑦 ∧ 𝑥 = -∞)
30	16, 14	wa 395	. . . . . . . 8 wff (𝑦 < 0 ∧ 𝑥 = +∞)
31	29, 30	wo 843	. . . . . . 7 wff ((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞))
32	21, 25	wa 395	. . . . . . . 8 wff (0 < 𝑥 ∧ 𝑦 = -∞)
33	24, 22	wa 395	. . . . . . . 8 wff (𝑥 < 0 ∧ 𝑦 = +∞)
34	32, 33	wo 843	. . . . . . 7 wff ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))
35	31, 34	wo 843	. . . . . 6 wff (((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞)))
36		cmul 10807	. . . . . . 7 class ·
37	5, 8, 36	co 7255	. . . . . 6 class (𝑥 · 𝑦)
38	35, 17, 37	cif 4456	. . . . 5 class if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))
39	28, 13, 38	cif 4456	. . . 4 class if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))
40	10, 6, 39	cif 4456	. . 3 class if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))
41	2, 3, 4, 4, 40	cmpo 7257	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
42	1, 41	wceq 1539	1 wff ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))

This definition is referenced by:  xmulval  12888  xmulf  12935