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 11986
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 11983 . 2 class ·e
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10111 . . 3 class *
52cv 1522 . . . . . 6 class 𝑥
6 cc0 9974 . . . . . 6 class 0
75, 6wceq 1523 . . . . 5 wff 𝑥 = 0
83cv 1522 . . . . . 6 class 𝑦
98, 6wceq 1523 . . . . 5 wff 𝑦 = 0
107, 9wo 382 . . . 4 wff (𝑥 = 0 ∨ 𝑦 = 0)
11 clt 10112 . . . . . . . . 9 class <
126, 8, 11wbr 4685 . . . . . . . 8 wff 0 < 𝑦
13 cpnf 10109 . . . . . . . . 9 class +∞
145, 13wceq 1523 . . . . . . . 8 wff 𝑥 = +∞
1512, 14wa 383 . . . . . . 7 wff (0 < 𝑦𝑥 = +∞)
168, 6, 11wbr 4685 . . . . . . . 8 wff 𝑦 < 0
17 cmnf 10110 . . . . . . . . 9 class -∞
185, 17wceq 1523 . . . . . . . 8 wff 𝑥 = -∞
1916, 18wa 383 . . . . . . 7 wff (𝑦 < 0 ∧ 𝑥 = -∞)
2015, 19wo 382 . . . . . 6 wff ((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞))
216, 5, 11wbr 4685 . . . . . . . 8 wff 0 < 𝑥
228, 13wceq 1523 . . . . . . . 8 wff 𝑦 = +∞
2321, 22wa 383 . . . . . . 7 wff (0 < 𝑥𝑦 = +∞)
245, 6, 11wbr 4685 . . . . . . . 8 wff 𝑥 < 0
258, 17wceq 1523 . . . . . . . 8 wff 𝑦 = -∞
2624, 25wa 383 . . . . . . 7 wff (𝑥 < 0 ∧ 𝑦 = -∞)
2723, 26wo 382 . . . . . 6 wff ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))
2820, 27wo 382 . . . . 5 wff (((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞)))
2912, 18wa 383 . . . . . . . 8 wff (0 < 𝑦𝑥 = -∞)
3016, 14wa 383 . . . . . . . 8 wff (𝑦 < 0 ∧ 𝑥 = +∞)
3129, 30wo 382 . . . . . . 7 wff ((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞))
3221, 25wa 383 . . . . . . . 8 wff (0 < 𝑥𝑦 = -∞)
3324, 22wa 383 . . . . . . . 8 wff (𝑥 < 0 ∧ 𝑦 = +∞)
3432, 33wo 382 . . . . . . 7 wff ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))
3531, 34wo 382 . . . . . 6 wff (((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞)))
36 cmul 9979 . . . . . . 7 class ·
375, 8, 36co 6690 . . . . . 6 class (𝑥 · 𝑦)
3835, 17, 37cif 4119 . . . . 5 class if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))
3928, 13, 38cif 4119 . . . 4 class if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))
4010, 6, 39cif 4119 . . 3 class if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))
412, 3, 4, 4, 40cmpt2 6692 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
421, 41wceq 1523 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  12094  xmulf  12140
  Copyright terms: Public domain W3C validator