This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )