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