Theorem fallfaccllem

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

	Ref	Expression
Hypotheses	risefallfaccllem.1	⊢ 𝑆 ⊆ ℂ
	risefallfaccllem.2	⊢ 1 ∈ 𝑆
	risefallfaccllem.3	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
	fallfaccllem.4	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 − 𝑘 ) ∈ 𝑆 )
Assertion	fallfaccllem	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		risefallfaccllem.1	⊢ 𝑆 ⊆ ℂ
2		risefallfaccllem.2	⊢ 1 ∈ 𝑆
3		risefallfaccllem.3	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
4		fallfaccllem.4	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 − 𝑘 ) ∈ 𝑆 )
5	1	sseli	⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ∈ ℂ )
6		fallfacval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) )
7	5 6	sylan	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) )
8	1	a1i	⊢ ( 𝐴 ∈ 𝑆 → 𝑆 ⊆ ℂ )
9	3	adantl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
10		fzfid	⊢ ( 𝐴 ∈ 𝑆 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
11		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
12	11 4	sylan2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 − 𝑘 ) ∈ 𝑆 )
13	2	a1i	⊢ ( 𝐴 ∈ 𝑆 → 1 ∈ 𝑆 )
14	8 9 10 12 13	fprodcllem	⊢ ( 𝐴 ∈ 𝑆 → ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) ∈ 𝑆 )
15	14	adantr	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) ∈ 𝑆 )
16	7 15	eqeltrd	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) ∈ 𝑆 )