Metamath Proof Explorer


Theorem fallfac0

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

Ref Expression
Assertion fallfac0 ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = 1 )

Proof

Step Hyp Ref Expression
1 0nn0 0 ∈ ℕ0
2 fallrisefac ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 FallFac 0 ) = ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) )
3 1 2 mpan2 ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) )
4 neg1cn - 1 ∈ ℂ
5 exp0 ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
6 4 5 mp1i ( 𝐴 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
7 negcl ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
8 risefac0 ( - 𝐴 ∈ ℂ → ( - 𝐴 RiseFac 0 ) = 1 )
9 7 8 syl ( 𝐴 ∈ ℂ → ( - 𝐴 RiseFac 0 ) = 1 )
10 6 9 oveq12d ( 𝐴 ∈ ℂ → ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) = ( 1 · 1 ) )
11 1t1e1 ( 1 · 1 ) = 1
12 10 11 eqtrdi ( 𝐴 ∈ ℂ → ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) = 1 )
13 3 12 eqtrd ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = 1 )