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