Theorem bcpascm1

Description: Pascal's rule for the binomial coefficient, generalized to all integers K , shifted down by 1. (Contributed by AV, 8-Sep-2019)

	Ref	Expression
Assertion	bcpascm1	|- ( ( N e. NN /\ K e. ZZ ) -> ( ( ( N - 1 ) _C K ) + ( ( N - 1 ) _C ( K - 1 ) ) ) = ( N _C K ) )

Proof

Step	Hyp	Ref	Expression
1		nnm1nn0	|- ( N e. NN -> ( N - 1 ) e. NN0 )
2		bcpasc	|- ( ( ( N - 1 ) e. NN0 /\ K e. ZZ ) -> ( ( ( N - 1 ) _C K ) + ( ( N - 1 ) _C ( K - 1 ) ) ) = ( ( ( N - 1 ) + 1 ) _C K ) )
3	1 2	sylan	|- ( ( N e. NN /\ K e. ZZ ) -> ( ( ( N - 1 ) _C K ) + ( ( N - 1 ) _C ( K - 1 ) ) ) = ( ( ( N - 1 ) + 1 ) _C K ) )
4		nncn	|- ( N e. NN -> N e. CC )
5		npcan1	|- ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
6	4 5	syl	|- ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
7	6	adantr	|- ( ( N e. NN /\ K e. ZZ ) -> ( ( N - 1 ) + 1 ) = N )
8	7	oveq1d	|- ( ( N e. NN /\ K e. ZZ ) -> ( ( ( N - 1 ) + 1 ) _C K ) = ( N _C K ) )
9	3 8	eqtrd	|- ( ( N e. NN /\ K e. ZZ ) -> ( ( ( N - 1 ) _C K ) + ( ( N - 1 ) _C ( K - 1 ) ) ) = ( N _C K ) )