Theorem risefac0

Description: The value of the rising factorial when N = 0 . (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	risefac0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 RiseFac 0 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		risefacval	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 RiseFac 0 ) = ∏ 𝑘 ∈ ( 0 ... ( 0 − 1 ) ) ( 𝐴 + 𝑘 ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 RiseFac 0 ) = ∏ 𝑘 ∈ ( 0 ... ( 0 − 1 ) ) ( 𝐴 + 𝑘 ) )
4		risefall0lem	⊢ ( 0 ... ( 0 − 1 ) ) = ∅
5	4	prodeq1i	⊢ ∏ 𝑘 ∈ ( 0 ... ( 0 − 1 ) ) ( 𝐴 + 𝑘 ) = ∏ 𝑘 ∈ ∅ ( 𝐴 + 𝑘 )
6		prod0	⊢ ∏ 𝑘 ∈ ∅ ( 𝐴 + 𝑘 ) = 1
7	5 6	eqtri	⊢ ∏ 𝑘 ∈ ( 0 ... ( 0 − 1 ) ) ( 𝐴 + 𝑘 ) = 1
8	3 7	eqtrdi	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 RiseFac 0 ) = 1 )