bccl

Description: A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by NM, 10-Jul-2005) (Revised by Mario Carneiro, 9-Nov-2013)

		Ref	Expression
	Assertion	bccl	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ m = 0 \to (\binom{m}{k}) = (\binom{0}{k})$
2	1	eleq1d	$⊢ m = 0 \to ((\binom{m}{k}) \in ℕ_{0} \leftrightarrow (\binom{0}{k}) \in ℕ_{0})$
3	2	ralbidv	$⊢ m = 0 \to (\forall k \in ℤ (\binom{m}{k}) \in ℕ_{0} \leftrightarrow \forall k \in ℤ (\binom{0}{k}) \in ℕ_{0})$
4		oveq1	$⊢ m = n \to (\binom{m}{k}) = (\binom{n}{k})$
5	4	eleq1d	$⊢ m = n \to ((\binom{m}{k}) \in ℕ_{0} \leftrightarrow (\binom{n}{k}) \in ℕ_{0})$
6	5	ralbidv	$⊢ m = n \to (\forall k \in ℤ (\binom{m}{k}) \in ℕ_{0} \leftrightarrow \forall k \in ℤ (\binom{n}{k}) \in ℕ_{0})$
7		oveq1	$⊢ m = n + 1 \to (\binom{m}{k}) = (\binom{n + 1}{k})$
8	7	eleq1d	$⊢ m = n + 1 \to ((\binom{m}{k}) \in ℕ_{0} \leftrightarrow (\binom{n + 1}{k}) \in ℕ_{0})$
9	8	ralbidv	$⊢ m = n + 1 \to (\forall k \in ℤ (\binom{m}{k}) \in ℕ_{0} \leftrightarrow \forall k \in ℤ (\binom{n + 1}{k}) \in ℕ_{0})$
10		oveq1	$⊢ m = N \to (\binom{m}{k}) = (\binom{N}{k})$
11	10	eleq1d	$⊢ m = N \to ((\binom{m}{k}) \in ℕ_{0} \leftrightarrow (\binom{N}{k}) \in ℕ_{0})$
12	11	ralbidv	$⊢ m = N \to (\forall k \in ℤ (\binom{m}{k}) \in ℕ_{0} \leftrightarrow \forall k \in ℤ (\binom{N}{k}) \in ℕ_{0})$
13		elfz1eq	$⊢ k \in (0 \dots 0) \to k = 0$
14	13	adantl	$⊢ (k \in ℤ \land k \in (0 \dots 0)) \to k = 0$
15		oveq2	$⊢ k = 0 \to (\binom{0}{k}) = (\binom{0}{0})$
16		0nn0	$⊢ 0 \in ℕ_{0}$
17		bcn0	$⊢ 0 \in ℕ_{0} \to (\binom{0}{0}) = 1$
18	16 17	ax-mp	$⊢ (\binom{0}{0}) = 1$
19		1nn0	$⊢ 1 \in ℕ_{0}$
20	18 19	eqeltri	$⊢ (\binom{0}{0}) \in ℕ_{0}$
21	15 20	eqeltrdi	$⊢ k = 0 \to (\binom{0}{k}) \in ℕ_{0}$
22	14 21	syl	$⊢ (k \in ℤ \land k \in (0 \dots 0)) \to (\binom{0}{k}) \in ℕ_{0}$
23		bcval3	$⊢ (0 \in ℕ_{0} \land k \in ℤ \land \neg k \in (0 \dots 0)) \to (\binom{0}{k}) = 0$
24	16 23	mp3an1	$⊢ (k \in ℤ \land \neg k \in (0 \dots 0)) \to (\binom{0}{k}) = 0$
25	24 16	eqeltrdi	$⊢ (k \in ℤ \land \neg k \in (0 \dots 0)) \to (\binom{0}{k}) \in ℕ_{0}$
26	22 25	pm2.61dan	$⊢ k \in ℤ \to (\binom{0}{k}) \in ℕ_{0}$
27	26	rgen	$⊢ \forall k \in ℤ (\binom{0}{k}) \in ℕ_{0}$
28		oveq2	$⊢ k = m \to (\binom{n}{k}) = (\binom{n}{m})$
29	28	eleq1d	$⊢ k = m \to ((\binom{n}{k}) \in ℕ_{0} \leftrightarrow (\binom{n}{m}) \in ℕ_{0})$
30	29	cbvralvw	$⊢ \forall k \in ℤ (\binom{n}{k}) \in ℕ_{0} \leftrightarrow \forall m \in ℤ (\binom{n}{m}) \in ℕ_{0}$
31		bcpasc	$⊢ (n \in ℕ_{0} \land k \in ℤ) \to (\binom{n}{k}) + (\binom{n}{k - 1}) = (\binom{n + 1}{k})$
32	31	adantlr	$⊢ ((n \in ℕ_{0} \land \forall m \in ℤ (\binom{n}{m}) \in ℕ_{0}) \land k \in ℤ) \to (\binom{n}{k}) + (\binom{n}{k - 1}) = (\binom{n + 1}{k})$
33		oveq2	$⊢ m = k \to (\binom{n}{m}) = (\binom{n}{k})$
34	33	eleq1d	$⊢ m = k \to ((\binom{n}{m}) \in ℕ_{0} \leftrightarrow (\binom{n}{k}) \in ℕ_{0})$
35	34	rspccva	$⊢ (\forall m \in ℤ (\binom{n}{m}) \in ℕ_{0} \land k \in ℤ) \to (\binom{n}{k}) \in ℕ_{0}$
36		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
37		oveq2	$⊢ m = k - 1 \to (\binom{n}{m}) = (\binom{n}{k - 1})$
38	37	eleq1d	$⊢ m = k - 1 \to ((\binom{n}{m}) \in ℕ_{0} \leftrightarrow (\binom{n}{k - 1}) \in ℕ_{0})$
39	38	rspccva	$⊢ (\forall m \in ℤ (\binom{n}{m}) \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{n}{k - 1}) \in ℕ_{0}$
40	36 39	sylan2	$⊢ (\forall m \in ℤ (\binom{n}{m}) \in ℕ_{0} \land k \in ℤ) \to (\binom{n}{k - 1}) \in ℕ_{0}$
41	35 40	nn0addcld	$⊢ (\forall m \in ℤ (\binom{n}{m}) \in ℕ_{0} \land k \in ℤ) \to (\binom{n}{k}) + (\binom{n}{k - 1}) \in ℕ_{0}$
42	41	adantll	$⊢ ((n \in ℕ_{0} \land \forall m \in ℤ (\binom{n}{m}) \in ℕ_{0}) \land k \in ℤ) \to (\binom{n}{k}) + (\binom{n}{k - 1}) \in ℕ_{0}$
43	32 42	eqeltrrd	$⊢ ((n \in ℕ_{0} \land \forall m \in ℤ (\binom{n}{m}) \in ℕ_{0}) \land k \in ℤ) \to (\binom{n + 1}{k}) \in ℕ_{0}$
44	43	ralrimiva	$⊢ (n \in ℕ_{0} \land \forall m \in ℤ (\binom{n}{m}) \in ℕ_{0}) \to \forall k \in ℤ (\binom{n + 1}{k}) \in ℕ_{0}$
45	44	ex	$⊢ n \in ℕ_{0} \to (\forall m \in ℤ (\binom{n}{m}) \in ℕ_{0} \to \forall k \in ℤ (\binom{n + 1}{k}) \in ℕ_{0})$
46	30 45	syl5bi	$⊢ n \in ℕ_{0} \to (\forall k \in ℤ (\binom{n}{k}) \in ℕ_{0} \to \forall k \in ℤ (\binom{n + 1}{k}) \in ℕ_{0})$
47	3 6 9 12 27 46	nn0ind	$⊢ N \in ℕ_{0} \to \forall k \in ℤ (\binom{N}{k}) \in ℕ_{0}$
48		oveq2	$⊢ k = K \to (\binom{N}{k}) = (\binom{N}{K})$
49	48	eleq1d	$⊢ k = K \to ((\binom{N}{k}) \in ℕ_{0} \leftrightarrow (\binom{N}{K}) \in ℕ_{0})$
50	49	rspccva	$⊢ (\forall k \in ℤ (\binom{N}{k}) \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) \in ℕ_{0}$
51	47 50	sylan	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) \in ℕ_{0}$

Metamath Proof Explorer

Theorem bccl

Proof