# Metamath Proof Explorer

## Theorem risefacp1

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

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

### Proof

Step Hyp Ref Expression
1 nn0cn ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℂ$
2 1 adantl ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℂ$
3 1cnd ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to 1\in ℂ$
4 2 3 pncand ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {N}+1-1={N}$
5 4 oveq2d ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to \left(0\dots {N}+1-1\right)=\left(0\dots {N}\right)$
6 5 prodeq1d ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to \prod _{{k}=0}^{{N}+1-1}\left({A}+{k}\right)=\prod _{{k}=0}^{{N}}\left({A}+{k}\right)$
7 elnn0uz ${⊢}{N}\in {ℕ}_{0}↔{N}\in {ℤ}_{\ge 0}$
8 7 biimpi ${⊢}{N}\in {ℕ}_{0}\to {N}\in {ℤ}_{\ge 0}$
9 8 adantl ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in {ℤ}_{\ge 0}$
10 elfznn0 ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in {ℕ}_{0}$
11 10 nn0cnd ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in ℂ$
12 addcl ${⊢}\left({A}\in ℂ\wedge {k}\in ℂ\right)\to {A}+{k}\in ℂ$
13 11 12 sylan2 ${⊢}\left({A}\in ℂ\wedge {k}\in \left(0\dots {N}\right)\right)\to {A}+{k}\in ℂ$
14 13 adantlr ${⊢}\left(\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {A}+{k}\in ℂ$
15 oveq2 ${⊢}{k}={N}\to {A}+{k}={A}+{N}$
16 9 14 15 fprodm1 ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to \prod _{{k}=0}^{{N}}\left({A}+{k}\right)=\prod _{{k}=0}^{{N}-1}\left({A}+{k}\right)\left({A}+{N}\right)$
17 6 16 eqtrd ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to \prod _{{k}=0}^{{N}+1-1}\left({A}+{k}\right)=\prod _{{k}=0}^{{N}-1}\left({A}+{k}\right)\left({A}+{N}\right)$
18 peano2nn0 ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in {ℕ}_{0}$
19 risefacval ${⊢}\left({A}\in ℂ\wedge {N}+1\in {ℕ}_{0}\right)\to {{A}}^{\stackrel{‾}{\left({N}+1\right)}}=\prod _{{k}=0}^{{N}+1-1}\left({A}+{k}\right)$
20 18 19 sylan2 ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{\stackrel{‾}{\left({N}+1\right)}}=\prod _{{k}=0}^{{N}+1-1}\left({A}+{k}\right)$
21 risefacval ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{\stackrel{‾}{{N}}}=\prod _{{k}=0}^{{N}-1}\left({A}+{k}\right)$
22 21 oveq1d ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to \left({{A}}^{\stackrel{‾}{{N}}}\right)\left({A}+{N}\right)=\prod _{{k}=0}^{{N}-1}\left({A}+{k}\right)\left({A}+{N}\right)$
23 17 20 22 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{\stackrel{‾}{\left({N}+1\right)}}=\left({{A}}^{\stackrel{‾}{{N}}}\right)\left({A}+{N}\right)$