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

Definition df-xmul 12509
 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
StepHypRef Expression
1 cxmu 12506 . 2 class ·e
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10673 . . 3 class *
52cv 1537 . . . . . 6 class 𝑥
6 cc0 10536 . . . . . 6 class 0
75, 6wceq 1538 . . . . 5 wff 𝑥 = 0
83cv 1537 . . . . . 6 class 𝑦
98, 6wceq 1538 . . . . 5 wff 𝑦 = 0
107, 9wo 844 . . . 4 wff (𝑥 = 0 ∨ 𝑦 = 0)
11 clt 10674 . . . . . . . . 9 class <
126, 8, 11wbr 5053 . . . . . . . 8 wff 0 < 𝑦
13 cpnf 10671 . . . . . . . . 9 class +∞
145, 13wceq 1538 . . . . . . . 8 wff 𝑥 = +∞
1512, 14wa 399 . . . . . . 7 wff (0 < 𝑦𝑥 = +∞)
168, 6, 11wbr 5053 . . . . . . . 8 wff 𝑦 < 0
17 cmnf 10672 . . . . . . . . 9 class -∞
185, 17wceq 1538 . . . . . . . 8 wff 𝑥 = -∞
1916, 18wa 399 . . . . . . 7 wff (𝑦 < 0 ∧ 𝑥 = -∞)
2015, 19wo 844 . . . . . 6 wff ((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞))
216, 5, 11wbr 5053 . . . . . . . 8 wff 0 < 𝑥
228, 13wceq 1538 . . . . . . . 8 wff 𝑦 = +∞
2321, 22wa 399 . . . . . . 7 wff (0 < 𝑥𝑦 = +∞)
245, 6, 11wbr 5053 . . . . . . . 8 wff 𝑥 < 0
258, 17wceq 1538 . . . . . . . 8 wff 𝑦 = -∞
2624, 25wa 399 . . . . . . 7 wff (𝑥 < 0 ∧ 𝑦 = -∞)
2723, 26wo 844 . . . . . 6 wff ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))
2820, 27wo 844 . . . . 5 wff (((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞)))
2912, 18wa 399 . . . . . . . 8 wff (0 < 𝑦𝑥 = -∞)
3016, 14wa 399 . . . . . . . 8 wff (𝑦 < 0 ∧ 𝑥 = +∞)
3129, 30wo 844 . . . . . . 7 wff ((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞))
3221, 25wa 399 . . . . . . . 8 wff (0 < 𝑥𝑦 = -∞)
3324, 22wa 399 . . . . . . . 8 wff (𝑥 < 0 ∧ 𝑦 = +∞)
3432, 33wo 844 . . . . . . 7 wff ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))
3531, 34wo 844 . . . . . 6 wff (((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞)))
36 cmul 10541 . . . . . . 7 class ·
375, 8, 36co 7150 . . . . . 6 class (𝑥 · 𝑦)
3835, 17, 37cif 4451 . . . . 5 class if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))
3928, 13, 38cif 4451 . . . 4 class if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))
4010, 6, 39cif 4451 . . 3 class if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))
412, 3, 4, 4, 40cmpo 7152 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
421, 41wceq 1538 1 wff ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
 Colors of variables: wff setvar class This definition is referenced by:  xmulval  12618  xmulf  12665
 Copyright terms: Public domain W3C validator