Theorem refallfaccl

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

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

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	$$⊢ℝ\subseteq ℂ$$
2		1re	$$⊢1\in ℝ$$
3		remulcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to xy\in ℝ$$
4		nn0re	$$⊢k\in {\mathbb{N}}_0\to k\in ℝ$$
5		resubcl	$$⊢\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 ℝ$$