bccp1k

Description: Generalized binomial coefficient: C choose ( K + 1 ) . (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	bccval.c	$⊢ φ \to C \in ℂ$
	bccval.k	$⊢ φ \to K \in ℕ_{0}$
Assertion	bccp1k	$⊢ φ \to C C_{𝑐} (K + 1) = (C C_{𝑐} K) (\frac{C - K}{K + 1})$

Proof

Step	Hyp	Ref	Expression
1		bccval.c	$⊢ φ \to C \in ℂ$
2		bccval.k	$⊢ φ \to K \in ℕ_{0}$
3		fallfacp1	$⊢ (C \in ℂ \land K \in ℕ_{0}) \to C^{\underline{(K + 1)}} = (C^{\underline{K}}) (C - K)$
4	1 2 3	syl2anc	$⊢ φ \to C^{\underline{(K + 1)}} = (C^{\underline{K}}) (C - K)$
5		facp1	$⊢ K \in ℕ_{0} \to (K + 1)! = K! (K + 1)$
6	2 5	syl	$⊢ φ \to (K + 1)! = K! (K + 1)$
7	4 6	oveq12d	$⊢ φ \to \frac{C^{\underline{(K + 1)}}}{(K + 1)!} = \frac{(C^{\underline{K}}) (C - K)}{K! (K + 1)}$
8		peano2nn0	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ_{0}$
9	2 8	syl	$⊢ φ \to K + 1 \in ℕ_{0}$
10	1 9	bccval	$⊢ φ \to C C_{𝑐} (K + 1) = \frac{C^{\underline{(K + 1)}}}{(K + 1)!}$
11		fallfaccl	$⊢ (C \in ℂ \land K \in ℕ_{0}) \to C^{\underline{K}} \in ℂ$
12	1 2 11	syl2anc	$⊢ φ \to C^{\underline{K}} \in ℂ$
13		faccl	$⊢ K \in ℕ_{0} \to K! \in ℕ$
14	2 13	syl	$⊢ φ \to K! \in ℕ$
15	14	nncnd	$⊢ φ \to K! \in ℂ$
16	2	nn0cnd	$⊢ φ \to K \in ℂ$
17	1 16	subcld	$⊢ φ \to C - K \in ℂ$
18	9	nn0cnd	$⊢ φ \to K + 1 \in ℂ$
19	14	nnne0d	$⊢ φ \to K! \neq 0$
20		nn0p1nn	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ$
21	2 20	syl	$⊢ φ \to K + 1 \in ℕ$
22	21	nnne0d	$⊢ φ \to K + 1 \neq 0$
23	12 15 17 18 19 22	divmuldivd	$⊢ φ \to (\frac{C^{\underline{K}}}{K!}) (\frac{C - K}{K + 1}) = \frac{(C^{\underline{K}}) (C - K)}{K! (K + 1)}$
24	7 10 23	3eqtr4d	$⊢ φ \to C C_{𝑐} (K + 1) = (\frac{C^{\underline{K}}}{K!}) (\frac{C - K}{K + 1})$
25	1 2	bccval	$⊢ φ \to C C_{𝑐} K = \frac{C^{\underline{K}}}{K!}$
26	25	oveq1d	$⊢ φ \to (C C_{𝑐} K) (\frac{C - K}{K + 1}) = (\frac{C^{\underline{K}}}{K!}) (\frac{C - K}{K + 1})$
27	24 26	eqtr4d	$⊢ φ \to C C_{𝑐} (K + 1) = (C C_{𝑐} K) (\frac{C - K}{K + 1})$

Metamath Proof Explorer

Theorem bccp1k

Proof