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	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + ( 𝑁 C 2 ) ) = ( ( 𝑁 + 1 ) C 2 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
2		2z	⊢ 2 ∈ ℤ
3		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℤ ) → ( 𝑁 C 2 ) ∈ ℕ0 )
4	2 3	mpan2	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 2 ) ∈ ℕ0 )
5	4	nn0cnd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 2 ) ∈ ℂ )
6	1 5	addcomd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + ( 𝑁 C 2 ) ) = ( ( 𝑁 C 2 ) + 𝑁 ) )
7		bcn1	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 1 ) = 𝑁 )
8		1e2m1	⊢ 1 = ( 2 − 1 )
9	8	a1i	⊢ ( 𝑁 ∈ ℕ0 → 1 = ( 2 − 1 ) )
10	9	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 1 ) = ( 𝑁 C ( 2 − 1 ) ) )
11	7 10	eqtr3d	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 = ( 𝑁 C ( 2 − 1 ) ) )
12	11	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 C 2 ) + 𝑁 ) = ( ( 𝑁 C 2 ) + ( 𝑁 C ( 2 − 1 ) ) ) )
13		bcpasc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℤ ) → ( ( 𝑁 C 2 ) + ( 𝑁 C ( 2 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 2 ) )
14	2 13	mpan2	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 C 2 ) + ( 𝑁 C ( 2 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 2 ) )
15	6 12 14	3eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + ( 𝑁 C 2 ) ) = ( ( 𝑁 + 1 ) C 2 ) )