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	|- ( N e. NN0 -> ( ( N + 1 ) _C N ) = ( N + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	|- ( N e. NN0 -> ( N + 1 ) e. NN0 )
2		nn0z	|- ( N e. NN0 -> N e. ZZ )
3		bccmpl	|- ( ( ( N + 1 ) e. NN0 /\ N e. ZZ ) -> ( ( N + 1 ) _C N ) = ( ( N + 1 ) _C ( ( N + 1 ) - N ) ) )
4	1 2 3	syl2anc	|- ( N e. NN0 -> ( ( N + 1 ) _C N ) = ( ( N + 1 ) _C ( ( N + 1 ) - N ) ) )
5		nn0cn	|- ( N e. NN0 -> N e. CC )
6		ax-1cn	|- 1 e. CC
7		pncan2	|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - N ) = 1 )
8	5 6 7	sylancl	|- ( N e. NN0 -> ( ( N + 1 ) - N ) = 1 )
9	8	oveq2d	|- ( N e. NN0 -> ( ( N + 1 ) _C ( ( N + 1 ) - N ) ) = ( ( N + 1 ) _C 1 ) )
10		bcn1	|- ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) _C 1 ) = ( N + 1 ) )
11	1 10	syl	|- ( N e. NN0 -> ( ( N + 1 ) _C 1 ) = ( N + 1 ) )
12	4 9 11	3eqtrd	|- ( N e. NN0 -> ( ( N + 1 ) _C N ) = ( N + 1 ) )