Detailed syntax breakdown of Definition df-exp
Step | Hyp | Ref
| Expression |
1 | | cexp 12722 |
. 2
class
↑ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cc 9813 |
. . 3
class
ℂ |
5 | | cz 11254 |
. . 3
class
ℤ |
6 | 3 | cv 1474 |
. . . . 5
class 𝑦 |
7 | | cc0 9815 |
. . . . 5
class
0 |
8 | 6, 7 | wceq 1475 |
. . . 4
wff 𝑦 = 0 |
9 | | c1 9816 |
. . . 4
class
1 |
10 | | clt 9953 |
. . . . . 6
class
< |
11 | 7, 6, 10 | wbr 4583 |
. . . . 5
wff 0 <
𝑦 |
12 | | cmul 9820 |
. . . . . . 7
class
· |
13 | | cn 10897 |
. . . . . . . 8
class
ℕ |
14 | 2 | cv 1474 |
. . . . . . . . 9
class 𝑥 |
15 | 14 | csn 4125 |
. . . . . . . 8
class {𝑥} |
16 | 13, 15 | cxp 5036 |
. . . . . . 7
class (ℕ
× {𝑥}) |
17 | 12, 16, 9 | cseq 12663 |
. . . . . 6
class seq1(
· , (ℕ × {𝑥})) |
18 | 6, 17 | cfv 5804 |
. . . . 5
class (seq1(
· , (ℕ × {𝑥}))‘𝑦) |
19 | 6 | cneg 10146 |
. . . . . . 7
class -𝑦 |
20 | 19, 17 | cfv 5804 |
. . . . . 6
class (seq1(
· , (ℕ × {𝑥}))‘-𝑦) |
21 | | cdiv 10563 |
. . . . . 6
class
/ |
22 | 9, 20, 21 | co 6549 |
. . . . 5
class (1 /
(seq1( · , (ℕ × {𝑥}))‘-𝑦)) |
23 | 11, 18, 22 | cif 4036 |
. . . 4
class if(0 <
𝑦, (seq1( · ,
(ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ ×
{𝑥}))‘-𝑦))) |
24 | 8, 9, 23 | cif 4036 |
. . 3
class if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ
× {𝑥}))‘𝑦), (1 / (seq1( · ,
(ℕ × {𝑥}))‘-𝑦)))) |
25 | 2, 3, 4, 5, 24 | cmpt2 6551 |
. 2
class (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ
× {𝑥}))‘𝑦), (1 / (seq1( · ,
(ℕ × {𝑥}))‘-𝑦))))) |
26 | 1, 25 | wceq 1475 |
1
wff ↑ =
(𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ
× {𝑥}))‘𝑦), (1 / (seq1( · ,
(ℕ × {𝑥}))‘-𝑦))))) |