Theorem bcp1m1

Description: Compute the binomial coefficient of ( N + 1 ) over ( N - 1 ) (Contributed by Scott Fenton, 11-May-2014) (Revised by Mario Carneiro, 22-May-2014)

	Ref	Expression
Assertion	bcp1m1	|- ( N e. NN0 -> ( ( N + 1 ) _C ( N - 1 ) ) = ( ( ( N + 1 ) x. N ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	|- ( N e. NN0 -> ( N + 1 ) e. NN0 )
2		nn0z	|- ( N e. NN0 -> N e. ZZ )
3		peano2zm	|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
4	2 3	syl	|- ( N e. NN0 -> ( N - 1 ) e. ZZ )
5		bccmpl	|- ( ( ( N + 1 ) e. NN0 /\ ( N - 1 ) e. ZZ ) -> ( ( N + 1 ) _C ( N - 1 ) ) = ( ( N + 1 ) _C ( ( N + 1 ) - ( N - 1 ) ) ) )
6	1 4 5	syl2anc	|- ( N e. NN0 -> ( ( N + 1 ) _C ( N - 1 ) ) = ( ( N + 1 ) _C ( ( N + 1 ) - ( N - 1 ) ) ) )
7		nn0cn	|- ( N e. NN0 -> N e. CC )
8		1cnd	|- ( N e. NN0 -> 1 e. CC )
9	7 8 8	pnncand	|- ( N e. NN0 -> ( ( N + 1 ) - ( N - 1 ) ) = ( 1 + 1 ) )
10		df-2	|- 2 = ( 1 + 1 )
11	9 10	eqtr4di	|- ( N e. NN0 -> ( ( N + 1 ) - ( N - 1 ) ) = 2 )
12	11	oveq2d	|- ( N e. NN0 -> ( ( N + 1 ) _C ( ( N + 1 ) - ( N - 1 ) ) ) = ( ( N + 1 ) _C 2 ) )
13		bcn2	|- ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) _C 2 ) = ( ( ( N + 1 ) x. ( ( N + 1 ) - 1 ) ) / 2 ) )
14	1 13	syl	|- ( N e. NN0 -> ( ( N + 1 ) _C 2 ) = ( ( ( N + 1 ) x. ( ( N + 1 ) - 1 ) ) / 2 ) )
15		ax-1cn	|- 1 e. CC
16		pncan	|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
17	7 15 16	sylancl	|- ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
18	17	oveq2d	|- ( N e. NN0 -> ( ( N + 1 ) x. ( ( N + 1 ) - 1 ) ) = ( ( N + 1 ) x. N ) )
19	18	oveq1d	|- ( N e. NN0 -> ( ( ( N + 1 ) x. ( ( N + 1 ) - 1 ) ) / 2 ) = ( ( ( N + 1 ) x. N ) / 2 ) )
20	14 19	eqtrd	|- ( N e. NN0 -> ( ( N + 1 ) _C 2 ) = ( ( ( N + 1 ) x. N ) / 2 ) )
21	12 20	eqtrd	|- ( N e. NN0 -> ( ( N + 1 ) _C ( ( N + 1 ) - ( N - 1 ) ) ) = ( ( ( N + 1 ) x. N ) / 2 ) )
22	6 21	eqtrd	|- ( N e. NN0 -> ( ( N + 1 ) _C ( N - 1 ) ) = ( ( ( N + 1 ) x. N ) / 2 ) )