Description: The binomial coefficent of ( N - 1 ) is N . (Contributed by Scott Fenton, 16-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | bcnm1 | ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C ( 𝑁 − 1 ) ) = 𝑁 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1z | ⊢ 1 ∈ ℤ | |
2 | bccmpl | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 1 ∈ ℤ ) → ( 𝑁 C 1 ) = ( 𝑁 C ( 𝑁 − 1 ) ) ) | |
3 | 1 2 | mpan2 | ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 1 ) = ( 𝑁 C ( 𝑁 − 1 ) ) ) |
4 | bcn1 | ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 1 ) = 𝑁 ) | |
5 | 3 4 | eqtr3d | ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C ( 𝑁 − 1 ) ) = 𝑁 ) |