Theorem bccn1

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

	Ref	Expression
Hypothesis	bccn0.c	|- ( ph -> C e. CC )
Assertion	bccn1	|- ( ph -> ( C _Cc 1 ) = C )

Proof

Step	Hyp	Ref	Expression
1		bccn0.c	|- ( ph -> C e. CC )
2		0nn0	|- 0 e. NN0
3	2	a1i	|- ( ph -> 0 e. NN0 )
4	1 3	bccp1k	|- ( ph -> ( C _Cc ( 0 + 1 ) ) = ( ( C _Cc 0 ) x. ( ( C - 0 ) / ( 0 + 1 ) ) ) )
5		0p1e1	|- ( 0 + 1 ) = 1
6	5	oveq2i	|- ( C _Cc ( 0 + 1 ) ) = ( C _Cc 1 )
7	6	a1i	|- ( ph -> ( C _Cc ( 0 + 1 ) ) = ( C _Cc 1 ) )
8	1	bccn0	|- ( ph -> ( C _Cc 0 ) = 1 )
9	1	subid1d	|- ( ph -> ( C - 0 ) = C )
10	5	a1i	|- ( ph -> ( 0 + 1 ) = 1 )
11	9 10	oveq12d	|- ( ph -> ( ( C - 0 ) / ( 0 + 1 ) ) = ( C / 1 ) )
12	1	div1d	|- ( ph -> ( C / 1 ) = C )
13	11 12	eqtrd	|- ( ph -> ( ( C - 0 ) / ( 0 + 1 ) ) = C )
14	8 13	oveq12d	|- ( ph -> ( ( C _Cc 0 ) x. ( ( C - 0 ) / ( 0 + 1 ) ) ) = ( 1 x. C ) )
15	4 7 14	3eqtr3d	|- ( ph -> ( C _Cc 1 ) = ( 1 x. C ) )
16	1	mulid2d	|- ( ph -> ( 1 x. C ) = C )
17	15 16	eqtrd	|- ( ph -> ( C _Cc 1 ) = C )