bcn2m1

Description: Compute the binomial coefficient " N choose 2 " from " ( N - 1 ) choose 2 ": (N-1) + ( (N-1) 2 ) = ( N 2 ). (Contributed by Alexander van der Vekens, 7-Jan-2018)

		Ref	Expression
	Assertion	bcn2m1	$⊢ N \in ℕ \to N - 1 + (\binom{N - 1}{2}) = (\binom{N}{2})$

Proof

Step	Hyp	Ref	Expression
1		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
2	1	nn0cnd	$⊢ N \in ℕ \to N - 1 \in ℂ$
3		2z	$⊢ 2 \in ℤ$
4		bccl	$⊢ (N - 1 \in ℕ_{0} \land 2 \in ℤ) \to (\binom{N - 1}{2}) \in ℕ_{0}$
5	1 3 4	sylancl	$⊢ N \in ℕ \to (\binom{N - 1}{2}) \in ℕ_{0}$
6	5	nn0cnd	$⊢ N \in ℕ \to (\binom{N - 1}{2}) \in ℂ$
7	2 6	addcomd	$⊢ N \in ℕ \to N - 1 + (\binom{N - 1}{2}) = (\binom{N - 1}{2}) + N - 1$
8		bcn1	$⊢ N - 1 \in ℕ_{0} \to (\binom{N - 1}{1}) = N - 1$
9	8	eqcomd	$⊢ N - 1 \in ℕ_{0} \to N - 1 = (\binom{N - 1}{1})$
10	1 9	syl	$⊢ N \in ℕ \to N - 1 = (\binom{N - 1}{1})$
11		1e2m1	$⊢ 1 = 2 - 1$
12	11	a1i	$⊢ N \in ℕ \to 1 = 2 - 1$
13	12	oveq2d	$⊢ N \in ℕ \to (\binom{N - 1}{1}) = (\binom{N - 1}{2 - 1})$
14	10 13	eqtrd	$⊢ N \in ℕ \to N - 1 = (\binom{N - 1}{2 - 1})$
15	14	oveq2d	$⊢ N \in ℕ \to (\binom{N - 1}{2}) + N - 1 = (\binom{N - 1}{2}) + (\binom{N - 1}{2 - 1})$
16		bcpasc	$⊢ (N - 1 \in ℕ_{0} \land 2 \in ℤ) \to (\binom{N - 1}{2}) + (\binom{N - 1}{2 - 1}) = (\binom{N - 1 + 1}{2})$
17	1 3 16	sylancl	$⊢ N \in ℕ \to (\binom{N - 1}{2}) + (\binom{N - 1}{2 - 1}) = (\binom{N - 1 + 1}{2})$
18		nncn	$⊢ N \in ℕ \to N \in ℂ$
19		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
20	18 19	npcand	$⊢ N \in ℕ \to N - 1 + 1 = N$
21	20	oveq1d	$⊢ N \in ℕ \to (\binom{N - 1 + 1}{2}) = (\binom{N}{2})$
22	17 21	eqtrd	$⊢ N \in ℕ \to (\binom{N - 1}{2}) + (\binom{N - 1}{2 - 1}) = (\binom{N}{2})$
23	7 15 22	3eqtrd	$⊢ N \in ℕ \to N - 1 + (\binom{N - 1}{2}) = (\binom{N}{2})$

Metamath Proof Explorer

Theorem bcn2m1

Proof