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

Metamath Proof Explorer

Theorem bcval3

Description: Value of the binomial coefficient, N choose K , outside of its standard domain. Remark in Gleason p. 295. (Contributed by NM, 14-Jul-2005) (Revised by Mario Carneiro, 8-Nov-2013)

Ref Expression
Assertion bcval3 ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )

Proof

Step Hyp Ref Expression
1 bcval ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) = if ( 𝐾 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) , 0 ) )
2 1 3adant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = if ( 𝐾 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) , 0 ) )
3 iffalse ⊢ ( ¬ 𝐾 ∈ ( 0 ... 𝑁 ) → if ( 𝐾 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) , 0 ) = 0 )
4 3 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → if ( 𝐾 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) , 0 ) = 0 )
5 2 4 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )