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

Metamath Proof Explorer

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 𝐾 ) / ( ! ‘ 𝐾 ) ) )