bcm1n

Description: The proportion of one binomial coefficient to another with N decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016)

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

Proof

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		nnz	$⊢ N \in ℕ \to N \in ℤ$
3	2	zcnd	$⊢ N \in ℕ \to N \in ℂ$
4	3	adantl	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N \in ℂ$
5		1cnd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to 1 \in ℂ$
6	4 5	npcand	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N - 1 + 1 = N$
7	6	oveq1d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N - 1 + 1}{K}) = (\binom{N}{K})$
8	6	oveq1d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (N - 1) + 1 - K = N - K$
9	6 8	oveq12d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to \frac{N - 1 + 1}{(N - 1) + 1 - K} = \frac{N}{N - K}$
10	9	oveq2d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N - 1}{K}) (\frac{N - 1 + 1}{(N - 1) + 1 - K}) = (\binom{N - 1}{K}) (\frac{N}{N - K})$
11	7 10	eqeq12d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to ((\binom{N - 1 + 1}{K}) = (\binom{N - 1}{K}) (\frac{N - 1 + 1}{(N - 1) + 1 - K}) \leftrightarrow (\binom{N}{K}) = (\binom{N - 1}{K}) (\frac{N}{N - K}))$
12	1 11	syl5ib	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (K \in (0 \dots N - 1) \to (\binom{N}{K}) = (\binom{N - 1}{K}) (\frac{N}{N - K}))$
13	12	3impia	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ \land K \in (0 \dots N - 1)) \to (\binom{N}{K}) = (\binom{N - 1}{K}) (\frac{N}{N - K})$
14	13	3anidm13	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N}{K}) = (\binom{N - 1}{K}) (\frac{N}{N - K})$
15		elfznn0	$⊢ K \in (0 \dots N - 1) \to K \in ℕ_{0}$
16	15	adantr	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K \in ℕ_{0}$
17		simpr	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N \in ℕ$
18	17	nnnn0d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N \in ℕ_{0}$
19		elfzelz	$⊢ K \in (0 \dots N - 1) \to K \in ℤ$
20	19	adantr	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K \in ℤ$
21	20	zred	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K \in ℝ$
22	2	adantl	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N \in ℤ$
23	22	zred	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N \in ℝ$
24		elfzle2	$⊢ K \in (0 \dots N - 1) \to K \leq N - 1$
25	24	adantr	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K \leq N - 1$
26		zltlem1	$⊢ (K \in ℤ \land N \in ℤ) \to (K < N \leftrightarrow K \leq N - 1)$
27	19 2 26	syl2an	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (K < N \leftrightarrow K \leq N - 1)$
28	25 27	mpbird	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K < N$
29	21 23 28	ltled	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K \leq N$
30		elfz2nn0	$⊢ K \in (0 \dots N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)$
31	16 18 29 30	syl3anbrc	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K \in (0 \dots N)$
32		bcrpcl	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℝ^{+}$
33	31 32	syl	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N}{K}) \in ℝ^{+}$
34	33	rpcnd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N}{K}) \in ℂ$
35	19	zcnd	$⊢ K \in (0 \dots N - 1) \to K \in ℂ$
36	35	adantr	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K \in ℂ$
37	4 36	subcld	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N - K \in ℂ$
38	36 4	negsubdi2d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to - (K - N) = N - K$
39	21 23	resubcld	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K - N \in ℝ$
40	39	recnd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K - N \in ℂ$
41	4	addid2d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to 0 + N = N$
42	28 41	breqtrrd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K < 0 + N$
43		0red	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to 0 \in ℝ$
44	21 23 43	ltsubaddd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (K - N < 0 \leftrightarrow K < 0 + N)$
45	42 44	mpbird	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K - N < 0$
46	45	lt0ne0d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to K - N \neq 0$
47	40 46	negne0d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to - (K - N) \neq 0$
48	38 47	eqnetrrd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N - K \neq 0$
49	4 37 48	divcld	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to \frac{N}{N - K} \in ℂ$
50		bcrpcl	$⊢ K \in (0 \dots N - 1) \to (\binom{N - 1}{K}) \in ℝ^{+}$
51	50	adantr	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N - 1}{K}) \in ℝ^{+}$
52	51	rpcnne0d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to ((\binom{N - 1}{K}) \in ℂ \land (\binom{N - 1}{K}) \neq 0)$
53		divmul2	$⊢ ((\binom{N}{K}) \in ℂ \land \frac{N}{N - K} \in ℂ \land ((\binom{N - 1}{K}) \in ℂ \land (\binom{N - 1}{K}) \neq 0)) \to (\frac{(\binom{N}{K})}{(\binom{N - 1}{K})} = \frac{N}{N - K} \leftrightarrow (\binom{N}{K}) = (\binom{N - 1}{K}) (\frac{N}{N - K}))$
54	34 49 52 53	syl3anc	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\frac{(\binom{N}{K})}{(\binom{N - 1}{K})} = \frac{N}{N - K} \leftrightarrow (\binom{N}{K}) = (\binom{N - 1}{K}) (\frac{N}{N - K}))$
55	14 54	mpbird	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to \frac{(\binom{N}{K})}{(\binom{N - 1}{K})} = \frac{N}{N - K}$
56	55	oveq2d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to \frac{1}{\frac{(\binom{N}{K})}{(\binom{N - 1}{K})}} = \frac{1}{\frac{N}{N - K}}$
57	51	rpcnd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N - 1}{K}) \in ℂ$
58		bccl2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℕ$
59	31 58	syl	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N}{K}) \in ℕ$
60	59	nnne0d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N}{K}) \neq 0$
61		bccl2	$⊢ K \in (0 \dots N - 1) \to (\binom{N - 1}{K}) \in ℕ$
62	61	nnne0d	$⊢ K \in (0 \dots N - 1) \to (\binom{N - 1}{K}) \neq 0$
63	62	adantr	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to (\binom{N - 1}{K}) \neq 0$
64	34 57 60 63	recdivd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to \frac{1}{\frac{(\binom{N}{K})}{(\binom{N - 1}{K})}} = \frac{(\binom{N - 1}{K})}{(\binom{N}{K})}$
65	17	nnne0d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to N \neq 0$
66	4 37 65 48	recdivd	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to \frac{1}{\frac{N}{N - K}} = \frac{N - K}{N}$
67	56 64 66	3eqtr3d	$⊢ (K \in (0 \dots N - 1) \land N \in ℕ) \to \frac{(\binom{N - 1}{K})}{(\binom{N}{K})} = \frac{N - K}{N}$

Metamath Proof Explorer

Theorem bcm1n

Proof