Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
2 1 nn0cnd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
3 2z ⊢ 2 ∈ ℤ
4 bccl ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ 2 ∈ ℤ ) → ( ( 𝑁 − 1 ) C 2 ) ∈ ℕ0 )
5 1 3 4 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) C 2 ) ∈ ℕ0 )
6 5 nn0cnd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) C 2 ) ∈ ℂ )
7 2 6 addcomd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + ( ( 𝑁 − 1 ) C 2 ) ) = ( ( ( 𝑁 − 1 ) C 2 ) + ( 𝑁 − 1 ) ) )
8 bcn1 ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ( 𝑁 − 1 ) C 1 ) = ( 𝑁 − 1 ) )
9 8 eqcomd ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( 𝑁 − 1 ) = ( ( 𝑁 − 1 ) C 1 ) )
10 1 9 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) = ( ( 𝑁 − 1 ) C 1 ) )
11 1e2m1 ⊢ 1 = ( 2 − 1 )
12 11 a1i ⊢ ( 𝑁 ∈ ℕ → 1 = ( 2 − 1 ) )
13 12 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) C 1 ) = ( ( 𝑁 − 1 ) C ( 2 − 1 ) ) )
14 10 13 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) = ( ( 𝑁 − 1 ) C ( 2 − 1 ) ) )
15 14 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) C 2 ) + ( 𝑁 − 1 ) ) = ( ( ( 𝑁 − 1 ) C 2 ) + ( ( 𝑁 − 1 ) C ( 2 − 1 ) ) ) )
16 bcpasc ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ 2 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) C 2 ) + ( ( 𝑁 − 1 ) C ( 2 − 1 ) ) ) = ( ( ( 𝑁 − 1 ) + 1 ) C 2 ) )
17 1 3 16 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) C 2 ) + ( ( 𝑁 − 1 ) C ( 2 − 1 ) ) ) = ( ( ( 𝑁 − 1 ) + 1 ) C 2 ) )
18 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
19 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
20 18 19 npcand ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
21 20 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) + 1 ) C 2 ) = ( 𝑁 C 2 ) )
22 17 21 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) C 2 ) + ( ( 𝑁 − 1 ) C ( 2 − 1 ) ) ) = ( 𝑁 C 2 ) )
23 7 15 22 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + ( ( 𝑁 − 1 ) C 2 ) ) = ( 𝑁 C 2 ) )