Detailed syntax breakdown of Definition df-risefac
Step | Hyp | Ref
| Expression |
1 | | crisefac 15444 |
. 2
class
RiseFac |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vn |
. . 3
setvar 𝑛 |
4 | | cc 10606 |
. . 3
class
ℂ |
5 | | cn0 11969 |
. . 3
class
ℕ0 |
6 | | cc0 10608 |
. . . . 5
class
0 |
7 | 3 | cv 1541 |
. . . . . 6
class 𝑛 |
8 | | c1 10609 |
. . . . . 6
class
1 |
9 | | cmin 10941 |
. . . . . 6
class
− |
10 | 7, 8, 9 | co 7164 |
. . . . 5
class (𝑛 − 1) |
11 | | cfz 12974 |
. . . . 5
class
... |
12 | 6, 10, 11 | co 7164 |
. . . 4
class
(0...(𝑛 −
1)) |
13 | 2 | cv 1541 |
. . . . 5
class 𝑥 |
14 | | vk |
. . . . . 6
setvar 𝑘 |
15 | 14 | cv 1541 |
. . . . 5
class 𝑘 |
16 | | caddc 10611 |
. . . . 5
class
+ |
17 | 13, 15, 16 | co 7164 |
. . . 4
class (𝑥 + 𝑘) |
18 | 12, 17, 14 | cprod 15344 |
. . 3
class
∏𝑘 ∈
(0...(𝑛 − 1))(𝑥 + 𝑘) |
19 | 2, 3, 4, 5, 18 | cmpo 7166 |
. 2
class (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0
↦ ∏𝑘 ∈
(0...(𝑛 − 1))(𝑥 + 𝑘)) |
20 | 1, 19 | wceq 1542 |
1
wff RiseFac =
(𝑥 ∈ ℂ, 𝑛 ∈ ℕ0
↦ ∏𝑘 ∈
(0...(𝑛 − 1))(𝑥 + 𝑘)) |