Theorem bcneg1

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

	Ref	Expression
Assertion	bcneg1	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C - 1 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		neg1z	⊢ - 1 ∈ ℤ
2		bcval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ - 1 ∈ ℤ ) → ( 𝑁 C - 1 ) = if ( - 1 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − - 1 ) ) · ( ! ‘ - 1 ) ) ) , 0 ) )
3	1 2	mpan2	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C - 1 ) = if ( - 1 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − - 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 ≤ 𝑁 )
10		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
11		0z	⊢ 0 ∈ ℤ
12		elfz	⊢ ( ( - 1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 1 ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ - 1 ∧ - 1 ≤ 𝑁 ) ) )
13	1 11 12	mp3an12	⊢ ( 𝑁 ∈ ℤ → ( - 1 ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ - 1 ∧ - 1 ≤ 𝑁 ) ) )
14	10 13	syl	⊢ ( 𝑁 ∈ ℕ0 → ( - 1 ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ - 1 ∧ - 1 ≤ 𝑁 ) ) )
15	9 14	mtbiri	⊢ ( 𝑁 ∈ ℕ0 → ¬ - 1 ∈ ( 0 ... 𝑁 ) )
16	15	iffalsed	⊢ ( 𝑁 ∈ ℕ0 → if ( - 1 ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − - 1 ) ) · ( ! ‘ - 1 ) ) ) , 0 ) = 0 )
17	3 16	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C - 1 ) = 0 )