Detailed syntax breakdown of Definition df-xadd
Step | Hyp | Ref
| Expression |
1 | | cxad 12845 |
. 2
class
+𝑒 |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cxr 11009 |
. . 3
class
ℝ* |
5 | 2 | cv 1541 |
. . . . 5
class 𝑥 |
6 | | cpnf 11007 |
. . . . 5
class
+∞ |
7 | 5, 6 | wceq 1542 |
. . . 4
wff 𝑥 = +∞ |
8 | 3 | cv 1541 |
. . . . . 6
class 𝑦 |
9 | | cmnf 11008 |
. . . . . 6
class
-∞ |
10 | 8, 9 | wceq 1542 |
. . . . 5
wff 𝑦 = -∞ |
11 | | cc0 10872 |
. . . . 5
class
0 |
12 | 10, 11, 6 | cif 4465 |
. . . 4
class if(𝑦 = -∞, 0,
+∞) |
13 | 5, 9 | wceq 1542 |
. . . . 5
wff 𝑥 = -∞ |
14 | 8, 6 | wceq 1542 |
. . . . . 6
wff 𝑦 = +∞ |
15 | 14, 11, 9 | cif 4465 |
. . . . 5
class if(𝑦 = +∞, 0,
-∞) |
16 | | caddc 10875 |
. . . . . . . 8
class
+ |
17 | 5, 8, 16 | co 7271 |
. . . . . . 7
class (𝑥 + 𝑦) |
18 | 10, 9, 17 | cif 4465 |
. . . . . 6
class if(𝑦 = -∞, -∞, (𝑥 + 𝑦)) |
19 | 14, 6, 18 | cif 4465 |
. . . . 5
class if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))) |
20 | 13, 15, 19 | cif 4465 |
. . . 4
class if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞),
if(𝑦 = +∞, +∞,
if(𝑦 = -∞, -∞,
(𝑥 + 𝑦)))) |
21 | 7, 12, 20 | cif 4465 |
. . 3
class if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞),
if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞),
if(𝑦 = +∞, +∞,
if(𝑦 = -∞, -∞,
(𝑥 + 𝑦))))) |
22 | 2, 3, 4, 4, 21 | cmpo 7273 |
. 2
class (𝑥 ∈ ℝ*,
𝑦 ∈
ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞),
if(𝑦 = +∞, +∞,
if(𝑦 = -∞, -∞,
(𝑥 + 𝑦)))))) |
23 | 1, 22 | wceq 1542 |
1
wff
+𝑒 = (𝑥
∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞),
if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞),
if(𝑦 = +∞, +∞,
if(𝑦 = -∞, -∞,
(𝑥 + 𝑦)))))) |