risefacp1

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

		Ref	Expression
	Assertion	risefacp1	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\overline{(N + 1)}} = (A^{\overline{N}}) (A + N)$

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
2	1	adantl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N \in ℂ$
3		1cnd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to 1 \in ℂ$
4	2 3	pncand	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N + 1 - 1 = N$
5	4	oveq2d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (0 \dots N + 1 - 1) = (0 \dots N)$
6	5	prodeq1d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 0}^{N + 1 - 1} (A + k) = \prod_{k = 0}^{N} (A + k)$
7		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
8	7	bilani	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N \in ℤ_{\geq 0}$
9		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
10	9	nn0cnd	$⊢ k \in (0 \dots N) \to k \in ℂ$
11		addcl	$⊢ (A \in ℂ \land k \in ℂ) \to A + k \in ℂ$
12	10 11	sylan2	$⊢ (A \in ℂ \land k \in (0 \dots N)) \to A + k \in ℂ$
13	12	adantlr	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to A + k \in ℂ$
14		oveq2	$⊢ k = N \to A + k = A + N$
15	8 13 14	fprodm1	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 0}^{N} (A + k) = \prod_{k = 0}^{N - 1} (A + k) (A + N)$
16	6 15	eqtrd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 0}^{N + 1 - 1} (A + k) = \prod_{k = 0}^{N - 1} (A + k) (A + N)$
17		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
18		risefacval	$⊢ (A \in ℂ \land N + 1 \in ℕ_{0}) \to A^{\overline{(N + 1)}} = \prod_{k = 0}^{N + 1 - 1} (A + k)$
19	17 18	sylan2	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\overline{(N + 1)}} = \prod_{k = 0}^{N + 1 - 1} (A + k)$
20		risefacval	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\overline{N}} = \prod_{k = 0}^{N - 1} (A + k)$
21	20	oveq1d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (A^{\overline{N}}) (A + N) = \prod_{k = 0}^{N - 1} (A + k) (A + N)$
22	16 19 21	3eqtr4d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\overline{(N + 1)}} = (A^{\overline{N}}) (A + N)$

Metamath Proof Explorer

Theorem risefacp1

Proof