Metamath Proof Explorer

Theorem risefacval

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

Ref Expression
Assertion risefacval ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{\stackrel{‾}{{N}}}=\prod _{{k}=0}^{{N}-1}\left({A}+{k}\right)$

Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{x}={A}\to {x}+{k}={A}+{k}$
2 1 prodeq2sdv ${⊢}{x}={A}\to \prod _{{k}=0}^{{n}-1}\left({x}+{k}\right)=\prod _{{k}=0}^{{n}-1}\left({A}+{k}\right)$
3 oveq1 ${⊢}{n}={N}\to {n}-1={N}-1$
4 3 oveq2d ${⊢}{n}={N}\to \left(0\dots {n}-1\right)=\left(0\dots {N}-1\right)$
5 4 prodeq1d ${⊢}{n}={N}\to \prod _{{k}=0}^{{n}-1}\left({A}+{k}\right)=\prod _{{k}=0}^{{N}-1}\left({A}+{k}\right)$
6 df-risefac ${⊢}RiseFac=\left({x}\in ℂ,{n}\in {ℕ}_{0}⟼\prod _{{k}=0}^{{n}-1}\left({x}+{k}\right)\right)$
7 prodex ${⊢}\prod _{{k}=0}^{{N}-1}\left({A}+{k}\right)\in \mathrm{V}$
8 2 5 6 7 ovmpo ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{\stackrel{‾}{{N}}}=\prod _{{k}=0}^{{N}-1}\left({A}+{k}\right)$