MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfznn0 Structured version   Visualization version   Unicode version

Theorem elfznn0 11894
Description: A member of a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by NM, 5-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfznn0  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )

Proof of Theorem elfznn0
StepHypRef Expression
1 elfz2nn0 11892 . 2  |-  ( K  e.  ( 0 ... N )  <->  ( K  e.  NN0  /\  N  e. 
NN0  /\  K  <_  N ) )
21simp1bi 1024 1  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1889   class class class wbr 4405  (class class class)co 6295   0cc0 9544    <_ cle 9681   NN0cn0 10876   ...cfz 11791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-nn 10617  df-n0 10877  df-z 10945  df-uz 11167  df-fz 11792
This theorem is referenced by:  fz0fzdiffz0  11906  difelfzle  11911  fzo0ssnn0  12001  bcrpcl  12500  bccmpl  12501  bcp1n  12508  bcp1nk  12509  bcval5  12510  permnn  12518  swrd0len  12785  swrd0f  12790  swrd0fv  12802  swrd0swrd  12824  swrdswrd0  12825  swrd0swrd0  12826  swrd0swrdid  12827  wrdcctswrd  12828  swrdccat3  12855  swrdccat3a  12857  swrdccat3blem  12858  splfv2a  12870  2cshwcshw  12931  cshwcsh2id  12934  binomlem  13899  binom1p  13901  binom1dif  13903  bcxmas  13905  climcnds  13921  arisum  13930  arisum2  13931  geolim  13938  geo2sum  13941  mertenslem1  13952  mertenslem2  13953  mertens  13954  risefacval2  14075  fallfacval2  14076  fallfacval3  14077  risefaccllem  14078  fallfaccllem  14079  risefacp1  14094  fallfacp1  14095  fallfacfwd  14101  binomfallfaclem1  14104  binomfallfaclem2  14105  binomrisefac  14107  bcfallfac  14109  bpolylem  14113  bpolysum  14118  bpolydiflem  14119  fsumkthpow  14121  bpoly4  14124  efcvgfsum  14152  efcj  14158  efaddlem  14159  effsumlt  14177  eirrlem  14268  3dvds  14381  prmdiveq  14746  pcbc  14857  vdwapf  14934  vdwlem2  14944  vdwlem6  14948  vdwlem8  14950  psgnunilem2  17148  efgcpbllemb  17417  gsummptnn0fz  17627  srgbinomlem3  17787  srgbinomlem4  17788  srgbinomlem  17789  psrbaglefi  18608  coe1mul2lem2  18873  coe1mul2  18874  coe1tmmul2  18881  coe1tmmul  18882  cply1mul  18899  gsummoncoe1  18910  m2pmfzgsumcl  19784  decpmatmul  19808  pmatcollpw3fi1lem1  19822  mp2pm2mplem4  19845  pm2mpmhmlem2  19855  chpscmatgsumbin  19880  chpscmatgsummon  19881  chfacfscmulgsum  19896  chfacfpmmulgsum  19900  cpmadugsumlemB  19910  cpmadugsumlemC  19911  cpmadugsumlemF  19912  cpmadugsumfi  19913  mbfi1fseqlem3  22687  mbfi1fseqlem4  22688  itg0  22749  itgz  22750  itgcl  22753  iblabsr  22799  iblmulc2  22800  itgsplit  22805  dvn2bss  22896  coe1mul3  23060  elply2  23162  plyf  23164  elplyd  23168  ply1termlem  23169  plyeq0lem  23176  plypf1  23178  plyaddlem1  23179  plymullem1  23180  plyaddlem  23181  plymullem  23182  coeeulem  23190  coeidlem  23203  coeid3  23206  plyco  23207  coeeq2  23208  dgreq  23210  coefv0  23214  coeaddlem  23215  coemullem  23216  coemulhi  23220  coemulc  23221  coe1termlem  23224  plycn  23227  plycjlem  23242  plycj  23243  plyrecj  23245  dvply1  23249  dvply2g  23250  vieta1lem2  23276  elqaalem2  23285  elqaalem3  23286  elqaalem2OLD  23288  elqaalem3OLD  23289  aareccl  23294  aannenlem1  23296  aalioulem1  23300  taylply2  23335  taylply  23336  dvtaylp  23337  dvntaylp0  23339  taylthlem2  23341  pserulm  23389  psercn2  23390  pserdvlem2  23395  abelthlem6  23403  abelthlem7  23405  abelthlem8  23406  advlogexp  23612  cxpeq  23709  log2tlbnd  23883  log2ublem2  23885  log2ub  23887  birthdaylem2  23890  birthdaylem3  23891  ftalem1  24009  ftalem5  24013  ftalem5OLD  24015  basellem2  24020  basellem3  24021  dvdsppwf1o  24127  musum  24132  sgmppw  24137  1sgmprm  24139  logexprlim  24165  mersenne  24167  lgseisenlem1  24289  dchrisum0flblem1  24358  pntpbnd2  24437  iseupa  25705  eupares  25715  bcm1n  28383  plymulx0  29448  signsplypnf  29451  signstres  29476  subfacval2  29922  subfaclim  29923  cvmliftlem7  30026  bccolsum  30387  poimirlem3  31955  poimirlem4  31956  poimirlem12  31964  poimirlem15  31967  poimirlem16  31968  poimirlem17  31969  poimirlem19  31971  poimirlem20  31972  poimirlem23  31975  poimirlem24  31976  poimirlem25  31977  poimirlem28  31980  poimirlem29  31981  poimirlem31  31983  iblmulc2nc  32019  jm2.22  35862  jm2.23  35863  hbt  36001  cnsrplycl  36045  hashgcdlem  36086  bcc0  36700  binomcxplemnn0  36709  binomcxplemfrat  36711  binomcxplemradcnv  36712  dvnmptdivc  37823  dvnmul  37828  dvnprodlem1  37831  dvnprodlem2  37832  dvnprodlem3  37833  iblsplit  37853  elaa2lem  38107  elaa2lemOLD  38108  etransclem2  38111  etransclem23  38132  etransclem28  38137  etransclem29  38138  etransclem32  38141  etransclem33  38142  etransclem35  38144  etransclem38  38147  etransclem39  38148  etransclem43  38152  etransclem44  38153  etransclem45  38154  etransclem46  38155  etransclem47  38156  etransclem48OLD  38157  etransclem48  38158  pfxmpt  38938  pfxlen  38942  addlenpfx  38949  pfxfv  38950  pfxswrd  38964  swrdpfx  38965  pfxpfx  38966  pfxpfxid  38967  pfxccat3  38977  pfxccatpfx1  38978  pfxccat3a  38980  repswpfx  38987  pfxco  38989  2elfz3nn0  39066  fz0addcom  39067  2elfz2melfz  39068  fz0addge0  39069  altgsumbc  40237  altgsumbcALT  40238  ply1mulgsumlem2  40283  ply1mulgsum  40286  nn0sumshdiglemA  40534  nn0sumshdiglemB  40535  aacllem  40644
  Copyright terms: Public domain W3C validator