Theorem fallfacp1

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

	Ref	Expression
Assertion	fallfacp1	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{\left(N+1\right)}}=\left(A^{\underset{\_}{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		subcl	$$⊢\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		fallfacval	$$⊢\left(A\in ℂ\wedge N+1\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{\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^{\underset{\_}{\left(N+1\right)}}=\prod _{k=0}^{N+1-1}\left(A-k\right)$$
21		fallfacval	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{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^{\underset{\_}{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^{\underset{\_}{\left(N+1\right)}}=\left(A^{\underset{\_}{N}}\right)\left(A-N\right)$$