This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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