Theorem bcnm1

Description: The binomial coefficent of ( N - 1 ) is N . (Contributed by Scott Fenton, 16-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		1z	|- 1 e. ZZ
2		bccmpl	|- ( ( N e. NN0 /\ 1 e. ZZ ) -> ( N _C 1 ) = ( N _C ( N - 1 ) ) )
3	1 2	mpan2	|- ( N e. NN0 -> ( N _C 1 ) = ( N _C ( N - 1 ) ) )
4		bcn1	|- ( N e. NN0 -> ( N _C 1 ) = N )
5	3 4	eqtr3d	|- ( N e. NN0 -> ( N _C ( N - 1 ) ) = N )