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 )