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

Metamath Proof Explorer

Theorem fallfacfac

Description: Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfacfac ( 𝑁 ∈ ℕ0 → ( 𝑁 FallFac 𝑁 ) = ( ! ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 nn0fz0 ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
2 fallfacval4 ⊢ ( 𝑁 ∈ ( 0 ... 𝑁 ) → ( 𝑁 FallFac 𝑁 ) = ( ( ! ‘ 𝑁 ) / ( ! ‘ ( 𝑁 − 𝑁 ) ) ) )
3 1 2 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 FallFac 𝑁 ) = ( ( ! ‘ 𝑁 ) / ( ! ‘ ( 𝑁 − 𝑁 ) ) ) )
4 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
5 4 subidd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 𝑁 ) = 0 )
6 5 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 − 𝑁 ) ) = ( ! ‘ 0 ) )
7 fac0 ⊢ ( ! ‘ 0 ) = 1
8 6 7 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 − 𝑁 ) ) = 1 )
9 8 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) / ( ! ‘ ( 𝑁 − 𝑁 ) ) ) = ( ( ! ‘ 𝑁 ) / 1 ) )
10 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
11 10 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℂ )
12 11 div1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) / 1 ) = ( ! ‘ 𝑁 ) )
13 3 9 12 3eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 FallFac 𝑁 ) = ( ! ‘ 𝑁 ) )