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

Metamath Proof Explorer

Theorem bcp1m1

Description: Compute the binomial coefficient of ( N + 1 ) over ( N - 1 ) (Contributed by Scott Fenton, 11-May-2014) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion bcp1m1 ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( 𝑁 − 1 ) ) = ( ( ( 𝑁 + 1 ) · 𝑁 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
2 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
3 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
4 2 3 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℤ )
5 bccmpl ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( ( 𝑁 + 1 ) C ( 𝑁 − 1 ) ) = ( ( 𝑁 + 1 ) C ( ( 𝑁 + 1 ) − ( 𝑁 − 1 ) ) ) )
6 1 4 5 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( 𝑁 − 1 ) ) = ( ( 𝑁 + 1 ) C ( ( 𝑁 + 1 ) − ( 𝑁 − 1 ) ) ) )
7 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
8 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
9 7 8 8 pnncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − ( 𝑁 − 1 ) ) = ( 1 + 1 ) )
10 df-2 ⊢ 2 = ( 1 + 1 )
11 9 10 eqtr4di ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − ( 𝑁 − 1 ) ) = 2 )
12 11 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( ( 𝑁 + 1 ) − ( 𝑁 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 2 ) )
13 bcn2 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) C 2 ) = ( ( ( 𝑁 + 1 ) · ( ( 𝑁 + 1 ) − 1 ) ) / 2 ) )
14 1 13 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C 2 ) = ( ( ( 𝑁 + 1 ) · ( ( 𝑁 + 1 ) − 1 ) ) / 2 ) )
15 ax-1cn ⊢ 1 ∈ ℂ
16 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
17 7 15 16 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
18 17 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) · ( ( 𝑁 + 1 ) − 1 ) ) = ( ( 𝑁 + 1 ) · 𝑁 ) )
19 18 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) · ( ( 𝑁 + 1 ) − 1 ) ) / 2 ) = ( ( ( 𝑁 + 1 ) · 𝑁 ) / 2 ) )
20 14 19 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C 2 ) = ( ( ( 𝑁 + 1 ) · 𝑁 ) / 2 ) )
21 12 20 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( ( 𝑁 + 1 ) − ( 𝑁 − 1 ) ) ) = ( ( ( 𝑁 + 1 ) · 𝑁 ) / 2 ) )
22 6 21 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( 𝑁 − 1 ) ) = ( ( ( 𝑁 + 1 ) · 𝑁 ) / 2 ) )