Metamath Proof Explorer


Theorem bcnp1n

Description: Binomial coefficient: N + 1 choose N . (Contributed by NM, 20-Jun-2005) (Revised by Mario Carneiro, 8-Nov-2013)

Ref Expression
Assertion bcnp1n ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C 𝑁 ) = ( 𝑁 + 1 ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
2 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
3 bccmpl ( ( ( 𝑁 + 1 ) ∈ ℕ0𝑁 ∈ ℤ ) → ( ( 𝑁 + 1 ) C 𝑁 ) = ( ( 𝑁 + 1 ) C ( ( 𝑁 + 1 ) − 𝑁 ) ) )
4 1 2 3 syl2anc ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C 𝑁 ) = ( ( 𝑁 + 1 ) C ( ( 𝑁 + 1 ) − 𝑁 ) ) )
5 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
6 ax-1cn 1 ∈ ℂ
7 pncan2 ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 𝑁 ) = 1 )
8 5 6 7 sylancl ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 𝑁 ) = 1 )
9 8 oveq2d ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( ( 𝑁 + 1 ) − 𝑁 ) ) = ( ( 𝑁 + 1 ) C 1 ) )
10 bcn1 ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) C 1 ) = ( 𝑁 + 1 ) )
11 1 10 syl ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C 1 ) = ( 𝑁 + 1 ) )
12 4 9 11 3eqtrd ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C 𝑁 ) = ( 𝑁 + 1 ) )