Metamath Proof Explorer

Theorem bcneg1

Description: The binomial coefficient over negative one is zero. (Contributed by Scott Fenton, 29-May-2020)

Ref Expression
Assertion bcneg1 ⊢ N ∈ ℕ 0 → ( N − 1 ) = 0

Proof

Step Hyp Ref Expression
1 neg1z ⊢ − 1 ∈ ℤ
2 bcval ⊢ N ∈ ℕ 0 ∧ − 1 ∈ ℤ → ( N − 1 ) = if − 1 ∈ 0 … N N ! N − -1 ! ⁢ -1 ! 0
3 1 2 mpan2 ⊢ N ∈ ℕ 0 → ( N − 1 ) = if − 1 ∈ 0 … N N ! N − -1 ! ⁢ -1 ! 0
4 neg1lt0 ⊢ − 1 < 0
5 neg1rr ⊢ − 1 ∈ ℝ
6 0re ⊢ 0 ∈ ℝ
7 5 6 ltnlei ⊢ − 1 < 0 ↔ ¬ 0 ≤ − 1
8 4 7 mpbi ⊢ ¬ 0 ≤ − 1
9 8 intnanr ⊢ ¬ 0 ≤ − 1 ∧ − 1 ≤ N
10 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
11 0z ⊢ 0 ∈ ℤ
12 elfz ⊢ − 1 ∈ ℤ ∧ 0 ∈ ℤ ∧ N ∈ ℤ → − 1 ∈ 0 … N ↔ 0 ≤ − 1 ∧ − 1 ≤ N
13 1 11 12 mp3an12 ⊢ N ∈ ℤ → − 1 ∈ 0 … N ↔ 0 ≤ − 1 ∧ − 1 ≤ N
14 10 13 syl ⊢ N ∈ ℕ 0 → − 1 ∈ 0 … N ↔ 0 ≤ − 1 ∧ − 1 ≤ N
15 9 14 mtbiri ⊢ N ∈ ℕ 0 → ¬ − 1 ∈ 0 … N
16 15 iffalsed ⊢ N ∈ ℕ 0 → if − 1 ∈ 0 … N N ! N − -1 ! ⁢ -1 ! 0 = 0
17 3 16 eqtrd ⊢ N ∈ ℕ 0 → ( N − 1 ) = 0