Theorem fallfac1

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

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

Proof

Step	Hyp	Ref	Expression
1		0p1e1	$$⊢0+1=1$$
2	1	oveq2i	$$⊢A^{\underset{\_}{\left(0+1\right)}}=A^{\underset{\_}{1}}$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		fallfacp1	$$⊢\left(A\in ℂ\wedge 0\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{\left(0+1\right)}}=\left(A^{\underset{\_}{0}}\right)\left(A-0\right)$$
5	3 4	mpan2	$$⊢A\in ℂ\to A^{\underset{\_}{\left(0+1\right)}}=\left(A^{\underset{\_}{0}}\right)\left(A-0\right)$$
6		fallfac0	$$⊢A\in ℂ\to A^{\underset{\_}{0}}=1$$
7		subid1	$$⊢A\in ℂ\to A-0=A$$
8	6 7	oveq12d	$$⊢A\in ℂ\to \left(A^{\underset{\_}{0}}\right)\left(A-0\right)=1A$$
9		mulid2	$$⊢A\in ℂ\to 1A=A$$
10	5 8 9	3eqtrd	$$⊢A\in ℂ\to A^{\underset{\_}{\left(0+1\right)}}=A$$
11	2 10	eqtr3id	$$⊢A\in ℂ\to A^{\underset{\_}{1}}=A$$