Detailed syntax breakdown of Definition df-xmul
Step | Hyp | Ref
| Expression |
1 | | cxmu 12844 |
. 2
class
·e |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cxr 11007 |
. . 3
class
ℝ* |
5 | 2 | cv 1541 |
. . . . . 6
class 𝑥 |
6 | | cc0 10870 |
. . . . . 6
class
0 |
7 | 5, 6 | wceq 1542 |
. . . . 5
wff 𝑥 = 0 |
8 | 3 | cv 1541 |
. . . . . 6
class 𝑦 |
9 | 8, 6 | wceq 1542 |
. . . . 5
wff 𝑦 = 0 |
10 | 7, 9 | wo 844 |
. . . 4
wff (𝑥 = 0 ∨ 𝑦 = 0) |
11 | | clt 11008 |
. . . . . . . . 9
class
< |
12 | 6, 8, 11 | wbr 5079 |
. . . . . . . 8
wff 0 <
𝑦 |
13 | | cpnf 11005 |
. . . . . . . . 9
class
+∞ |
14 | 5, 13 | wceq 1542 |
. . . . . . . 8
wff 𝑥 = +∞ |
15 | 12, 14 | wa 396 |
. . . . . . 7
wff (0 <
𝑦 ∧ 𝑥 = +∞) |
16 | 8, 6, 11 | wbr 5079 |
. . . . . . . 8
wff 𝑦 < 0 |
17 | | cmnf 11006 |
. . . . . . . . 9
class
-∞ |
18 | 5, 17 | wceq 1542 |
. . . . . . . 8
wff 𝑥 = -∞ |
19 | 16, 18 | wa 396 |
. . . . . . 7
wff (𝑦 < 0 ∧ 𝑥 = -∞) |
20 | 15, 19 | wo 844 |
. . . . . 6
wff ((0 <
𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) |
21 | 6, 5, 11 | wbr 5079 |
. . . . . . . 8
wff 0 <
𝑥 |
22 | 8, 13 | wceq 1542 |
. . . . . . . 8
wff 𝑦 = +∞ |
23 | 21, 22 | wa 396 |
. . . . . . 7
wff (0 <
𝑥 ∧ 𝑦 = +∞) |
24 | 5, 6, 11 | wbr 5079 |
. . . . . . . 8
wff 𝑥 < 0 |
25 | 8, 17 | wceq 1542 |
. . . . . . . 8
wff 𝑦 = -∞ |
26 | 24, 25 | wa 396 |
. . . . . . 7
wff (𝑥 < 0 ∧ 𝑦 = -∞) |
27 | 23, 26 | wo 844 |
. . . . . 6
wff ((0 <
𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞)) |
28 | 20, 27 | wo 844 |
. . . . 5
wff (((0 <
𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))) |
29 | 12, 18 | wa 396 |
. . . . . . . 8
wff (0 <
𝑦 ∧ 𝑥 = -∞) |
30 | 16, 14 | wa 396 |
. . . . . . . 8
wff (𝑦 < 0 ∧ 𝑥 = +∞) |
31 | 29, 30 | wo 844 |
. . . . . . 7
wff ((0 <
𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) |
32 | 21, 25 | wa 396 |
. . . . . . . 8
wff (0 <
𝑥 ∧ 𝑦 = -∞) |
33 | 24, 22 | wa 396 |
. . . . . . . 8
wff (𝑥 < 0 ∧ 𝑦 = +∞) |
34 | 32, 33 | wo 844 |
. . . . . . 7
wff ((0 <
𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞)) |
35 | 31, 34 | wo 844 |
. . . . . 6
wff (((0 <
𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))) |
36 | | cmul 10875 |
. . . . . . 7
class
· |
37 | 5, 8, 36 | co 7269 |
. . . . . 6
class (𝑥 · 𝑦) |
38 | 35, 17, 37 | cif 4465 |
. . . . 5
class if((((0
< 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)) |
39 | 28, 13, 38 | cif 4465 |
. . . 4
class if((((0
< 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))) |
40 | 10, 6, 39 | cif 4465 |
. . 3
class if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))) |
41 | 2, 3, 4, 4, 40 | cmpo 7271 |
. 2
class (𝑥 ∈ ℝ*,
𝑦 ∈
ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))) |
42 | 1, 41 | wceq 1542 |
1
wff
·e = (𝑥
∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))) |