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

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 ) )