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 N0N+(N2)=(N+12)

Proof

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