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