Metamath Proof Explorer


Theorem bcn2m1

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

Ref Expression
Assertion bcn2m1 NN-1+(N12)=(N2)

Proof

Step Hyp Ref Expression
1 nnm1nn0 NN10
2 1 nn0cnd NN1
3 2z 2
4 bccl N102(N12)0
5 1 3 4 sylancl N(N12)0
6 5 nn0cnd N(N12)
7 2 6 addcomd NN-1+(N12)=(N12)+N-1
8 bcn1 N10(N11)=N1
9 8 eqcomd N10N1=(N11)
10 1 9 syl NN1=(N11)
11 1e2m1 1=21
12 11 a1i N1=21
13 12 oveq2d N(N11)=(N121)
14 10 13 eqtrd NN1=(N121)
15 14 oveq2d N(N12)+N-1=(N12)+(N121)
16 bcpasc N102(N12)+(N121)=(N-1+12)
17 1 3 16 sylancl N(N12)+(N121)=(N-1+12)
18 nncn NN
19 1cnd N1
20 18 19 npcand NN-1+1=N
21 20 oveq1d N(N-1+12)=(N2)
22 17 21 eqtrd N(N12)+(N121)=(N2)
23 7 15 22 3eqtrd NN-1+(N12)=(N2)