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 𝑁 ) = ( ! ‘ 𝑁 ) )