Theorem bccn0

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

	Ref	Expression
Hypothesis	bccn0.c	$$⊢\phi \to C\in ℂ$$
Assertion	bccn0	$$⊢\phi \to C{C}_{𝑐}0=1$$

Proof

Step	Hyp	Ref	Expression
1		bccn0.c	$$⊢\phi \to C\in ℂ$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	2	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
4	1 3	bccval	$$⊢\phi \to C{C}_{𝑐}0=\frac{C^{\underset{\_}{0}}}{0!}$$
5		fallfac0	$$⊢C\in ℂ\to C^{\underset{\_}{0}}=1$$
6	1 5	syl	$$⊢\phi \to C^{\underset{\_}{0}}=1$$
7		fac0	$$⊢0!=1$$
8	7	a1i	$$⊢\phi \to 0!=1$$
9	6 8	oveq12d	$$⊢\phi \to \frac{C^{\underset{\_}{0}}}{0!}=\frac{1}{1}$$
10		1div1e1	$$⊢\frac{1}{1}=1$$
11	9 10	eqtrdi	$$⊢\phi \to \frac{C^{\underset{\_}{0}}}{0!}=1$$
12	4 11	eqtrd	$$⊢\phi \to C{C}_{𝑐}0=1$$