bcn2

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

		Ref	Expression
	Assertion	bcn2	$⊢ N \in ℕ_{0} \to (\binom{N}{2}) = \frac{N (N - 1)}{2}$

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2		bcval5	$⊢ (N \in ℕ_{0} \land 2 \in ℕ) \to (\binom{N}{2}) = \frac{seq (N - 2 + 1) (\times I) (N)}{2!}$
3	1 2	mpan2	$⊢ N \in ℕ_{0} \to (\binom{N}{2}) = \frac{seq (N - 2 + 1) (\times I) (N)}{2!}$
4		2m1e1	$⊢ 2 - 1 = 1$
5	4	oveq2i	$⊢ (N - 2) + 2 - 1 = N - 2 + 1$
6		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
7		2cn	$⊢ 2 \in ℂ$
8		ax-1cn	$⊢ 1 \in ℂ$
9		npncan	$⊢ (N \in ℂ \land 2 \in ℂ \land 1 \in ℂ) \to (N - 2) + 2 - 1 = N - 1$
10	7 8 9	mp3an23	$⊢ N \in ℂ \to (N - 2) + 2 - 1 = N - 1$
11	6 10	syl	$⊢ N \in ℕ_{0} \to (N - 2) + 2 - 1 = N - 1$
12	5 11	eqtr3id	$⊢ N \in ℕ_{0} \to N - 2 + 1 = N - 1$
13	12	seqeq1d	$⊢ N \in ℕ_{0} \to seq (N - 2 + 1) (\times I) = seq (N - 1) (\times I)$
14	13	fveq1d	$⊢ N \in ℕ_{0} \to seq (N - 2 + 1) (\times I) (N) = seq (N - 1) (\times I) (N)$
15		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
16		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
17	15 16	syl	$⊢ N \in ℕ_{0} \to N - 1 \in ℤ$
18		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
19	15 18	syl	$⊢ N \in ℕ_{0} \to N \in ℤ_{\geq N}$
20		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
21	6 8 20	sylancl	$⊢ N \in ℕ_{0} \to N - 1 + 1 = N$
22	21	fveq2d	$⊢ N \in ℕ_{0} \to ℤ_{\geq (N - 1 + 1)} = ℤ_{\geq N}$
23	19 22	eleqtrrd	$⊢ N \in ℕ_{0} \to N \in ℤ_{\geq (N - 1 + 1)}$
24		seqm1	$⊢ (N - 1 \in ℤ \land N \in ℤ_{\geq (N - 1 + 1)}) \to seq (N - 1) (\times I) (N) = seq (N - 1) (\times I) (N - 1) I (N)$
25	17 23 24	syl2anc	$⊢ N \in ℕ_{0} \to seq (N - 1) (\times I) (N) = seq (N - 1) (\times I) (N - 1) I (N)$
26		seq1	$⊢ N - 1 \in ℤ \to seq (N - 1) (\times I) (N - 1) = I (N - 1)$
27	17 26	syl	$⊢ N \in ℕ_{0} \to seq (N - 1) (\times I) (N - 1) = I (N - 1)$
28		fvi	$⊢ N - 1 \in ℤ \to I (N - 1) = N - 1$
29	17 28	syl	$⊢ N \in ℕ_{0} \to I (N - 1) = N - 1$
30	27 29	eqtrd	$⊢ N \in ℕ_{0} \to seq (N - 1) (\times I) (N - 1) = N - 1$
31		fvi	$⊢ N \in ℕ_{0} \to I (N) = N$
32	30 31	oveq12d	$⊢ N \in ℕ_{0} \to seq (N - 1) (\times I) (N - 1) I (N) = (N - 1) \cdot N$
33	25 32	eqtrd	$⊢ N \in ℕ_{0} \to seq (N - 1) (\times I) (N) = (N - 1) \cdot N$
34		subcl	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 \in ℂ$
35	6 8 34	sylancl	$⊢ N \in ℕ_{0} \to N - 1 \in ℂ$
36	35 6	mulcomd	$⊢ N \in ℕ_{0} \to (N - 1) \cdot N = N (N - 1)$
37	33 36	eqtrd	$⊢ N \in ℕ_{0} \to seq (N - 1) (\times I) (N) = N (N - 1)$
38	14 37	eqtrd	$⊢ N \in ℕ_{0} \to seq (N - 2 + 1) (\times I) (N) = N (N - 1)$
39		fac2	$⊢ 2! = 2$
40	39	a1i	$⊢ N \in ℕ_{0} \to 2! = 2$
41	38 40	oveq12d	$⊢ N \in ℕ_{0} \to \frac{seq (N - 2 + 1) (\times I) (N)}{2!} = \frac{N (N - 1)}{2}$
42	3 41	eqtrd	$⊢ N \in ℕ_{0} \to (\binom{N}{2}) = \frac{N (N - 1)}{2}$

Metamath Proof Explorer

Theorem bcn2

Proof