risefaccllem

Description: Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Hypotheses	risefallfaccllem.1	$⊢ S \subseteq ℂ$
	risefallfaccllem.2	$⊢ 1 \in S$
	risefallfaccllem.3	$⊢ (x \in S \land y \in S) \to x y \in S$
	risefaccllem.4	$⊢ (A \in S \land k \in ℕ_{0}) \to A + k \in S$
Assertion	risefaccllem	$⊢ (A \in S \land N \in ℕ_{0}) \to A^{\overline{N}} \in S$

Step	Hyp	Ref	Expression
1		risefallfaccllem.1	$⊢ S \subseteq ℂ$
2		risefallfaccllem.2	$⊢ 1 \in S$
3		risefallfaccllem.3	$⊢ (x \in S \land y \in S) \to x y \in S$
4		risefaccllem.4	$⊢ (A \in S \land k \in ℕ_{0}) \to A + k \in S$
5	1	sseli	$⊢ A \in S \to A \in ℂ$
6		risefacval	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{\overline{N}} = \prod_{k = 0}^{N - 1} (A + k)$
7	5 6	sylan	$⊢ (A \in S \land N \in ℕ_{0}) \to A^{\overline{N}} = \prod_{k = 0}^{N - 1} (A + k)$
8	1	a1i	$⊢ A \in S \to S \subseteq ℂ$
9	3	adantl	$⊢ (A \in S \land (x \in S \land y \in S)) \to x y \in S$
10		fzfid	$⊢ A \in S \to (0 \dots N - 1) \in Fin$
11		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
12	11 4	sylan2	$⊢ (A \in S \land k \in (0 \dots N - 1)) \to A + k \in S$
13	2	a1i	$⊢ A \in S \to 1 \in S$
14	8 9 10 12 13	fprodcllem	$⊢ A \in S \to \prod_{k = 0}^{N - 1} (A + k) \in S$
15	14	adantr	$⊢ (A \in S \land N \in ℕ_{0}) \to \prod_{k = 0}^{N - 1} (A + k) \in S$
16	7 15	eqeltrd	$⊢ (A \in S \land N \in ℕ_{0}) \to A^{\overline{N}} \in S$

Metamath Proof Explorer