bcm1k

Description: The proportion of one binomial coefficient to another with K decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		elfzuz2	$⊢ K \in (1 \dots N) \to N \in ℤ_{\geq 1}$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3	1 2	eleqtrrdi	$⊢ K \in (1 \dots N) \to N \in ℕ$
4	3	nnnn0d	$⊢ K \in (1 \dots N) \to N \in ℕ_{0}$
5	4	faccld	$⊢ K \in (1 \dots N) \to N! \in ℕ$
6	5	nncnd	$⊢ K \in (1 \dots N) \to N! \in ℂ$
7		fznn0sub	$⊢ K \in (1 \dots N) \to N - K \in ℕ_{0}$
8		nn0p1nn	$⊢ N - K \in ℕ_{0} \to N - K + 1 \in ℕ$
9	7 8	syl	$⊢ K \in (1 \dots N) \to N - K + 1 \in ℕ$
10	9	nncnd	$⊢ K \in (1 \dots N) \to N - K + 1 \in ℂ$
11	9	nnnn0d	$⊢ K \in (1 \dots N) \to N - K + 1 \in ℕ_{0}$
12	11	faccld	$⊢ K \in (1 \dots N) \to (N - K + 1)! \in ℕ$
13		elfznn	$⊢ K \in (1 \dots N) \to K \in ℕ$
14		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
15		faccl	$⊢ K - 1 \in ℕ_{0} \to (K - 1)! \in ℕ$
16	13 14 15	3syl	$⊢ K \in (1 \dots N) \to (K - 1)! \in ℕ$
17	12 16	nnmulcld	$⊢ K \in (1 \dots N) \to (N - K + 1)! (K - 1)! \in ℕ$
18		nncn	$⊢ (N - K + 1)! (K - 1)! \in ℕ \to (N - K + 1)! (K - 1)! \in ℂ$
19		nnne0	$⊢ (N - K + 1)! (K - 1)! \in ℕ \to (N - K + 1)! (K - 1)! \neq 0$
20	18 19	jca	$⊢ (N - K + 1)! (K - 1)! \in ℕ \to ((N - K + 1)! (K - 1)! \in ℂ \land (N - K + 1)! (K - 1)! \neq 0)$
21	17 20	syl	$⊢ K \in (1 \dots N) \to ((N - K + 1)! (K - 1)! \in ℂ \land (N - K + 1)! (K - 1)! \neq 0)$
22	13	nncnd	$⊢ K \in (1 \dots N) \to K \in ℂ$
23	13	nnne0d	$⊢ K \in (1 \dots N) \to K \neq 0$
24	22 23	jca	$⊢ K \in (1 \dots N) \to (K \in ℂ \land K \neq 0)$
25		divmuldiv	$⊢ ((N! \in ℂ \land N - K + 1 \in ℂ) \land (((N - K + 1)! (K - 1)! \in ℂ \land (N - K + 1)! (K - 1)! \neq 0) \land (K \in ℂ \land K \neq 0))) \to (\frac{N!}{(N - K + 1)! (K - 1)!}) (\frac{N - K + 1}{K}) = \frac{N! (N - K + 1)}{(N - K + 1)! (K - 1)! K}$
26	6 10 21 24 25	syl22anc	$⊢ K \in (1 \dots N) \to (\frac{N!}{(N - K + 1)! (K - 1)!}) (\frac{N - K + 1}{K}) = \frac{N! (N - K + 1)}{(N - K + 1)! (K - 1)! K}$
27		elfzel2	$⊢ K \in (1 \dots N) \to N \in ℤ$
28	27	zcnd	$⊢ K \in (1 \dots N) \to N \in ℂ$
29		1cnd	$⊢ K \in (1 \dots N) \to 1 \in ℂ$
30	28 22 29	subsubd	$⊢ K \in (1 \dots N) \to N - (K - 1) = N - K + 1$
31	30	fveq2d	$⊢ K \in (1 \dots N) \to (N - (K - 1))! = (N - K + 1)!$
32	31	oveq1d	$⊢ K \in (1 \dots N) \to (N - (K - 1))! (K - 1)! = (N - K + 1)! (K - 1)!$
33	32	oveq2d	$⊢ K \in (1 \dots N) \to \frac{N!}{(N - (K - 1))! (K - 1)!} = \frac{N!}{(N - K + 1)! (K - 1)!}$
34	30	oveq1d	$⊢ K \in (1 \dots N) \to \frac{N - (K - 1)}{K} = \frac{N - K + 1}{K}$
35	33 34	oveq12d	$⊢ K \in (1 \dots N) \to (\frac{N!}{(N - (K - 1))! (K - 1)!}) (\frac{N - (K - 1)}{K}) = (\frac{N!}{(N - K + 1)! (K - 1)!}) (\frac{N - K + 1}{K})$
36		facp1	$⊢ N - K \in ℕ_{0} \to (N - K + 1)! = (N - K)! (N - K + 1)$
37	7 36	syl	$⊢ K \in (1 \dots N) \to (N - K + 1)! = (N - K)! (N - K + 1)$
38	37	eqcomd	$⊢ K \in (1 \dots N) \to (N - K)! (N - K + 1) = (N - K + 1)!$
39		facnn2	$⊢ K \in ℕ \to K! = (K - 1)! K$
40	13 39	syl	$⊢ K \in (1 \dots N) \to K! = (K - 1)! K$
41	38 40	oveq12d	$⊢ K \in (1 \dots N) \to (N - K)! (N - K + 1) K! = (N - K + 1)! (K - 1)! K$
42	7	faccld	$⊢ K \in (1 \dots N) \to (N - K)! \in ℕ$
43	42	nncnd	$⊢ K \in (1 \dots N) \to (N - K)! \in ℂ$
44	13	nnnn0d	$⊢ K \in (1 \dots N) \to K \in ℕ_{0}$
45	44	faccld	$⊢ K \in (1 \dots N) \to K! \in ℕ$
46	45	nncnd	$⊢ K \in (1 \dots N) \to K! \in ℂ$
47	43 46 10	mul32d	$⊢ K \in (1 \dots N) \to (N - K)! K! (N - K + 1) = (N - K)! (N - K + 1) K!$
48	12	nncnd	$⊢ K \in (1 \dots N) \to (N - K + 1)! \in ℂ$
49	16	nncnd	$⊢ K \in (1 \dots N) \to (K - 1)! \in ℂ$
50	48 49 22	mulassd	$⊢ K \in (1 \dots N) \to (N - K + 1)! (K - 1)! K = (N - K + 1)! (K - 1)! K$
51	41 47 50	3eqtr4d	$⊢ K \in (1 \dots N) \to (N - K)! K! (N - K + 1) = (N - K + 1)! (K - 1)! K$
52	51	oveq2d	$⊢ K \in (1 \dots N) \to \frac{N! (N - K + 1)}{(N - K)! K! (N - K + 1)} = \frac{N! (N - K + 1)}{(N - K + 1)! (K - 1)! K}$
53	26 35 52	3eqtr4d	$⊢ K \in (1 \dots N) \to (\frac{N!}{(N - (K - 1))! (K - 1)!}) (\frac{N - (K - 1)}{K}) = \frac{N! (N - K + 1)}{(N - K)! K! (N - K + 1)}$
54	6 10	mulcomd	$⊢ K \in (1 \dots N) \to N! (N - K + 1) = (N - K + 1) N!$
55	42 45	nnmulcld	$⊢ K \in (1 \dots N) \to (N - K)! K! \in ℕ$
56	55	nncnd	$⊢ K \in (1 \dots N) \to (N - K)! K! \in ℂ$
57	56 10	mulcomd	$⊢ K \in (1 \dots N) \to (N - K)! K! (N - K + 1) = (N - K + 1) (N - K)! K!$
58	54 57	oveq12d	$⊢ K \in (1 \dots N) \to \frac{N! (N - K + 1)}{(N - K)! K! (N - K + 1)} = \frac{(N - K + 1) N!}{(N - K + 1) (N - K)! K!}$
59	55	nnne0d	$⊢ K \in (1 \dots N) \to (N - K)! K! \neq 0$
60	9	nnne0d	$⊢ K \in (1 \dots N) \to N - K + 1 \neq 0$
61	6 56 10 59 60	divcan5d	$⊢ K \in (1 \dots N) \to \frac{(N - K + 1) N!}{(N - K + 1) (N - K)! K!} = \frac{N!}{(N - K)! K!}$
62	53 58 61	3eqtrrd	$⊢ K \in (1 \dots N) \to \frac{N!}{(N - K)! K!} = (\frac{N!}{(N - (K - 1))! (K - 1)!}) (\frac{N - (K - 1)}{K})$
63		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
64	63	sseli	$⊢ K \in (1 \dots N) \to K \in (0 \dots N)$
65		bcval2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
66	64 65	syl	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
67		ax-1cn	$⊢ 1 \in ℂ$
68		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
69	28 67 68	sylancl	$⊢ K \in (1 \dots N) \to N - 1 + 1 = N$
70		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
71		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
72		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
73	27 70 71 72	4syl	$⊢ K \in (1 \dots N) \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
74	69 73	eqeltrrd	$⊢ K \in (1 \dots N) \to N \in ℤ_{\geq (N - 1)}$
75		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (0 \dots N - 1) \subseteq (0 \dots N)$
76	74 75	syl	$⊢ K \in (1 \dots N) \to (0 \dots N - 1) \subseteq (0 \dots N)$
77		elfzmlbm	$⊢ K \in (1 \dots N) \to K - 1 \in (0 \dots N - 1)$
78	76 77	sseldd	$⊢ K \in (1 \dots N) \to K - 1 \in (0 \dots N)$
79		bcval2	$⊢ K - 1 \in (0 \dots N) \to (\binom{N}{K - 1}) = \frac{N!}{(N - (K - 1))! (K - 1)!}$
80	78 79	syl	$⊢ K \in (1 \dots N) \to (\binom{N}{K - 1}) = \frac{N!}{(N - (K - 1))! (K - 1)!}$
81	80	oveq1d	$⊢ K \in (1 \dots N) \to (\binom{N}{K - 1}) (\frac{N - (K - 1)}{K}) = (\frac{N!}{(N - (K - 1))! (K - 1)!}) (\frac{N - (K - 1)}{K})$
82	62 66 81	3eqtr4d	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) = (\binom{N}{K - 1}) (\frac{N - (K - 1)}{K})$

Metamath Proof Explorer

Theorem bcm1k

Proof