Theorem fallfac0

Description: The value of the falling factorial when N = 0 . (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	fallfac0	$$⊢A\in ℂ\to A^{\underset{\_}{0}}=1$$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		fallrisefac	$$⊢\left(A\in ℂ\wedge 0\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{0}}={\left(-1\right)}^0\left({\left(-A\right)}^{\bar{0}}\right)$$
3	1 2	mpan2	$$⊢A\in ℂ\to A^{\underset{\_}{0}}={\left(-1\right)}^0\left({\left(-A\right)}^{\bar{0}}\right)$$
4		neg1cn	$$⊢-1\in ℂ$$
5		exp0	$$⊢-1\in ℂ\to {\left(-1\right)}^0=1$$
6	4 5	mp1i	$$⊢A\in ℂ\to {\left(-1\right)}^0=1$$
7		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
8		risefac0	$$⊢-A\in ℂ\to {\left(-A\right)}^{\bar{0}}=1$$
9	7 8	syl	$$⊢A\in ℂ\to {\left(-A\right)}^{\bar{0}}=1$$
10	6 9	oveq12d	$$⊢A\in ℂ\to {\left(-1\right)}^0\left({\left(-A\right)}^{\bar{0}}\right)=1\cdot 1$$
11		1t1e1	$$⊢1\cdot 1=1$$
12	10 11	eqtrdi	$$⊢A\in ℂ\to {\left(-1\right)}^0\left({\left(-A\right)}^{\bar{0}}\right)=1$$
13	3 12	eqtrd	$$⊢A\in ℂ\to A^{\underset{\_}{0}}=1$$