Theorem bccval

Description: Value of the generalized binomial coefficient, C choose K . (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	bccval.c	$$⊢\phi \to C\in ℂ$$
	bccval.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
Assertion	bccval	$$⊢\phi \to C{C}_{𝑐}K=\frac{C^{\underset{\_}{K}}}{K!}$$

Proof

Step	Hyp	Ref	Expression
1		bccval.c	$$⊢\phi \to C\in ℂ$$
2		bccval.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
3		df-bcc	$$⊢C_{𝑐}=\left(c\in ℂ,k\in {\mathbb{N}}_0⟼\frac{c^{\underset{\_}{k}}}{k!}\right)$$
4	3	a1i	$$⊢\phi \to C_{𝑐}=\left(c\in ℂ,k\in {\mathbb{N}}_0⟼\frac{c^{\underset{\_}{k}}}{k!}\right)$$
5		simprl	$$⊢\left(\phi \wedge \left(c=C\wedge k=K\right)\right)\to c=C$$
6		simprr	$$⊢\left(\phi \wedge \left(c=C\wedge k=K\right)\right)\to k=K$$
7	5 6	oveq12d	$$⊢\left(\phi \wedge \left(c=C\wedge k=K\right)\right)\to c^{\underset{\_}{k}}=C^{\underset{\_}{K}}$$
8	6	fveq2d	$$⊢\left(\phi \wedge \left(c=C\wedge k=K\right)\right)\to k!=K!$$
9	7 8	oveq12d	$$⊢\left(\phi \wedge \left(c=C\wedge k=K\right)\right)\to \frac{c^{\underset{\_}{k}}}{k!}=\frac{C^{\underset{\_}{K}}}{K!}$$
10		ovexd	$$⊢\phi \to \frac{C^{\underset{\_}{K}}}{K!}\in \mathrm{V}$$
11	4 9 1 2 10	ovmpod	$$⊢\phi \to C{C}_{𝑐}K=\frac{C^{\underset{\_}{K}}}{K!}$$