ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-xmul GIF version

Definition df-xmul 8996
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 8993 . 2 class ·e
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 7284 . . 3 class *
52cv 1284 . . . . . 6 class 𝑥
6 cc0 7113 . . . . . 6 class 0
75, 6wceq 1285 . . . . 5 wff 𝑥 = 0
83cv 1284 . . . . . 6 class 𝑦
98, 6wceq 1285 . . . . 5 wff 𝑦 = 0
107, 9wo 662 . . . 4 wff (𝑥 = 0 ∨ 𝑦 = 0)
11 clt 7285 . . . . . . . . 9 class <
126, 8, 11wbr 3805 . . . . . . . 8 wff 0 < 𝑦
13 cpnf 7282 . . . . . . . . 9 class +∞
145, 13wceq 1285 . . . . . . . 8 wff 𝑥 = +∞
1512, 14wa 102 . . . . . . 7 wff (0 < 𝑦𝑥 = +∞)
168, 6, 11wbr 3805 . . . . . . . 8 wff 𝑦 < 0
17 cmnf 7283 . . . . . . . . 9 class -∞
185, 17wceq 1285 . . . . . . . 8 wff 𝑥 = -∞
1916, 18wa 102 . . . . . . 7 wff (𝑦 < 0 ∧ 𝑥 = -∞)
2015, 19wo 662 . . . . . 6 wff ((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞))
216, 5, 11wbr 3805 . . . . . . . 8 wff 0 < 𝑥
228, 13wceq 1285 . . . . . . . 8 wff 𝑦 = +∞
2321, 22wa 102 . . . . . . 7 wff (0 < 𝑥𝑦 = +∞)
245, 6, 11wbr 3805 . . . . . . . 8 wff 𝑥 < 0
258, 17wceq 1285 . . . . . . . 8 wff 𝑦 = -∞
2624, 25wa 102 . . . . . . 7 wff (𝑥 < 0 ∧ 𝑦 = -∞)
2723, 26wo 662 . . . . . 6 wff ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))
2820, 27wo 662 . . . . 5 wff (((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞)))
2912, 18wa 102 . . . . . . . 8 wff (0 < 𝑦𝑥 = -∞)
3016, 14wa 102 . . . . . . . 8 wff (𝑦 < 0 ∧ 𝑥 = +∞)
3129, 30wo 662 . . . . . . 7 wff ((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞))
3221, 25wa 102 . . . . . . . 8 wff (0 < 𝑥𝑦 = -∞)
3324, 22wa 102 . . . . . . . 8 wff (𝑥 < 0 ∧ 𝑦 = +∞)
3432, 33wo 662 . . . . . . 7 wff ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))
3531, 34wo 662 . . . . . 6 wff (((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞)))
36 cmul 7118 . . . . . . 7 class ·
375, 8, 36co 5564 . . . . . 6 class (𝑥 · 𝑦)
3835, 17, 37cif 3368 . . . . 5 class if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))
3928, 13, 38cif 3368 . . . 4 class if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))
4010, 6, 39cif 3368 . . 3 class if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))
412, 3, 4, 4, 40cmpt2 5566 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
421, 41wceq 1285 1 wff ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
Colors of variables: wff set class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator