Metamath Proof Explorer


Theorem 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 ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑚 = 0 → ( 𝑚 C 𝑘 ) = ( 0 C 𝑘 ) )
2 1 eleq1d ( 𝑚 = 0 → ( ( 𝑚 C 𝑘 ) ∈ ℕ0 ↔ ( 0 C 𝑘 ) ∈ ℕ0 ) )
3 2 ralbidv ( 𝑚 = 0 → ( ∀ 𝑘 ∈ ℤ ( 𝑚 C 𝑘 ) ∈ ℕ0 ↔ ∀ 𝑘 ∈ ℤ ( 0 C 𝑘 ) ∈ ℕ0 ) )
4 oveq1 ( 𝑚 = 𝑛 → ( 𝑚 C 𝑘 ) = ( 𝑛 C 𝑘 ) )
5 4 eleq1d ( 𝑚 = 𝑛 → ( ( 𝑚 C 𝑘 ) ∈ ℕ0 ↔ ( 𝑛 C 𝑘 ) ∈ ℕ0 ) )
6 5 ralbidv ( 𝑚 = 𝑛 → ( ∀ 𝑘 ∈ ℤ ( 𝑚 C 𝑘 ) ∈ ℕ0 ↔ ∀ 𝑘 ∈ ℤ ( 𝑛 C 𝑘 ) ∈ ℕ0 ) )
7 oveq1 ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 C 𝑘 ) = ( ( 𝑛 + 1 ) C 𝑘 ) )
8 7 eleq1d ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑚 C 𝑘 ) ∈ ℕ0 ↔ ( ( 𝑛 + 1 ) C 𝑘 ) ∈ ℕ0 ) )
9 8 ralbidv ( 𝑚 = ( 𝑛 + 1 ) → ( ∀ 𝑘 ∈ ℤ ( 𝑚 C 𝑘 ) ∈ ℕ0 ↔ ∀ 𝑘 ∈ ℤ ( ( 𝑛 + 1 ) C 𝑘 ) ∈ ℕ0 ) )
10 oveq1 ( 𝑚 = 𝑁 → ( 𝑚 C 𝑘 ) = ( 𝑁 C 𝑘 ) )
11 10 eleq1d ( 𝑚 = 𝑁 → ( ( 𝑚 C 𝑘 ) ∈ ℕ0 ↔ ( 𝑁 C 𝑘 ) ∈ ℕ0 ) )
12 11 ralbidv ( 𝑚 = 𝑁 → ( ∀ 𝑘 ∈ ℤ ( 𝑚 C 𝑘 ) ∈ ℕ0 ↔ ∀ 𝑘 ∈ ℤ ( 𝑁 C 𝑘 ) ∈ ℕ0 ) )
13 elfz1eq ( 𝑘 ∈ ( 0 ... 0 ) → 𝑘 = 0 )
14 13 adantl ( ( 𝑘 ∈ ℤ ∧ 𝑘 ∈ ( 0 ... 0 ) ) → 𝑘 = 0 )
15 oveq2 ( 𝑘 = 0 → ( 0 C 𝑘 ) = ( 0 C 0 ) )
16 0nn0 0 ∈ ℕ0
17 bcn0 ( 0 ∈ ℕ0 → ( 0 C 0 ) = 1 )
18 16 17 ax-mp ( 0 C 0 ) = 1
19 1nn0 1 ∈ ℕ0
20 18 19 eqeltri ( 0 C 0 ) ∈ ℕ0
21 15 20 eqeltrdi ( 𝑘 = 0 → ( 0 C 𝑘 ) ∈ ℕ0 )
22 14 21 syl ( ( 𝑘 ∈ ℤ ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( 0 C 𝑘 ) ∈ ℕ0 )
23 bcval3 ( ( 0 ∈ ℕ0𝑘 ∈ ℤ ∧ ¬ 𝑘 ∈ ( 0 ... 0 ) ) → ( 0 C 𝑘 ) = 0 )
24 16 23 mp3an1 ( ( 𝑘 ∈ ℤ ∧ ¬ 𝑘 ∈ ( 0 ... 0 ) ) → ( 0 C 𝑘 ) = 0 )
25 24 16 eqeltrdi ( ( 𝑘 ∈ ℤ ∧ ¬ 𝑘 ∈ ( 0 ... 0 ) ) → ( 0 C 𝑘 ) ∈ ℕ0 )
26 22 25 pm2.61dan ( 𝑘 ∈ ℤ → ( 0 C 𝑘 ) ∈ ℕ0 )
27 26 rgen 𝑘 ∈ ℤ ( 0 C 𝑘 ) ∈ ℕ0
28 oveq2 ( 𝑘 = 𝑚 → ( 𝑛 C 𝑘 ) = ( 𝑛 C 𝑚 ) )
29 28 eleq1d ( 𝑘 = 𝑚 → ( ( 𝑛 C 𝑘 ) ∈ ℕ0 ↔ ( 𝑛 C 𝑚 ) ∈ ℕ0 ) )
30 29 cbvralvw ( ∀ 𝑘 ∈ ℤ ( 𝑛 C 𝑘 ) ∈ ℕ0 ↔ ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0 )
31 bcpasc ( ( 𝑛 ∈ ℕ0𝑘 ∈ ℤ ) → ( ( 𝑛 C 𝑘 ) + ( 𝑛 C ( 𝑘 − 1 ) ) ) = ( ( 𝑛 + 1 ) C 𝑘 ) )
32 31 adantlr ( ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑛 C 𝑘 ) + ( 𝑛 C ( 𝑘 − 1 ) ) ) = ( ( 𝑛 + 1 ) C 𝑘 ) )
33 oveq2 ( 𝑚 = 𝑘 → ( 𝑛 C 𝑚 ) = ( 𝑛 C 𝑘 ) )
34 33 eleq1d ( 𝑚 = 𝑘 → ( ( 𝑛 C 𝑚 ) ∈ ℕ0 ↔ ( 𝑛 C 𝑘 ) ∈ ℕ0 ) )
35 34 rspccva ( ( ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0𝑘 ∈ ℤ ) → ( 𝑛 C 𝑘 ) ∈ ℕ0 )
36 peano2zm ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
37 oveq2 ( 𝑚 = ( 𝑘 − 1 ) → ( 𝑛 C 𝑚 ) = ( 𝑛 C ( 𝑘 − 1 ) ) )
38 37 eleq1d ( 𝑚 = ( 𝑘 − 1 ) → ( ( 𝑛 C 𝑚 ) ∈ ℕ0 ↔ ( 𝑛 C ( 𝑘 − 1 ) ) ∈ ℕ0 ) )
39 38 rspccva ( ( ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑛 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
40 36 39 sylan2 ( ( ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0𝑘 ∈ ℤ ) → ( 𝑛 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
41 35 40 nn0addcld ( ( ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0𝑘 ∈ ℤ ) → ( ( 𝑛 C 𝑘 ) + ( 𝑛 C ( 𝑘 − 1 ) ) ) ∈ ℕ0 )
42 41 adantll ( ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑛 C 𝑘 ) + ( 𝑛 C ( 𝑘 − 1 ) ) ) ∈ ℕ0 )
43 32 42 eqeltrrd ( ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑛 + 1 ) C 𝑘 ) ∈ ℕ0 )
44 43 ralrimiva ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0 ) → ∀ 𝑘 ∈ ℤ ( ( 𝑛 + 1 ) C 𝑘 ) ∈ ℕ0 )
45 44 ex ( 𝑛 ∈ ℕ0 → ( ∀ 𝑚 ∈ ℤ ( 𝑛 C 𝑚 ) ∈ ℕ0 → ∀ 𝑘 ∈ ℤ ( ( 𝑛 + 1 ) C 𝑘 ) ∈ ℕ0 ) )
46 30 45 syl5bi ( 𝑛 ∈ ℕ0 → ( ∀ 𝑘 ∈ ℤ ( 𝑛 C 𝑘 ) ∈ ℕ0 → ∀ 𝑘 ∈ ℤ ( ( 𝑛 + 1 ) C 𝑘 ) ∈ ℕ0 ) )
47 3 6 9 12 27 46 nn0ind ( 𝑁 ∈ ℕ0 → ∀ 𝑘 ∈ ℤ ( 𝑁 C 𝑘 ) ∈ ℕ0 )
48 oveq2 ( 𝑘 = 𝐾 → ( 𝑁 C 𝑘 ) = ( 𝑁 C 𝐾 ) )
49 48 eleq1d ( 𝑘 = 𝐾 → ( ( 𝑁 C 𝑘 ) ∈ ℕ0 ↔ ( 𝑁 C 𝐾 ) ∈ ℕ0 ) )
50 49 rspccva ( ( ∀ 𝑘 ∈ ℤ ( 𝑁 C 𝑘 ) ∈ ℕ0𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )
51 47 50 sylan ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )