risefac1

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

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

Step	Hyp	Ref	Expression
1		0p1e1	$⊢ 0 + 1 = 1$
2	1	oveq2i	$⊢ A^{\overline{(0 + 1)}} = A^{\overline{1}}$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4		risefacp1	$⊢ (A \in ℂ \land 0 \in ℕ_{0}) \to A^{\overline{(0 + 1)}} = (A^{\overline{0}}) (A + 0)$
5	3 4	mpan2	$⊢ A \in ℂ \to A^{\overline{(0 + 1)}} = (A^{\overline{0}}) (A + 0)$
6		risefac0	$⊢ A \in ℂ \to A^{\overline{0}} = 1$
7		addrid	$⊢ A \in ℂ \to A + 0 = A$
8	6 7	oveq12d	$⊢ A \in ℂ \to (A^{\overline{0}}) (A + 0) = 1 A$
9		mullid	$⊢ A \in ℂ \to 1 A = A$
10	5 8 9	3eqtrd	$⊢ A \in ℂ \to A^{\overline{(0 + 1)}} = A$
11	2 10	eqtr3id	$⊢ A \in ℂ \to A^{\overline{1}} = A$

Metamath Proof Explorer