bcm1nt

Description: The proportion of one binomial coefficient to another with N decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020)

		Ref	Expression
	Assertion	bcm1nt	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to (\binom{N}{K}) = (\binom{N - 1}{K}) (\frac{N}{N - K})$

Step	Hyp	Ref	Expression
1		bcp1n	$⊢ K \in (0 \dots N - 1) \to (\binom{N - 1 + 1}{K}) = (\binom{N - 1}{K}) (\frac{N - 1 + 1}{(N - 1) + 1 - K})$
2	1	adantl	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to (\binom{N - 1 + 1}{K}) = (\binom{N - 1}{K}) (\frac{N - 1 + 1}{(N - 1) + 1 - K})$
3		simpl	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to N \in ℕ$
4	3	nncnd	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to N \in ℂ$
5		1cnd	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to 1 \in ℂ$
6	4 5	npcand	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to N - 1 + 1 = N$
7	6	oveq1d	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to (\binom{N - 1 + 1}{K}) = (\binom{N}{K})$
8	6	oveq1d	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to (N - 1) + 1 - K = N - K$
9	6 8	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to \frac{N - 1 + 1}{(N - 1) + 1 - K} = \frac{N}{N - K}$
10	9	oveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to (\binom{N - 1}{K}) (\frac{N - 1 + 1}{(N - 1) + 1 - K}) = (\binom{N - 1}{K}) (\frac{N}{N - K})$
11	2 7 10	3eqtr3d	$⊢ (N \in ℕ \land K \in (0 \dots N - 1)) \to (\binom{N}{K}) = (\binom{N - 1}{K}) (\frac{N}{N - K})$

Metamath Proof Explorer