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 
|- ( N e. NN -> ( ( N - 1 ) + ( ( N - 1 ) _C 2 ) ) = ( N _C 2 ) )

Proof

Step Hyp Ref Expression
1 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
2 1 nn0cnd 
 |-  ( N e. NN -> ( N - 1 ) e. CC )
3 2z 
 |-  2 e. ZZ
4 bccl 
 |-  ( ( ( N - 1 ) e. NN0 /\ 2 e. ZZ ) -> ( ( N - 1 ) _C 2 ) e. NN0 )
5 1 3 4 sylancl 
 |-  ( N e. NN -> ( ( N - 1 ) _C 2 ) e. NN0 )
6 5 nn0cnd 
 |-  ( N e. NN -> ( ( N - 1 ) _C 2 ) e. CC )
7 2 6 addcomd 
 |-  ( N e. NN -> ( ( N - 1 ) + ( ( N - 1 ) _C 2 ) ) = ( ( ( N - 1 ) _C 2 ) + ( N - 1 ) ) )
8 bcn1 
 |-  ( ( N - 1 ) e. NN0 -> ( ( N - 1 ) _C 1 ) = ( N - 1 ) )
9 8 eqcomd 
 |-  ( ( N - 1 ) e. NN0 -> ( N - 1 ) = ( ( N - 1 ) _C 1 ) )
10 1 9 syl 
 |-  ( N e. NN -> ( N - 1 ) = ( ( N - 1 ) _C 1 ) )
11 1e2m1 
 |-  1 = ( 2 - 1 )
12 11 a1i 
 |-  ( N e. NN -> 1 = ( 2 - 1 ) )
13 12 oveq2d 
 |-  ( N e. NN -> ( ( N - 1 ) _C 1 ) = ( ( N - 1 ) _C ( 2 - 1 ) ) )
14 10 13 eqtrd 
 |-  ( N e. NN -> ( N - 1 ) = ( ( N - 1 ) _C ( 2 - 1 ) ) )
15 14 oveq2d 
 |-  ( N e. NN -> ( ( ( N - 1 ) _C 2 ) + ( N - 1 ) ) = ( ( ( N - 1 ) _C 2 ) + ( ( N - 1 ) _C ( 2 - 1 ) ) ) )
16 bcpasc 
 |-  ( ( ( N - 1 ) e. NN0 /\ 2 e. ZZ ) -> ( ( ( N - 1 ) _C 2 ) + ( ( N - 1 ) _C ( 2 - 1 ) ) ) = ( ( ( N - 1 ) + 1 ) _C 2 ) )
17 1 3 16 sylancl 
 |-  ( N e. NN -> ( ( ( N - 1 ) _C 2 ) + ( ( N - 1 ) _C ( 2 - 1 ) ) ) = ( ( ( N - 1 ) + 1 ) _C 2 ) )
18 nncn 
 |-  ( N e. NN -> N e. CC )
19 1cnd 
 |-  ( N e. NN -> 1 e. CC )
20 18 19 npcand 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
21 20 oveq1d 
 |-  ( N e. NN -> ( ( ( N - 1 ) + 1 ) _C 2 ) = ( N _C 2 ) )
22 17 21 eqtrd 
 |-  ( N e. NN -> ( ( ( N - 1 ) _C 2 ) + ( ( N - 1 ) _C ( 2 - 1 ) ) ) = ( N _C 2 ) )
23 7 15 22 3eqtrd 
 |-  ( N e. NN -> ( ( N - 1 ) + ( ( N - 1 ) _C 2 ) ) = ( N _C 2 ) )