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 ) )