Metamath Proof Explorer

Theorem bcneg1

Description: The binomial coefficent 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…NN!N−-1!⁢-1!0
3 1 2 mpan2 ⊢N∈ℕ0→(N−1)=if−1∈0…NN!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…NN!N−-1!⁢-1!0=0
17 3 16 eqtrd ⊢N∈ℕ0→(N−1)=0