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