bcp1n

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

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

Proof

Step	Hyp	Ref	Expression
1		elfz3nn0	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$
2		facp1	$⊢ N \in ℕ_{0} \to (N + 1)! = N! (N + 1)$
3	1 2	syl	$⊢ K \in (0 \dots N) \to (N + 1)! = N! (N + 1)$
4		fznn0sub	$⊢ K \in (0 \dots N) \to N - K \in ℕ_{0}$
5		facp1	$⊢ N - K \in ℕ_{0} \to (N - K + 1)! = (N - K)! (N - K + 1)$
6	4 5	syl	$⊢ K \in (0 \dots N) \to (N - K + 1)! = (N - K)! (N - K + 1)$
7	1	nn0cnd	$⊢ K \in (0 \dots N) \to N \in ℂ$
8		1cnd	$⊢ K \in (0 \dots N) \to 1 \in ℂ$
9		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
10	9	nn0cnd	$⊢ K \in (0 \dots N) \to K \in ℂ$
11	7 8 10	addsubd	$⊢ K \in (0 \dots N) \to N + 1 - K = N - K + 1$
12	11	fveq2d	$⊢ K \in (0 \dots N) \to (N + 1 - K)! = (N - K + 1)!$
13	11	oveq2d	$⊢ K \in (0 \dots N) \to (N - K)! (N + 1 - K) = (N - K)! (N - K + 1)$
14	6 12 13	3eqtr4d	$⊢ K \in (0 \dots N) \to (N + 1 - K)! = (N - K)! (N + 1 - K)$
15	14	oveq1d	$⊢ K \in (0 \dots N) \to (N + 1 - K)! K! = (N - K)! (N + 1 - K) K!$
16	4	faccld	$⊢ K \in (0 \dots N) \to (N - K)! \in ℕ$
17	16	nncnd	$⊢ K \in (0 \dots N) \to (N - K)! \in ℂ$
18		nn0p1nn	$⊢ N - K \in ℕ_{0} \to N - K + 1 \in ℕ$
19	4 18	syl	$⊢ K \in (0 \dots N) \to N - K + 1 \in ℕ$
20	11 19	eqeltrd	$⊢ K \in (0 \dots N) \to N + 1 - K \in ℕ$
21	20	nncnd	$⊢ K \in (0 \dots N) \to N + 1 - K \in ℂ$
22	9	faccld	$⊢ K \in (0 \dots N) \to K! \in ℕ$
23	22	nncnd	$⊢ K \in (0 \dots N) \to K! \in ℂ$
24	17 21 23	mul32d	$⊢ K \in (0 \dots N) \to (N - K)! (N + 1 - K) K! = (N - K)! K! (N + 1 - K)$
25	15 24	eqtrd	$⊢ K \in (0 \dots N) \to (N + 1 - K)! K! = (N - K)! K! (N + 1 - K)$
26	3 25	oveq12d	$⊢ K \in (0 \dots N) \to \frac{(N + 1)!}{(N + 1 - K)! K!} = \frac{N! (N + 1)}{(N - K)! K! (N + 1 - K)}$
27	1	faccld	$⊢ K \in (0 \dots N) \to N! \in ℕ$
28	27	nncnd	$⊢ K \in (0 \dots N) \to N! \in ℂ$
29		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
30	1 29	syl	$⊢ K \in (0 \dots N) \to N + 1 \in ℕ$
31	30	nncnd	$⊢ K \in (0 \dots N) \to N + 1 \in ℂ$
32	16 22	nnmulcld	$⊢ K \in (0 \dots N) \to (N - K)! K! \in ℕ$
33		nncn	$⊢ (N - K)! K! \in ℕ \to (N - K)! K! \in ℂ$
34		nnne0	$⊢ (N - K)! K! \in ℕ \to (N - K)! K! \neq 0$
35	33 34	jca	$⊢ (N - K)! K! \in ℕ \to ((N - K)! K! \in ℂ \land (N - K)! K! \neq 0)$
36	32 35	syl	$⊢ K \in (0 \dots N) \to ((N - K)! K! \in ℂ \land (N - K)! K! \neq 0)$
37	20	nnne0d	$⊢ K \in (0 \dots N) \to N + 1 - K \neq 0$
38	21 37	jca	$⊢ K \in (0 \dots N) \to (N + 1 - K \in ℂ \land N + 1 - K \neq 0)$
39		divmuldiv	$⊢ ((N! \in ℂ \land N + 1 \in ℂ) \land (((N - K)! K! \in ℂ \land (N - K)! K! \neq 0) \land (N + 1 - K \in ℂ \land N + 1 - K \neq 0))) \to (\frac{N!}{(N - K)! K!}) (\frac{N + 1}{N + 1 - K}) = \frac{N! (N + 1)}{(N - K)! K! (N + 1 - K)}$
40	28 31 36 38 39	syl22anc	$⊢ K \in (0 \dots N) \to (\frac{N!}{(N - K)! K!}) (\frac{N + 1}{N + 1 - K}) = \frac{N! (N + 1)}{(N - K)! K! (N + 1 - K)}$
41	26 40	eqtr4d	$⊢ K \in (0 \dots N) \to \frac{(N + 1)!}{(N + 1 - K)! K!} = (\frac{N!}{(N - K)! K!}) (\frac{N + 1}{N + 1 - K})$
42		fzelp1	$⊢ K \in (0 \dots N) \to K \in (0 \dots N + 1)$
43		bcval2	$⊢ K \in (0 \dots N + 1) \to (\binom{N + 1}{K}) = \frac{(N + 1)!}{(N + 1 - K)! K!}$
44	42 43	syl	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K}) = \frac{(N + 1)!}{(N + 1 - K)! K!}$
45		bcval2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
46	45	oveq1d	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) = (\frac{N!}{(N - K)! K!}) (\frac{N + 1}{N + 1 - K})$
47	41 44 46	3eqtr4d	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K}) = (\binom{N}{K}) (\frac{N + 1}{N + 1 - K})$

Metamath Proof Explorer

Theorem bcp1n

Proof