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