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

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 )