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 𝑁 ) = ( ! ‘ 𝑁 ) )