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	$⊢ (N \in ℕ \land K \in ℤ) \to (\binom{N - 1}{K}) + (\binom{N - 1}{K - 1}) = (\binom{N}{K})$

Step	Hyp	Ref	Expression
1		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
2		bcpasc	$⊢ (N - 1 \in ℕ_{0} \land K \in ℤ) \to (\binom{N - 1}{K}) + (\binom{N - 1}{K - 1}) = (\binom{N - 1 + 1}{K})$
3	1 2	sylan	$⊢ (N \in ℕ \land K \in ℤ) \to (\binom{N - 1}{K}) + (\binom{N - 1}{K - 1}) = (\binom{N - 1 + 1}{K})$
4		nncn	$⊢ N \in ℕ \to N \in ℂ$
5		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
6	4 5	syl	$⊢ N \in ℕ \to N - 1 + 1 = N$
7	6	adantr	$⊢ (N \in ℕ \land K \in ℤ) \to N - 1 + 1 = N$
8	7	oveq1d	$⊢ (N \in ℕ \land K \in ℤ) \to (\binom{N - 1 + 1}{K}) = (\binom{N}{K})$
9	3 8	eqtrd	$⊢ (N \in ℕ \land K \in ℤ) \to (\binom{N - 1}{K}) + (\binom{N - 1}{K - 1}) = (\binom{N}{K})$

Metamath Proof Explorer