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 e. NN0 -> ( N _C -u 1 ) = 0 )

Proof

Step Hyp Ref Expression
1 neg1z
 |-  -u 1 e. ZZ
2 bcval
 |-  ( ( N e. NN0 /\ -u 1 e. ZZ ) -> ( N _C -u 1 ) = if ( -u 1 e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - -u 1 ) ) x. ( ! ` -u 1 ) ) ) , 0 ) )
3 1 2 mpan2
 |-  ( N e. NN0 -> ( N _C -u 1 ) = if ( -u 1 e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - -u 1 ) ) x. ( ! ` -u 1 ) ) ) , 0 ) )
4 neg1lt0
 |-  -u 1 < 0
5 neg1rr
 |-  -u 1 e. RR
6 0re
 |-  0 e. RR
7 5 6 ltnlei
 |-  ( -u 1 < 0 <-> -. 0 <_ -u 1 )
8 4 7 mpbi
 |-  -. 0 <_ -u 1
9 8 intnanr
 |-  -. ( 0 <_ -u 1 /\ -u 1 <_ N )
10 nn0z
 |-  ( N e. NN0 -> N e. ZZ )
11 0z
 |-  0 e. ZZ
12 elfz
 |-  ( ( -u 1 e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( -u 1 e. ( 0 ... N ) <-> ( 0 <_ -u 1 /\ -u 1 <_ N ) ) )
13 1 11 12 mp3an12
 |-  ( N e. ZZ -> ( -u 1 e. ( 0 ... N ) <-> ( 0 <_ -u 1 /\ -u 1 <_ N ) ) )
14 10 13 syl
 |-  ( N e. NN0 -> ( -u 1 e. ( 0 ... N ) <-> ( 0 <_ -u 1 /\ -u 1 <_ N ) ) )
15 9 14 mtbiri
 |-  ( N e. NN0 -> -. -u 1 e. ( 0 ... N ) )
16 15 iffalsed
 |-  ( N e. NN0 -> if ( -u 1 e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - -u 1 ) ) x. ( ! ` -u 1 ) ) ) , 0 ) = 0 )
17 3 16 eqtrd
 |-  ( N e. NN0 -> ( N _C -u 1 ) = 0 )