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

Metamath Proof Explorer

Theorem risefacfac

Description: Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion risefacfac ( 𝑁 ∈ ℕ0 → ( 1 RiseFac 𝑁 ) = ( ! ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 1cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
2 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
3 2 nncnd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
4 3 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
5 1 4 pncan3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 1 + ( 𝑘 − 1 ) ) = 𝑘 )
6 5 prodeq2dv ⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( 1 + ( 𝑘 − 1 ) ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 )
7 ax-1cn ⊢ 1 ∈ ℂ
8 risefacval2 ⊢ ( ( 1 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 1 RiseFac 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( 1 + ( 𝑘 − 1 ) ) )
9 7 8 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( 1 RiseFac 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( 1 + ( 𝑘 − 1 ) ) )
10 fprodfac ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 )
11 6 9 10 3eqtr4d ⊢ ( 𝑁 ∈ ℕ0 → ( 1 RiseFac 𝑁 ) = ( ! ‘ 𝑁 ) )