Theorem bccval

Description: Value of the generalized binomial coefficient, C choose K . (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	bccval.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	bccval.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion	bccval	⊢ ( 𝜑 → ( 𝐶 C𝑐 𝐾 ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bccval.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2		bccval.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3		df-bcc	⊢ C𝑐 = ( 𝑐 ∈ ℂ , 𝑘 ∈ ℕ0 ↦ ( ( 𝑐 FallFac 𝑘 ) / ( ! ‘ 𝑘 ) ) )
4	3	a1i	⊢ ( 𝜑 → C𝑐 = ( 𝑐 ∈ ℂ , 𝑘 ∈ ℕ0 ↦ ( ( 𝑐 FallFac 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
5		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑘 = 𝐾 ) ) → 𝑐 = 𝐶 )
6		simprr	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑘 = 𝐾 ) ) → 𝑘 = 𝐾 )
7	5 6	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑘 = 𝐾 ) ) → ( 𝑐 FallFac 𝑘 ) = ( 𝐶 FallFac 𝐾 ) )
8	6	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑘 = 𝐾 ) ) → ( ! ‘ 𝑘 ) = ( ! ‘ 𝐾 ) )
9	7 8	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑘 = 𝐾 ) ) → ( ( 𝑐 FallFac 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
10		ovexd	⊢ ( 𝜑 → ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) ∈ V )
11	4 9 1 2 10	ovmpod	⊢ ( 𝜑 → ( 𝐶 C𝑐 𝐾 ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )