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