Description: Define the rising factorial function. This is the function ( A x. ( A + 1 ) x. ... ( A + N ) ) for complex A and nonnegative integers N . (Contributed by Scott Fenton, 5-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | df-risefac | ⊢ RiseFac = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | crisefac | ⊢ RiseFac | |
1 | vx | ⊢ 𝑥 | |
2 | cc | ⊢ ℂ | |
3 | vn | ⊢ 𝑛 | |
4 | cn0 | ⊢ ℕ0 | |
5 | vk | ⊢ 𝑘 | |
6 | cc0 | ⊢ 0 | |
7 | cfz | ⊢ ... | |
8 | 3 | cv | ⊢ 𝑛 |
9 | cmin | ⊢ − | |
10 | c1 | ⊢ 1 | |
11 | 8 10 9 | co | ⊢ ( 𝑛 − 1 ) |
12 | 6 11 7 | co | ⊢ ( 0 ... ( 𝑛 − 1 ) ) |
13 | 1 | cv | ⊢ 𝑥 |
14 | caddc | ⊢ + | |
15 | 5 | cv | ⊢ 𝑘 |
16 | 13 15 14 | co | ⊢ ( 𝑥 + 𝑘 ) |
17 | 12 16 5 | cprod | ⊢ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 ) |
18 | 1 3 2 4 17 | cmpo | ⊢ ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 ) ) |
19 | 0 18 | wceq | ⊢ RiseFac = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 ) ) |