Metamath Proof Explorer

Theorem bcnn

Description: N choose N is 1. Remark in Gleason p. 296. (Contributed by NM, 17-Jun-2005) (Revised by Mario Carneiro, 8-Nov-2013)

Ref Expression
Assertion bcnn 
|- ( N e. NN0 -> ( N _C N ) = 1 )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 bccmpl 
 |-  ( ( N e. NN0 /\ 0 e. ZZ ) -> ( N _C 0 ) = ( N _C ( N - 0 ) ) )
3 1 2 mpan2 
 |-  ( N e. NN0 -> ( N _C 0 ) = ( N _C ( N - 0 ) ) )
4 bcn0 
 |-  ( N e. NN0 -> ( N _C 0 ) = 1 )
5 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
6 5 subid1d 
 |-  ( N e. NN0 -> ( N - 0 ) = N )
7 6 oveq2d 
 |-  ( N e. NN0 -> ( N _C ( N - 0 ) ) = ( N _C N ) )
8 3 4 7 3eqtr3rd 
 |-  ( N e. NN0 -> ( N _C N ) = 1 )