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 ) )