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^{\underline{0}} = 1$

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		fallrisefac	$⊢ (A \in ℂ \land 0 \in ℕ_{0}) \to A^{\underline{0}} = {(- 1)}^{0} ({(- A)}^{\overline{0}})$
3	1 2	mpan2	$⊢ A \in ℂ \to A^{\underline{0}} = {(- 1)}^{0} ({(- A)}^{\overline{0}})$
4		neg1cn	$⊢ - 1 \in ℂ$
5		exp0	$⊢ - 1 \in ℂ \to {(- 1)}^{0} = 1$
6	4 5	mp1i	$⊢ A \in ℂ \to {(- 1)}^{0} = 1$
7		negcl	$⊢ A \in ℂ \to - A \in ℂ$
8		risefac0	$⊢ - A \in ℂ \to {(- A)}^{\overline{0}} = 1$
9	7 8	syl	$⊢ A \in ℂ \to {(- A)}^{\overline{0}} = 1$
10	6 9	oveq12d	$⊢ A \in ℂ \to {(- 1)}^{0} ({(- A)}^{\overline{0}}) = 1 \cdot 1$
11		1t1e1	$⊢ 1 \cdot 1 = 1$
12	10 11	eqtrdi	$⊢ A \in ℂ \to {(- 1)}^{0} ({(- A)}^{\overline{0}}) = 1$
13	3 12	eqtrd	$⊢ A \in ℂ \to A^{\underline{0}} = 1$

Metamath Proof Explorer