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	$⊢ (N \in ℕ_{0} \land K \in ℤ \land (K < 0 \lor N < K)) \to (\binom{N}{K}) = 0$

Proof

Step	Hyp	Ref	Expression
1		elfzle1	$⊢ K \in (0 \dots N) \to 0 \leq K$
2		0re	$⊢ 0 \in ℝ$
3		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
4	3	zred	$⊢ K \in (0 \dots N) \to K \in ℝ$
5		lenlt	$⊢ (0 \in ℝ \land K \in ℝ) \to (0 \leq K \leftrightarrow \neg K < 0)$
6	2 4 5	sylancr	$⊢ K \in (0 \dots N) \to (0 \leq K \leftrightarrow \neg K < 0)$
7	1 6	mpbid	$⊢ K \in (0 \dots N) \to \neg K < 0$
8	7	adantl	$⊢ (N \in ℕ_{0} \land K \in (0 \dots N)) \to \neg K < 0$
9		elfzle2	$⊢ K \in (0 \dots N) \to K \leq N$
10	9	adantl	$⊢ (N \in ℕ_{0} \land K \in (0 \dots N)) \to K \leq N$
11		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
12		lenlt	$⊢ (K \in ℝ \land N \in ℝ) \to (K \leq N \leftrightarrow \neg N < K)$
13	4 11 12	syl2anr	$⊢ (N \in ℕ_{0} \land K \in (0 \dots N)) \to (K \leq N \leftrightarrow \neg N < K)$
14	10 13	mpbid	$⊢ (N \in ℕ_{0} \land K \in (0 \dots N)) \to \neg N < K$
15		ioran	$⊢ \neg (K < 0 \lor N < K) \leftrightarrow (\neg K < 0 \land \neg N < K)$
16	8 14 15	sylanbrc	$⊢ (N \in ℕ_{0} \land K \in (0 \dots N)) \to \neg (K < 0 \lor N < K)$
17	16	ex	$⊢ N \in ℕ_{0} \to (K \in (0 \dots N) \to \neg (K < 0 \lor N < K))$
18	17	adantr	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (K \in (0 \dots N) \to \neg (K < 0 \lor N < K))$
19	18	con2d	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to ((K < 0 \lor N < K) \to \neg K \in (0 \dots N))$
20	19	3impia	$⊢ (N \in ℕ_{0} \land K \in ℤ \land (K < 0 \lor N < K)) \to \neg K \in (0 \dots N)$
21		bcval3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
22	20 21	syld3an3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land (K < 0 \lor N < K)) \to (\binom{N}{K}) = 0$

Metamath Proof Explorer

Theorem bcval4

Proof