Metamath Proof Explorer


Theorem bccn0

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

Ref Expression
Hypothesis bccn0.c φ C
Assertion bccn0 φ C C 𝑐 0 = 1

Proof

Step Hyp Ref Expression
1 bccn0.c φ C
2 0nn0 0 0
3 2 a1i φ 0 0
4 1 3 bccval φ C C 𝑐 0 = C 0 _ 0 !
5 fallfac0 C C 0 _ = 1
6 1 5 syl φ C 0 _ = 1
7 fac0 0 ! = 1
8 7 a1i φ 0 ! = 1
9 6 8 oveq12d φ C 0 _ 0 ! = 1 1
10 1div1e1 1 1 = 1
11 9 10 syl6eq φ C 0 _ 0 ! = 1
12 4 11 eqtrd φ C C 𝑐 0 = 1