Theorem bccn1

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

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

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	bccp1k	$$⊢\phi \to C{C}_{𝑐}\left(0+1\right)=\left(C{C}_{𝑐}0\right)\left(\frac{C-0}{0+1}\right)$$
5		0p1e1	$$⊢0+1=1$$
6	5	oveq2i	$$⊢C{C}_{𝑐}\left(0+1\right)=C{C}_{𝑐}1$$
7	6	a1i	$$⊢\phi \to C{C}_{𝑐}\left(0+1\right)=C{C}_{𝑐}1$$
8	1	bccn0	$$⊢\phi \to C{C}_{𝑐}0=1$$
9	1	subid1d	$$⊢\phi \to C-0=C$$
10	5	a1i	$$⊢\phi \to 0+1=1$$
11	9 10	oveq12d	$$⊢\phi \to \frac{C-0}{0+1}=\frac{C}{1}$$
12	1	div1d	$$⊢\phi \to \frac{C}{1}=C$$
13	11 12	eqtrd	$$⊢\phi \to \frac{C-0}{0+1}=C$$
14	8 13	oveq12d	$$⊢\phi \to \left(C{C}_{𝑐}0\right)\left(\frac{C-0}{0+1}\right)=1C$$
15	4 7 14	3eqtr3d	$$⊢\phi \to C{C}_{𝑐}1=1C$$
16	1	mullidd	$$⊢\phi \to 1C=C$$
17	15 16	eqtrd	$$⊢\phi \to C{C}_{𝑐}1=C$$