Metamath Proof Explorer


Theorem bcn2p1

Description: Compute the binomial coefficient " ( N + 1 ) choose 2 " from " N choose 2 ": N + ( N 2 ) = ( (N+1) 2 ). (Contributed by Alexander van der Vekens, 8-Jan-2018)

Ref Expression
Assertion bcn2p1 N 0 N + ( N 2 ) = ( N + 1 2 )

Proof

Step Hyp Ref Expression
1 nn0cn N 0 N
2 2z 2
3 bccl N 0 2 ( N 2 ) 0
4 2 3 mpan2 N 0 ( N 2 ) 0
5 4 nn0cnd N 0 ( N 2 )
6 1 5 addcomd N 0 N + ( N 2 ) = ( N 2 ) + N
7 bcn1 N 0 ( N 1 ) = N
8 1e2m1 1 = 2 1
9 8 a1i N 0 1 = 2 1
10 9 oveq2d N 0 ( N 1 ) = ( N 2 1 )
11 7 10 eqtr3d N 0 N = ( N 2 1 )
12 11 oveq2d N 0 ( N 2 ) + N = ( N 2 ) + ( N 2 1 )
13 bcpasc N 0 2 ( N 2 ) + ( N 2 1 ) = ( N + 1 2 )
14 2 13 mpan2 N 0 ( N 2 ) + ( N 2 1 ) = ( N + 1 2 )
15 6 12 14 3eqtrd N 0 N + ( N 2 ) = ( N + 1 2 )