bcp1nk

Description: The proportion of one binomial coefficient to another with N and K increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Assertion	bcp1nk	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K + 1}) = (\binom{N}{K}) (\frac{N + 1}{K + 1})$

Proof

Step	Hyp	Ref	Expression
1		elfzel1	$⊢ K \in (0 \dots N) \to 0 \in ℤ$
2		elfzel2	$⊢ K \in (0 \dots N) \to N \in ℤ$
3		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
4		1zzd	$⊢ K \in (0 \dots N) \to 1 \in ℤ$
5		fzaddel	$⊢ ((0 \in ℤ \land N \in ℤ) \land (K \in ℤ \land 1 \in ℤ)) \to (K \in (0 \dots N) \leftrightarrow K + 1 \in (0 + 1 \dots N + 1))$
6	1 2 3 4 5	syl22anc	$⊢ K \in (0 \dots N) \to (K \in (0 \dots N) \leftrightarrow K + 1 \in (0 + 1 \dots N + 1))$
7	6	ibi	$⊢ K \in (0 \dots N) \to K + 1 \in (0 + 1 \dots N + 1)$
8		1e0p1	$⊢ 1 = 0 + 1$
9	8	oveq1i	$⊢ (1 \dots N + 1) = (0 + 1 \dots N + 1)$
10	7 9	eleqtrrdi	$⊢ K \in (0 \dots N) \to K + 1 \in (1 \dots N + 1)$
11		bcm1k	$⊢ K + 1 \in (1 \dots N + 1) \to (\binom{N + 1}{K + 1}) = (\binom{N + 1}{K + 1 - 1}) (\frac{N + 1 - (K + 1 - 1)}{K + 1})$
12	10 11	syl	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K + 1}) = (\binom{N + 1}{K + 1 - 1}) (\frac{N + 1 - (K + 1 - 1)}{K + 1})$
13	3	zcnd	$⊢ K \in (0 \dots N) \to K \in ℂ$
14		ax-1cn	$⊢ 1 \in ℂ$
15		pncan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K + 1 - 1 = K$
16	13 14 15	sylancl	$⊢ K \in (0 \dots N) \to K + 1 - 1 = K$
17	16	oveq2d	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K + 1 - 1}) = (\binom{N + 1}{K})$
18		bcp1n	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K}) = (\binom{N}{K}) (\frac{N + 1}{N + 1 - K})$
19	17 18	eqtrd	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K + 1 - 1}) = (\binom{N}{K}) (\frac{N + 1}{N + 1 - K})$
20	16	oveq2d	$⊢ K \in (0 \dots N) \to N + 1 - (K + 1 - 1) = N + 1 - K$
21	20	oveq1d	$⊢ K \in (0 \dots N) \to \frac{N + 1 - (K + 1 - 1)}{K + 1} = \frac{N + 1 - K}{K + 1}$
22	19 21	oveq12d	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K + 1 - 1}) (\frac{N + 1 - (K + 1 - 1)}{K + 1}) = (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) (\frac{N + 1 - K}{K + 1})$
23		bcrpcl	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℝ^{+}$
24	23	rpcnd	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℂ$
25	2	peano2zd	$⊢ K \in (0 \dots N) \to N + 1 \in ℤ$
26	25	zred	$⊢ K \in (0 \dots N) \to N + 1 \in ℝ$
27	3	zred	$⊢ K \in (0 \dots N) \to K \in ℝ$
28	2	zred	$⊢ K \in (0 \dots N) \to N \in ℝ$
29		elfzle2	$⊢ K \in (0 \dots N) \to K \leq N$
30	28	ltp1d	$⊢ K \in (0 \dots N) \to N < N + 1$
31	27 28 26 29 30	lelttrd	$⊢ K \in (0 \dots N) \to K < N + 1$
32		znnsub	$⊢ (K \in ℤ \land N + 1 \in ℤ) \to (K < N + 1 \leftrightarrow N + 1 - K \in ℕ)$
33	3 25 32	syl2anc	$⊢ K \in (0 \dots N) \to (K < N + 1 \leftrightarrow N + 1 - K \in ℕ)$
34	31 33	mpbid	$⊢ K \in (0 \dots N) \to N + 1 - K \in ℕ$
35	26 34	nndivred	$⊢ K \in (0 \dots N) \to \frac{N + 1}{N + 1 - K} \in ℝ$
36	35	recnd	$⊢ K \in (0 \dots N) \to \frac{N + 1}{N + 1 - K} \in ℂ$
37	34	nnred	$⊢ K \in (0 \dots N) \to N + 1 - K \in ℝ$
38		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
39		nn0p1nn	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ$
40	38 39	syl	$⊢ K \in (0 \dots N) \to K + 1 \in ℕ$
41	37 40	nndivred	$⊢ K \in (0 \dots N) \to \frac{N + 1 - K}{K + 1} \in ℝ$
42	41	recnd	$⊢ K \in (0 \dots N) \to \frac{N + 1 - K}{K + 1} \in ℂ$
43	24 36 42	mulassd	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) (\frac{N + 1 - K}{K + 1}) = (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) (\frac{N + 1 - K}{K + 1})$
44	25	zcnd	$⊢ K \in (0 \dots N) \to N + 1 \in ℂ$
45	34	nncnd	$⊢ K \in (0 \dots N) \to N + 1 - K \in ℂ$
46	40	nncnd	$⊢ K \in (0 \dots N) \to K + 1 \in ℂ$
47	34	nnne0d	$⊢ K \in (0 \dots N) \to N + 1 - K \neq 0$
48	40	nnne0d	$⊢ K \in (0 \dots N) \to K + 1 \neq 0$
49	44 45 46 47 48	dmdcan2d	$⊢ K \in (0 \dots N) \to (\frac{N + 1}{N + 1 - K}) (\frac{N + 1 - K}{K + 1}) = \frac{N + 1}{K + 1}$
50	49	oveq2d	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) (\frac{N + 1 - K}{K + 1}) = (\binom{N}{K}) (\frac{N + 1}{K + 1})$
51	43 50	eqtrd	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) (\frac{N + 1 - K}{K + 1}) = (\binom{N}{K}) (\frac{N + 1}{K + 1})$
52	22 51	eqtrd	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K + 1 - 1}) (\frac{N + 1 - (K + 1 - 1)}{K + 1}) = (\binom{N}{K}) (\frac{N + 1}{K + 1})$
53	12 52	eqtrd	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K + 1}) = (\binom{N}{K}) (\frac{N + 1}{K + 1})$

Metamath Proof Explorer

Theorem bcp1nk

Proof