Theorem bcpascm1

Description: Pascal's rule for the binomial coefficient, generalized to all integers K , shifted down by 1. (Contributed by AV, 8-Sep-2019)

	Ref	Expression
Assertion	bcpascm1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) + ( ( 𝑁 − 1 ) C ( 𝐾 − 1 ) ) ) = ( 𝑁 C 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
2		bcpasc	⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) + ( ( 𝑁 − 1 ) C ( 𝐾 − 1 ) ) ) = ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) )
3	1 2	sylan	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) + ( ( 𝑁 − 1 ) C ( 𝐾 − 1 ) ) ) = ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) )
4		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
5		npcan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
6	4 5	syl	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
7	6	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
8	7	oveq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( 𝑁 C 𝐾 ) )
9	3 8	eqtrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) + ( ( 𝑁 − 1 ) C ( 𝐾 − 1 ) ) ) = ( 𝑁 C 𝐾 ) )