This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑁 ) ∈ 𝑆 )