Metamath Proof Explorer


Theorem risefaccllem

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

Ref Expression
Hypotheses risefallfaccllem.1 𝑆 ⊆ ℂ
risefallfaccllem.2 1 ∈ 𝑆
risefallfaccllem.3 ( ( 𝑥𝑆𝑦𝑆 ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
risefaccllem.4 ( ( 𝐴𝑆𝑘 ∈ ℕ0 ) → ( 𝐴 + 𝑘 ) ∈ 𝑆 )
Assertion risefaccllem ( ( 𝐴𝑆𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 risefallfaccllem.1 𝑆 ⊆ ℂ
2 risefallfaccllem.2 1 ∈ 𝑆
3 risefallfaccllem.3 ( ( 𝑥𝑆𝑦𝑆 ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
4 risefaccllem.4 ( ( 𝐴𝑆𝑘 ∈ ℕ0 ) → ( 𝐴 + 𝑘 ) ∈ 𝑆 )
5 1 sseli ( 𝐴𝑆𝐴 ∈ ℂ )
6 risefacval ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 + 𝑘 ) )
7 5 6 sylan ( ( 𝐴𝑆𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) = ∏ 𝑘 ∈ ( 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 ) → ( 𝐴 RiseFac 𝑁 ) ∈ 𝑆 )