This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bcn2p1

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

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

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
2		2z	$⊢ 2 \in ℤ$
3		bccl	$⊢ (N \in ℕ_{0} \land 2 \in ℤ) \to (\binom{N}{2}) \in ℕ_{0}$
4	2 3	mpan2	$⊢ N \in ℕ_{0} \to (\binom{N}{2}) \in ℕ_{0}$
5	4	nn0cnd	$⊢ N \in ℕ_{0} \to (\binom{N}{2}) \in ℂ$
6	1 5	addcomd	$⊢ N \in ℕ_{0} \to N + (\binom{N}{2}) = (\binom{N}{2}) + N$
7		bcn1	$⊢ N \in ℕ_{0} \to (\binom{N}{1}) = N$
8		1e2m1	$⊢ 1 = 2 - 1$
9	8	a1i	$⊢ N \in ℕ_{0} \to 1 = 2 - 1$
10	9	oveq2d	$⊢ N \in ℕ_{0} \to (\binom{N}{1}) = (\binom{N}{2 - 1})$
11	7 10	eqtr3d	$⊢ N \in ℕ_{0} \to N = (\binom{N}{2 - 1})$
12	11	oveq2d	$⊢ N \in ℕ_{0} \to (\binom{N}{2}) + N = (\binom{N}{2}) + (\binom{N}{2 - 1})$
13		bcpasc	$⊢ (N \in ℕ_{0} \land 2 \in ℤ) \to (\binom{N}{2}) + (\binom{N}{2 - 1}) = (\binom{N + 1}{2})$
14	2 13	mpan2	$⊢ N \in ℕ_{0} \to (\binom{N}{2}) + (\binom{N}{2 - 1}) = (\binom{N + 1}{2})$
15	6 12 14	3eqtrd	$⊢ N \in ℕ_{0} \to N + (\binom{N}{2}) = (\binom{N + 1}{2})$