Metamath Proof Explorer


Theorem bcn2

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

Ref Expression
Assertion bcn2 ( 𝑁 ∈ ℕ0 → ( 𝑁 C 2 ) = ( ( 𝑁 · ( 𝑁 − 1 ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 2nn 2 ∈ ℕ
2 bcval5 ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℕ ) → ( 𝑁 C 2 ) = ( ( seq ( ( 𝑁 − 2 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 2 ) ) )
3 1 2 mpan2 ( 𝑁 ∈ ℕ0 → ( 𝑁 C 2 ) = ( ( seq ( ( 𝑁 − 2 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 2 ) ) )
4 2m1e1 ( 2 − 1 ) = 1
5 4 oveq2i ( ( 𝑁 − 2 ) + ( 2 − 1 ) ) = ( ( 𝑁 − 2 ) + 1 )
6 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
7 2cn 2 ∈ ℂ
8 ax-1cn 1 ∈ ℂ
9 npncan ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 2 ) + ( 2 − 1 ) ) = ( 𝑁 − 1 ) )
10 7 8 9 mp3an23 ( 𝑁 ∈ ℂ → ( ( 𝑁 − 2 ) + ( 2 − 1 ) ) = ( 𝑁 − 1 ) )
11 6 10 syl ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 2 ) + ( 2 − 1 ) ) = ( 𝑁 − 1 ) )
12 5 11 eqtr3id ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − 1 ) )
13 12 seqeq1d ( 𝑁 ∈ ℕ0 → seq ( ( 𝑁 − 2 ) + 1 ) ( · , I ) = seq ( 𝑁 − 1 ) ( · , I ) )
14 13 fveq1d ( 𝑁 ∈ ℕ0 → ( seq ( ( 𝑁 − 2 ) + 1 ) ( · , I ) ‘ 𝑁 ) = ( seq ( 𝑁 − 1 ) ( · , I ) ‘ 𝑁 ) )
15 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
16 peano2zm ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
17 15 16 syl ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℤ )
18 uzid ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ𝑁 ) )
19 15 18 syl ( 𝑁 ∈ ℕ0𝑁 ∈ ( ℤ𝑁 ) )
20 npcan ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
21 6 8 20 sylancl ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
22 21 fveq2d ( 𝑁 ∈ ℕ0 → ( ℤ ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ℤ𝑁 ) )
23 19 22 eleqtrrd ( 𝑁 ∈ ℕ0𝑁 ∈ ( ℤ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
24 seqm1 ( ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ ( ( 𝑁 − 1 ) + 1 ) ) ) → ( seq ( 𝑁 − 1 ) ( · , I ) ‘ 𝑁 ) = ( ( seq ( 𝑁 − 1 ) ( · , I ) ‘ ( 𝑁 − 1 ) ) · ( I ‘ 𝑁 ) ) )
25 17 23 24 syl2anc ( 𝑁 ∈ ℕ0 → ( seq ( 𝑁 − 1 ) ( · , I ) ‘ 𝑁 ) = ( ( seq ( 𝑁 − 1 ) ( · , I ) ‘ ( 𝑁 − 1 ) ) · ( I ‘ 𝑁 ) ) )
26 seq1 ( ( 𝑁 − 1 ) ∈ ℤ → ( seq ( 𝑁 − 1 ) ( · , I ) ‘ ( 𝑁 − 1 ) ) = ( I ‘ ( 𝑁 − 1 ) ) )
27 17 26 syl ( 𝑁 ∈ ℕ0 → ( seq ( 𝑁 − 1 ) ( · , I ) ‘ ( 𝑁 − 1 ) ) = ( I ‘ ( 𝑁 − 1 ) ) )
28 fvi ( ( 𝑁 − 1 ) ∈ ℤ → ( I ‘ ( 𝑁 − 1 ) ) = ( 𝑁 − 1 ) )
29 17 28 syl ( 𝑁 ∈ ℕ0 → ( I ‘ ( 𝑁 − 1 ) ) = ( 𝑁 − 1 ) )
30 27 29 eqtrd ( 𝑁 ∈ ℕ0 → ( seq ( 𝑁 − 1 ) ( · , I ) ‘ ( 𝑁 − 1 ) ) = ( 𝑁 − 1 ) )
31 fvi ( 𝑁 ∈ ℕ0 → ( I ‘ 𝑁 ) = 𝑁 )
32 30 31 oveq12d ( 𝑁 ∈ ℕ0 → ( ( seq ( 𝑁 − 1 ) ( · , I ) ‘ ( 𝑁 − 1 ) ) · ( I ‘ 𝑁 ) ) = ( ( 𝑁 − 1 ) · 𝑁 ) )
33 25 32 eqtrd ( 𝑁 ∈ ℕ0 → ( seq ( 𝑁 − 1 ) ( · , I ) ‘ 𝑁 ) = ( ( 𝑁 − 1 ) · 𝑁 ) )
34 subcl ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℂ )
35 6 8 34 sylancl ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℂ )
36 35 6 mulcomd ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) · 𝑁 ) = ( 𝑁 · ( 𝑁 − 1 ) ) )
37 33 36 eqtrd ( 𝑁 ∈ ℕ0 → ( seq ( 𝑁 − 1 ) ( · , I ) ‘ 𝑁 ) = ( 𝑁 · ( 𝑁 − 1 ) ) )
38 14 37 eqtrd ( 𝑁 ∈ ℕ0 → ( seq ( ( 𝑁 − 2 ) + 1 ) ( · , I ) ‘ 𝑁 ) = ( 𝑁 · ( 𝑁 − 1 ) ) )
39 fac2 ( ! ‘ 2 ) = 2
40 39 a1i ( 𝑁 ∈ ℕ0 → ( ! ‘ 2 ) = 2 )
41 38 40 oveq12d ( 𝑁 ∈ ℕ0 → ( ( seq ( ( 𝑁 − 2 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 2 ) ) = ( ( 𝑁 · ( 𝑁 − 1 ) ) / 2 ) )
42 3 41 eqtrd ( 𝑁 ∈ ℕ0 → ( 𝑁 C 2 ) = ( ( 𝑁 · ( 𝑁 − 1 ) ) / 2 ) )