Metamath Proof Explorer

Theorem 0risefac

Description: The value of the zero rising factorial at natural N . (Contributed by Scott Fenton, 17-Feb-2018)

Ref Expression
Assertion 0risefac ( 𝑁 ∈ ℕ → ( 0 RiseFac 𝑁 ) = 0 )

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3 risefallfac ⊢ ( ( 0 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 0 RiseFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - 0 FallFac 𝑁 ) ) )
4 1 2 3 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 0 RiseFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - 0 FallFac 𝑁 ) ) )
5 neg0 ⊢ - 0 = 0
6 5 oveq1i ⊢ ( - 0 FallFac 𝑁 ) = ( 0 FallFac 𝑁 )
7 0fallfac ⊢ ( 𝑁 ∈ ℕ → ( 0 FallFac 𝑁 ) = 0 )
8 6 7 eqtrid ⊢ ( 𝑁 ∈ ℕ → ( - 0 FallFac 𝑁 ) = 0 )
9 8 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑ 𝑁 ) · ( - 0 FallFac 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · 0 ) )
10 neg1cn ⊢ - 1 ∈ ℂ
11 expcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℂ )
12 10 2 11 sylancr ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑ 𝑁 ) ∈ ℂ )
13 12 mul01d ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑ 𝑁 ) · 0 ) = 0 )
14 4 9 13 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 0 RiseFac 𝑁 ) = 0 )