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 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 )