Theorem risefac1

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

	Ref	Expression
Assertion	risefac1	$$⊢A\in ℂ\to A^{\bar{1}}=A$$

Proof

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