Theorem fallfaccl

Description: Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	fallfaccl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{N}}\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢ℂ\subseteq ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3		mulcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to xy\in ℂ$$
4		nn0cn	$$⊢k\in {\mathbb{N}}_0\to k\in ℂ$$
5		subcl	$$⊢\left(A\in ℂ\wedge k\in ℂ\right)\to A-k\in ℂ$$
6	4 5	sylan2	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A-k\in ℂ$$
7	1 2 3 6	fallfaccllem	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{N}}\in ℂ$$