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

Definition df-xmul 11782
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 11779 . 2 class ·e
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 9929 . . 3 class *
52cv 1473 . . . . . 6 class 𝑥
6 cc0 9792 . . . . . 6 class 0
75, 6wceq 1474 . . . . 5 wff 𝑥 = 0
83cv 1473 . . . . . 6 class 𝑦
98, 6wceq 1474 . . . . 5 wff 𝑦 = 0
107, 9wo 381 . . . 4 wff (𝑥 = 0 ∨ 𝑦 = 0)
11 clt 9930 . . . . . . . . 9 class <
126, 8, 11wbr 4577 . . . . . . . 8 wff 0 < 𝑦
13 cpnf 9927 . . . . . . . . 9 class +∞
145, 13wceq 1474 . . . . . . . 8 wff 𝑥 = +∞
1512, 14wa 382 . . . . . . 7 wff (0 < 𝑦𝑥 = +∞)
168, 6, 11wbr 4577 . . . . . . . 8 wff 𝑦 < 0
17 cmnf 9928 . . . . . . . . 9 class -∞
185, 17wceq 1474 . . . . . . . 8 wff 𝑥 = -∞
1916, 18wa 382 . . . . . . 7 wff (𝑦 < 0 ∧ 𝑥 = -∞)
2015, 19wo 381 . . . . . 6 wff ((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞))
216, 5, 11wbr 4577 . . . . . . . 8 wff 0 < 𝑥
228, 13wceq 1474 . . . . . . . 8 wff 𝑦 = +∞
2321, 22wa 382 . . . . . . 7 wff (0 < 𝑥𝑦 = +∞)
245, 6, 11wbr 4577 . . . . . . . 8 wff 𝑥 < 0
258, 17wceq 1474 . . . . . . . 8 wff 𝑦 = -∞
2624, 25wa 382 . . . . . . 7 wff (𝑥 < 0 ∧ 𝑦 = -∞)
2723, 26wo 381 . . . . . 6 wff ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))
2820, 27wo 381 . . . . 5 wff (((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞)))
2912, 18wa 382 . . . . . . . 8 wff (0 < 𝑦𝑥 = -∞)
3016, 14wa 382 . . . . . . . 8 wff (𝑦 < 0 ∧ 𝑥 = +∞)
3129, 30wo 381 . . . . . . 7 wff ((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞))
3221, 25wa 382 . . . . . . . 8 wff (0 < 𝑥𝑦 = -∞)
3324, 22wa 382 . . . . . . . 8 wff (𝑥 < 0 ∧ 𝑦 = +∞)
3432, 33wo 381 . . . . . . 7 wff ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))
3531, 34wo 381 . . . . . 6 wff (((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞)))
36 cmul 9797 . . . . . . 7 class ·
375, 8, 36co 6526 . . . . . 6 class (𝑥 · 𝑦)
3835, 17, 37cif 4035 . . . . 5 class if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))
3928, 13, 38cif 4035 . . . 4 class if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))
4010, 6, 39cif 4035 . . 3 class if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))
412, 3, 4, 4, 40cmpt2 6528 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
421, 41wceq 1474 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  11891  xmulf  11933
  Copyright terms: Public domain W3C validator