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

Metamath Proof Explorer

Theorem bcval4

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, 7-Nov-2013)

Ref Expression
Assertion bcval4 ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ( 𝐾 < 0 ∨ 𝑁 < 𝐾 ) ) → ( 𝑁 C 𝐾 ) = 0 )

Proof

Step Hyp Ref Expression
1 elfzle1 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝐾 )
2 0re ⊢ 0 ∈ ℝ
3 elfzelz ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
4 3 zred ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℝ )
5 lenlt ⊢ ( ( 0 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 0 ≤ 𝐾 ↔ ¬ 𝐾 < 0 ) )
6 2 4 5 sylancr ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 0 ≤ 𝐾 ↔ ¬ 𝐾 < 0 ) )
7 1 6 mpbid ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ¬ 𝐾 < 0 )
8 7 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ¬ 𝐾 < 0 )
9 elfzle2 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ≤ 𝑁 )
10 9 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ≤ 𝑁 )
11 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
12 lenlt ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐾 ≤ 𝑁 ↔ ¬ 𝑁 < 𝐾 ) )
13 4 11 12 syl2anr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 ≤ 𝑁 ↔ ¬ 𝑁 < 𝐾 ) )
14 10 13 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ¬ 𝑁 < 𝐾 )
15 ioran ⊢ ( ¬ ( 𝐾 < 0 ∨ 𝑁 < 𝐾 ) ↔ ( ¬ 𝐾 < 0 ∧ ¬ 𝑁 < 𝐾 ) )
16 8 14 15 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝐾 < 0 ∨ 𝑁 < 𝐾 ) )
17 16 ex ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( 0 ... 𝑁 ) → ¬ ( 𝐾 < 0 ∨ 𝑁 < 𝐾 ) ) )
18 17 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) → ¬ ( 𝐾 < 0 ∨ 𝑁 < 𝐾 ) ) )
19 18 con2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 < 0 ∨ 𝑁 < 𝐾 ) → ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) )
20 19 3impia ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ( 𝐾 < 0 ∨ 𝑁 < 𝐾 ) ) → ¬ 𝐾 ∈ ( 0 ... 𝑁 ) )
21 bcval3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
22 20 21 syld3an3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ( 𝐾 < 0 ∨ 𝑁 < 𝐾 ) ) → ( 𝑁 C 𝐾 ) = 0 )