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 ( 𝑁 ∈ ℕ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 ) )