Theorem bcval

Description: Value of the binomial coefficient, N choose K . Definition of binomial coefficient in Gleason p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ K <_ N does not hold. See bcval2 for the value in the standard domain. (Contributed by NM, 10-Jul-2005) (Revised by Mario Carneiro, 7-Nov-2013)

	Ref	Expression
Assertion	bcval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) = if ( 𝐾 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
2	1	eleq2d	⊢ ( 𝑛 = 𝑁 → ( 𝑘 ∈ ( 0 ... 𝑛 ) ↔ 𝑘 ∈ ( 0 ... 𝑁 ) ) )
3		fveq2	⊢ ( 𝑛 = 𝑁 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑁 ) )
4		fvoveq1	⊢ ( 𝑛 = 𝑁 → ( ! ‘ ( 𝑛 − 𝑘 ) ) = ( ! ‘ ( 𝑁 − 𝑘 ) ) )
5	4	oveq1d	⊢ ( 𝑛 = 𝑁 → ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) = ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) )
6	3 5	oveq12d	⊢ ( 𝑛 = 𝑁 → ( ( ! ‘ 𝑛 ) / ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) )
7	2 6	ifbieq1d	⊢ ( 𝑛 = 𝑁 → if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( ( ! ‘ 𝑛 ) / ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) , 0 ) = if ( 𝑘 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) , 0 ) )
8		eleq1	⊢ ( 𝑘 = 𝐾 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ∈ ( 0 ... 𝑁 ) ) )
9		oveq2	⊢ ( 𝑘 = 𝐾 → ( 𝑁 − 𝑘 ) = ( 𝑁 − 𝐾 ) )
10	9	fveq2d	⊢ ( 𝑘 = 𝐾 → ( ! ‘ ( 𝑁 − 𝑘 ) ) = ( ! ‘ ( 𝑁 − 𝐾 ) ) )
11		fveq2	⊢ ( 𝑘 = 𝐾 → ( ! ‘ 𝑘 ) = ( ! ‘ 𝐾 ) )
12	10 11	oveq12d	⊢ ( 𝑘 = 𝐾 → ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) )
13	12	oveq2d	⊢ ( 𝑘 = 𝐾 → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
14	8 13	ifbieq1d	⊢ ( 𝑘 = 𝐾 → if ( 𝑘 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) , 0 ) = if ( 𝐾 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) , 0 ) )
15		df-bc	⊢ C = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( ( ! ‘ 𝑛 ) / ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) , 0 ) )
16		ovex	⊢ ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ∈ V
17		c0ex	⊢ 0 ∈ V
18	16 17	ifex	⊢ if ( 𝐾 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) , 0 ) ∈ V
19	7 14 15 18	ovmpo	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) = if ( 𝐾 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) , 0 ) )