Metamath Proof Explorer

Theorem bcn2

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

Ref Expression
Assertion bcn2 ⊢N∈ℕ0→(N2)=N⁢N−12

Proof

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