Theorem bcfallfac

Description: Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018)

	Ref	Expression
Assertion	bcfallfac	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfz3nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
2	1	faccld	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℕ )
3	2	nncnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℂ )
4		fznn0sub	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
5	4	faccld	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ )
6	5	nncnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℂ )
7		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
8	7	faccld	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℕ )
9	8	nncnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
10	5	nnne0d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ≠ 0 )
11	8	nnne0d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ≠ 0 )
12	3 6 9 10 11	divdiv1d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ! ‘ ( 𝑁 − 𝐾 ) ) ) / ( ! ‘ 𝐾 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
13		fallfacval4	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 FallFac 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ! ‘ ( 𝑁 − 𝐾 ) ) ) )
14	13	oveq1d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) / ( ! ‘ ( 𝑁 − 𝐾 ) ) ) / ( ! ‘ 𝐾 ) ) )
15		bcval2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
16	12 14 15	3eqtr4rd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )