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 0 ( N + 1 N 1 ) = N + 1 N 2

Proof

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