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

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 biimtrid ⊢ ( 𝑛 ∈ ℕ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 )