Metamath Proof Explorer

Theorem bcn2

Description: Binomial coefficient: N choose 2 . (Contributed by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion bcn2 
|- ( N e. NN0 -> ( N _C 2 ) = ( ( N x. ( N - 1 ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 bcval5 
 |-  ( ( N e. NN0 /\ 2 e. NN ) -> ( N _C 2 ) = ( ( seq ( ( N - 2 ) + 1 ) ( x. , _I ) ` N ) / ( ! ` 2 ) ) )
3 1 2 mpan2 
 |-  ( N e. NN0 -> ( N _C 2 ) = ( ( seq ( ( N - 2 ) + 1 ) ( x. , _I ) ` N ) / ( ! ` 2 ) ) )
4 2m1e1 
 |-  ( 2 - 1 ) = 1
5 4 oveq2i 
 |-  ( ( N - 2 ) + ( 2 - 1 ) ) = ( ( N - 2 ) + 1 )
6 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
7 2cn 
 |-  2 e. CC
8 ax-1cn 
 |-  1 e. CC
9 npncan 
 |-  ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N - 2 ) + ( 2 - 1 ) ) = ( N - 1 ) )
10 7 8 9 mp3an23 
 |-  ( N e. CC -> ( ( N - 2 ) + ( 2 - 1 ) ) = ( N - 1 ) )
11 6 10 syl 
 |-  ( N e. NN0 -> ( ( N - 2 ) + ( 2 - 1 ) ) = ( N - 1 ) )
12 5 11 eqtr3id 
 |-  ( N e. NN0 -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
13 12 seqeq1d 
 |-  ( N e. NN0 -> seq ( ( N - 2 ) + 1 ) ( x. , _I ) = seq ( N - 1 ) ( x. , _I ) )
14 13 fveq1d 
 |-  ( N e. NN0 -> ( seq ( ( N - 2 ) + 1 ) ( x. , _I ) ` N ) = ( seq ( N - 1 ) ( x. , _I ) ` N ) )
15 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
16 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
17 15 16 syl 
 |-  ( N e. NN0 -> ( N - 1 ) e. ZZ )
18 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
19 15 18 syl 
 |-  ( N e. NN0 -> N e. ( ZZ>= ` N ) )
20 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
21 6 8 20 sylancl 
 |-  ( N e. NN0 -> ( ( N - 1 ) + 1 ) = N )
22 21 fveq2d 
 |-  ( N e. NN0 -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) = ( ZZ>= ` N ) )
23 19 22 eleqtrrd 
 |-  ( N e. NN0 -> N e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
24 seqm1 
 |-  ( ( ( N - 1 ) e. ZZ /\ N e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) ) -> ( seq ( N - 1 ) ( x. , _I ) ` N ) = ( ( seq ( N - 1 ) ( x. , _I ) ` ( N - 1 ) ) x. ( _I ` N ) ) )
25 17 23 24 syl2anc 
 |-  ( N e. NN0 -> ( seq ( N - 1 ) ( x. , _I ) ` N ) = ( ( seq ( N - 1 ) ( x. , _I ) ` ( N - 1 ) ) x. ( _I ` N ) ) )
26 seq1 
 |-  ( ( N - 1 ) e. ZZ -> ( seq ( N - 1 ) ( x. , _I ) ` ( N - 1 ) ) = ( _I ` ( N - 1 ) ) )
27 17 26 syl 
 |-  ( N e. NN0 -> ( seq ( N - 1 ) ( x. , _I ) ` ( N - 1 ) ) = ( _I ` ( N - 1 ) ) )
28 fvi 
 |-  ( ( N - 1 ) e. ZZ -> ( _I ` ( N - 1 ) ) = ( N - 1 ) )
29 17 28 syl 
 |-  ( N e. NN0 -> ( _I ` ( N - 1 ) ) = ( N - 1 ) )
30 27 29 eqtrd 
 |-  ( N e. NN0 -> ( seq ( N - 1 ) ( x. , _I ) ` ( N - 1 ) ) = ( N - 1 ) )
31 fvi 
 |-  ( N e. NN0 -> ( _I ` N ) = N )
32 30 31 oveq12d 
 |-  ( N e. NN0 -> ( ( seq ( N - 1 ) ( x. , _I ) ` ( N - 1 ) ) x. ( _I ` N ) ) = ( ( N - 1 ) x. N ) )
33 25 32 eqtrd 
 |-  ( N e. NN0 -> ( seq ( N - 1 ) ( x. , _I ) ` N ) = ( ( N - 1 ) x. N ) )
34 subcl 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N - 1 ) e. CC )
35 6 8 34 sylancl 
 |-  ( N e. NN0 -> ( N - 1 ) e. CC )
36 35 6 mulcomd 
 |-  ( N e. NN0 -> ( ( N - 1 ) x. N ) = ( N x. ( N - 1 ) ) )
37 33 36 eqtrd 
 |-  ( N e. NN0 -> ( seq ( N - 1 ) ( x. , _I ) ` N ) = ( N x. ( N - 1 ) ) )
38 14 37 eqtrd 
 |-  ( N e. NN0 -> ( seq ( ( N - 2 ) + 1 ) ( x. , _I ) ` N ) = ( N x. ( N - 1 ) ) )
39 fac2 
 |-  ( ! ` 2 ) = 2
40 39 a1i 
 |-  ( N e. NN0 -> ( ! ` 2 ) = 2 )
41 38 40 oveq12d 
 |-  ( N e. NN0 -> ( ( seq ( ( N - 2 ) + 1 ) ( x. , _I ) ` N ) / ( ! ` 2 ) ) = ( ( N x. ( N - 1 ) ) / 2 ) )
42 3 41 eqtrd 
 |-  ( N e. NN0 -> ( N _C 2 ) = ( ( N x. ( N - 1 ) ) / 2 ) )