This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem risefacval

Description: The value of the rising factorial function. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion risefacval ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 + 𝑘 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 + 𝑘 ) = ( 𝐴 + 𝑘 ) )
2 1 prodeq2sdv ⊢ ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 + 𝑘 ) )
3 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 − 1 ) = ( 𝑁 − 1 ) )
4 3 oveq2d ⊢ ( 𝑛 = 𝑁 → ( 0 ... ( 𝑛 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) ) )
5 4 prodeq1d ⊢ ( 𝑛 = 𝑁 → ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 + 𝑘 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 + 𝑘 ) )
6 df-risefac ⊢ RiseFac = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑥 + 𝑘 ) )
7 prodex ⊢ ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 + 𝑘 ) ∈ V
8 2 5 6 7 ovmpo ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 + 𝑘 ) )