Theorem bccn0

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

	Ref	Expression
Hypothesis	bccn0.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion	bccn0	⊢ ( 𝜑 → ( 𝐶 C𝑐 0 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		bccn0.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2		0nn0	⊢ 0 ∈ ℕ0
3	2	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
4	1 3	bccval	⊢ ( 𝜑 → ( 𝐶 C𝑐 0 ) = ( ( 𝐶 FallFac 0 ) / ( ! ‘ 0 ) ) )
5		fallfac0	⊢ ( 𝐶 ∈ ℂ → ( 𝐶 FallFac 0 ) = 1 )
6	1 5	syl	⊢ ( 𝜑 → ( 𝐶 FallFac 0 ) = 1 )
7		fac0	⊢ ( ! ‘ 0 ) = 1
8	7	a1i	⊢ ( 𝜑 → ( ! ‘ 0 ) = 1 )
9	6 8	oveq12d	⊢ ( 𝜑 → ( ( 𝐶 FallFac 0 ) / ( ! ‘ 0 ) ) = ( 1 / 1 ) )
10		1div1e1	⊢ ( 1 / 1 ) = 1
11	9 10	eqtrdi	⊢ ( 𝜑 → ( ( 𝐶 FallFac 0 ) / ( ! ‘ 0 ) ) = 1 )
12	4 11	eqtrd	⊢ ( 𝜑 → ( 𝐶 C𝑐 0 ) = 1 )