This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bccl

Description: A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by NM, 10-Jul-2005) (Revised by Mario Carneiro, 9-Nov-2013)

Ref Expression
Assertion bccl 
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( m = 0 -> ( m _C k ) = ( 0 _C k ) )
2 1 eleq1d 
 |-  ( m = 0 -> ( ( m _C k ) e. NN0 <-> ( 0 _C k ) e. NN0 ) )
3 2 ralbidv 
 |-  ( m = 0 -> ( A. k e. ZZ ( m _C k ) e. NN0 <-> A. k e. ZZ ( 0 _C k ) e. NN0 ) )
4 oveq1 
 |-  ( m = n -> ( m _C k ) = ( n _C k ) )
5 4 eleq1d 
 |-  ( m = n -> ( ( m _C k ) e. NN0 <-> ( n _C k ) e. NN0 ) )
6 5 ralbidv 
 |-  ( m = n -> ( A. k e. ZZ ( m _C k ) e. NN0 <-> A. k e. ZZ ( n _C k ) e. NN0 ) )
7 oveq1 
 |-  ( m = ( n + 1 ) -> ( m _C k ) = ( ( n + 1 ) _C k ) )
8 7 eleq1d 
 |-  ( m = ( n + 1 ) -> ( ( m _C k ) e. NN0 <-> ( ( n + 1 ) _C k ) e. NN0 ) )
9 8 ralbidv 
 |-  ( m = ( n + 1 ) -> ( A. k e. ZZ ( m _C k ) e. NN0 <-> A. k e. ZZ ( ( n + 1 ) _C k ) e. NN0 ) )
10 oveq1 
 |-  ( m = N -> ( m _C k ) = ( N _C k ) )
11 10 eleq1d 
 |-  ( m = N -> ( ( m _C k ) e. NN0 <-> ( N _C k ) e. NN0 ) )
12 11 ralbidv 
 |-  ( m = N -> ( A. k e. ZZ ( m _C k ) e. NN0 <-> A. k e. ZZ ( N _C k ) e. NN0 ) )
13 elfz1eq 
 |-  ( k e. ( 0 ... 0 ) -> k = 0 )
14 13 adantl 
 |-  ( ( k e. ZZ /\ k e. ( 0 ... 0 ) ) -> k = 0 )
15 oveq2 
 |-  ( k = 0 -> ( 0 _C k ) = ( 0 _C 0 ) )
16 0nn0 
 |-  0 e. NN0
17 bcn0 
 |-  ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
18 16 17 ax-mp 
 |-  ( 0 _C 0 ) = 1
19 1nn0 
 |-  1 e. NN0
20 18 19 eqeltri 
 |-  ( 0 _C 0 ) e. NN0
21 15 20 eqeltrdi 
 |-  ( k = 0 -> ( 0 _C k ) e. NN0 )
22 14 21 syl 
 |-  ( ( k e. ZZ /\ k e. ( 0 ... 0 ) ) -> ( 0 _C k ) e. NN0 )
23 bcval3 
 |-  ( ( 0 e. NN0 /\ k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( 0 _C k ) = 0 )
24 16 23 mp3an1 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( 0 _C k ) = 0 )
25 24 16 eqeltrdi 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( 0 _C k ) e. NN0 )
26 22 25 pm2.61dan 
 |-  ( k e. ZZ -> ( 0 _C k ) e. NN0 )
27 26 rgen 
 |-  A. k e. ZZ ( 0 _C k ) e. NN0
28 oveq2 
 |-  ( k = m -> ( n _C k ) = ( n _C m ) )
29 28 eleq1d 
 |-  ( k = m -> ( ( n _C k ) e. NN0 <-> ( n _C m ) e. NN0 ) )
30 29 cbvralvw 
 |-  ( A. k e. ZZ ( n _C k ) e. NN0 <-> A. m e. ZZ ( n _C m ) e. NN0 )
31 bcpasc 
 |-  ( ( n e. NN0 /\ k e. ZZ ) -> ( ( n _C k ) + ( n _C ( k - 1 ) ) ) = ( ( n + 1 ) _C k ) )
32 31 adantlr 
 |-  ( ( ( n e. NN0 /\ A. m e. ZZ ( n _C m ) e. NN0 ) /\ k e. ZZ ) -> ( ( n _C k ) + ( n _C ( k - 1 ) ) ) = ( ( n + 1 ) _C k ) )
33 oveq2 
 |-  ( m = k -> ( n _C m ) = ( n _C k ) )
34 33 eleq1d 
 |-  ( m = k -> ( ( n _C m ) e. NN0 <-> ( n _C k ) e. NN0 ) )
35 34 rspccva 
 |-  ( ( A. m e. ZZ ( n _C m ) e. NN0 /\ k e. ZZ ) -> ( n _C k ) e. NN0 )
36 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
37 oveq2 
 |-  ( m = ( k - 1 ) -> ( n _C m ) = ( n _C ( k - 1 ) ) )
38 37 eleq1d 
 |-  ( m = ( k - 1 ) -> ( ( n _C m ) e. NN0 <-> ( n _C ( k - 1 ) ) e. NN0 ) )
39 38 rspccva 
 |-  ( ( A. m e. ZZ ( n _C m ) e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( n _C ( k - 1 ) ) e. NN0 )
40 36 39 sylan2 
 |-  ( ( A. m e. ZZ ( n _C m ) e. NN0 /\ k e. ZZ ) -> ( n _C ( k - 1 ) ) e. NN0 )
41 35 40 nn0addcld 
 |-  ( ( A. m e. ZZ ( n _C m ) e. NN0 /\ k e. ZZ ) -> ( ( n _C k ) + ( n _C ( k - 1 ) ) ) e. NN0 )
42 41 adantll 
 |-  ( ( ( n e. NN0 /\ A. m e. ZZ ( n _C m ) e. NN0 ) /\ k e. ZZ ) -> ( ( n _C k ) + ( n _C ( k - 1 ) ) ) e. NN0 )
43 32 42 eqeltrrd 
 |-  ( ( ( n e. NN0 /\ A. m e. ZZ ( n _C m ) e. NN0 ) /\ k e. ZZ ) -> ( ( n + 1 ) _C k ) e. NN0 )
44 43 ralrimiva 
 |-  ( ( n e. NN0 /\ A. m e. ZZ ( n _C m ) e. NN0 ) -> A. k e. ZZ ( ( n + 1 ) _C k ) e. NN0 )
45 44 ex 
 |-  ( n e. NN0 -> ( A. m e. ZZ ( n _C m ) e. NN0 -> A. k e. ZZ ( ( n + 1 ) _C k ) e. NN0 ) )
46 30 45 biimtrid 
 |-  ( n e. NN0 -> ( A. k e. ZZ ( n _C k ) e. NN0 -> A. k e. ZZ ( ( n + 1 ) _C k ) e. NN0 ) )
47 3 6 9 12 27 46 nn0ind 
 |-  ( N e. NN0 -> A. k e. ZZ ( N _C k ) e. NN0 )
48 oveq2 
 |-  ( k = K -> ( N _C k ) = ( N _C K ) )
49 48 eleq1d 
 |-  ( k = K -> ( ( N _C k ) e. NN0 <-> ( N _C K ) e. NN0 ) )
50 49 rspccva 
 |-  ( ( A. k e. ZZ ( N _C k ) e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 )
51 47 50 sylan 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 )