Metamath Proof Explorer


Definition df-risefac

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 ) ) ( 𝑥 + 𝑘 ) )

Detailed syntax breakdown

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 ) ) ( 𝑥 + 𝑘 ) )