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 {\mathbb{N}}_0\right)\to A^{\overline{\left(N+1\right)}}=\left(A^{\bar{N}}\right)\left(A+N\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
2	1	adantl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to N\in ℂ$$
3		1cnd	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to 1\in ℂ$$
4	2 3	pncand	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to N+1-1=N$$
5	4	oveq2d	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(0\dots N+1-1\right)=\left(0\dots N\right)$$
6	5	prodeq1d	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_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 {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$
8	7	biimpi	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{Z}}_{\ge 0}$$
9	8	adantl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{Z}}_{\ge 0}$$
10		elfznn0	$$⊢k\in \left(0\dots N\right)\to k\in {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
19		risefacval	$$⊢\left(A\in ℂ\wedge N+1\in {\mathbb{N}}_0\right)\to A^{\overline{\left(N+1\right)}}=\prod _{k=0}^{N+1-1}\left(A+k\right)$$
20	18 19	sylan2	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\overline{\left(N+1\right)}}=\prod _{k=0}^{N+1-1}\left(A+k\right)$$
21		risefacval	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}=\prod _{k=0}^{N-1}\left(A+k\right)$$
22	21	oveq1d	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(A^{\bar{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 {\mathbb{N}}_0\right)\to A^{\overline{\left(N+1\right)}}=\left(A^{\bar{N}}\right)\left(A+N\right)$$