Metamath Proof Explorer

Theorem bccn0

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

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

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 bccval 
 |-  ( ph -> ( C _Cc 0 ) = ( ( C FallFac 0 ) / ( ! ` 0 ) ) )
5 fallfac0 
 |-  ( C e. CC -> ( C FallFac 0 ) = 1 )
6 1 5 syl 
 |-  ( ph -> ( C FallFac 0 ) = 1 )
7 fac0 
 |-  ( ! ` 0 ) = 1
8 7 a1i 
 |-  ( ph -> ( ! ` 0 ) = 1 )
9 6 8 oveq12d 
 |-  ( ph -> ( ( C FallFac 0 ) / ( ! ` 0 ) ) = ( 1 / 1 ) )
10 1div1e1 
 |-  ( 1 / 1 ) = 1
11 9 10 eqtrdi 
 |-  ( ph -> ( ( C FallFac 0 ) / ( ! ` 0 ) ) = 1 )
12 4 11 eqtrd 
 |-  ( ph -> ( C _Cc 0 ) = 1 )