0risefac

Description: The value of the zero rising factorial at natural N . (Contributed by Scott Fenton, 17-Feb-2018)

		Ref	Expression
	Assertion	0risefac	$⊢ N \in ℕ \to 0^{\overline{N}} = 0$

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
3		risefallfac	$⊢ (0 \in ℂ \land N \in ℕ_{0}) \to 0^{\overline{N}} = {(- 1)}^{N} ({-0}^{\underline{N}})$
4	1 2 3	sylancr	$⊢ N \in ℕ \to 0^{\overline{N}} = {(- 1)}^{N} ({-0}^{\underline{N}})$
5		neg0	$⊢ - 0 = 0$
6	5	oveq1i	$⊢ {-0}^{\underline{N}} = 0^{\underline{N}}$
7		0fallfac	$⊢ N \in ℕ \to 0^{\underline{N}} = 0$
8	6 7	eqtrid	$⊢ N \in ℕ \to {-0}^{\underline{N}} = 0$
9	8	oveq2d	$⊢ N \in ℕ \to {(- 1)}^{N} ({-0}^{\underline{N}}) = {(- 1)}^{N} \cdot 0$
10		neg1cn	$⊢ - 1 \in ℂ$
11		expcl	$⊢ (- 1 \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} \in ℂ$
12	10 2 11	sylancr	$⊢ N \in ℕ \to {(- 1)}^{N} \in ℂ$
13	12	mul01d	$⊢ N \in ℕ \to {(- 1)}^{N} \cdot 0 = 0$
14	4 9 13	3eqtrd	$⊢ N \in ℕ \to 0^{\overline{N}} = 0$

Metamath Proof Explorer