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

Theorem elfznn0 11888
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 11886 . 2  |-  ( K  e.  ( 0 ... N )  <->  ( K  e.  NN0  /\  N  e. 
NN0  /\  K  <_  N ) )
21simp1bi 1020 1  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   class class class wbr 4420  (class class class)co 6302   0cc0 9540    <_ cle 9677   NN0cn0 10870   ...cfz 11785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-om 6704  df-1st 6804  df-2nd 6805  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-nn 10611  df-n0 10871  df-z 10939  df-uz 11161  df-fz 11786
This theorem is referenced by:  fz0fzdiffz0  11900  difelfzle  11905  fzo0ssnn0  11994  bcrpcl  12493  bccmpl  12494  bcp1n  12501  bcp1nk  12502  bcval5  12503  permnn  12511  swrd0len  12769  swrd0f  12774  swrd0fv  12786  swrd0swrd  12808  swrdswrd0  12809  swrd0swrd0  12810  swrd0swrdid  12811  wrdcctswrd  12812  swrdccat3  12839  swrdccat3a  12841  swrdccat3blem  12842  splfv2a  12854  2cshwcshw  12915  cshwcsh2id  12918  binomlem  13875  binom1p  13877  binom1dif  13879  bcxmas  13881  climcnds  13897  arisum  13906  arisum2  13907  geolim  13914  geo2sum  13917  mertenslem1  13928  mertenslem2  13929  mertens  13930  risefacval2  14051  fallfacval2  14052  fallfacval3  14053  risefaccllem  14054  fallfaccllem  14055  risefacp1  14070  fallfacp1  14071  fallfacfwd  14077  binomfallfaclem1  14080  binomfallfaclem2  14081  binomrisefac  14083  bcfallfac  14085  bpolylem  14089  bpolysum  14094  bpolydiflem  14095  fsumkthpow  14097  bpoly4  14100  efcvgfsum  14128  efcj  14134  efaddlem  14135  effsumlt  14153  eirrlem  14244  3dvds  14357  prmdiveq  14722  pcbc  14833  vdwapf  14910  vdwlem2  14920  vdwlem6  14924  vdwlem8  14926  psgnunilem2  17124  efgcpbllemb  17393  gsummptnn0fz  17603  srgbinomlem3  17763  srgbinomlem4  17764  srgbinomlem  17765  psrbaglefi  18584  coe1mul2lem2  18849  coe1mul2  18850  coe1tmmul2  18857  coe1tmmul  18858  cply1mul  18875  gsummoncoe1  18886  m2pmfzgsumcl  19759  decpmatmul  19783  pmatcollpw3fi1lem1  19797  mp2pm2mplem4  19820  pm2mpmhmlem2  19830  chpscmatgsumbin  19855  chpscmatgsummon  19856  chfacfscmulgsum  19871  chfacfpmmulgsum  19875  cpmadugsumlemB  19885  cpmadugsumlemC  19886  cpmadugsumlemF  19887  cpmadugsumfi  19888  mbfi1fseqlem3  22662  mbfi1fseqlem4  22663  itg0  22724  itgz  22725  itgcl  22728  iblabsr  22774  iblmulc2  22775  itgsplit  22780  dvn2bss  22871  coe1mul3  23035  elply2  23137  plyf  23139  elplyd  23143  ply1termlem  23144  plyeq0lem  23151  plypf1  23153  plyaddlem1  23154  plymullem1  23155  plyaddlem  23156  plymullem  23157  coeeulem  23165  coeidlem  23178  coeid3  23181  plyco  23182  coeeq2  23183  dgreq  23185  coefv0  23189  coeaddlem  23190  coemullem  23191  coemulhi  23195  coemulc  23196  coe1termlem  23199  plycn  23202  plycjlem  23217  plycj  23218  plyrecj  23220  dvply1  23224  dvply2g  23225  vieta1lem2  23251  elqaalem2  23260  elqaalem3  23261  elqaalem2OLD  23263  elqaalem3OLD  23264  aareccl  23269  aannenlem1  23271  aalioulem1  23275  taylply2  23310  taylply  23311  dvtaylp  23312  dvntaylp0  23314  taylthlem2  23316  pserulm  23364  psercn2  23365  pserdvlem2  23370  abelthlem6  23378  abelthlem7  23380  abelthlem8  23381  advlogexp  23587  cxpeq  23684  log2tlbnd  23858  log2ublem2  23860  log2ub  23862  birthdaylem2  23865  birthdaylem3  23866  ftalem1  23984  ftalem5  23988  ftalem5OLD  23990  basellem2  23995  basellem3  23996  dvdsppwf1o  24102  musum  24107  sgmppw  24112  1sgmprm  24114  logexprlim  24140  mersenne  24142  lgseisenlem1  24264  dchrisum0flblem1  24333  pntpbnd2  24412  iseupa  25679  eupares  25689  bcm1n  28365  plymulx0  29432  signsplypnf  29435  signstres  29460  subfacval2  29906  subfaclim  29907  cvmliftlem7  30010  bccolsum  30370  poimirlem3  31857  poimirlem4  31858  poimirlem12  31866  poimirlem15  31869  poimirlem16  31870  poimirlem17  31871  poimirlem19  31873  poimirlem20  31874  poimirlem23  31877  poimirlem24  31878  poimirlem25  31879  poimirlem28  31882  poimirlem29  31883  poimirlem31  31885  iblmulc2nc  31921  jm2.22  35770  jm2.23  35771  hbt  35909  cnsrplycl  35953  hashgcdlem  35994  bcc0  36547  binomcxplemnn0  36556  binomcxplemfrat  36558  binomcxplemradcnv  36559  dvnmptdivc  37633  dvnmul  37638  dvnprodlem1  37641  dvnprodlem2  37642  dvnprodlem3  37643  iblsplit  37663  elaa2lem  37917  elaa2lemOLD  37918  etransclem2  37921  etransclem23  37942  etransclem28  37947  etransclem29  37948  etransclem32  37951  etransclem33  37952  etransclem35  37954  etransclem38  37957  etransclem39  37958  etransclem43  37962  etransclem44  37963  etransclem45  37964  etransclem46  37965  etransclem47  37966  etransclem48OLD  37967  etransclem48  37968  pfxmpt  38640  pfxlen  38644  addlenpfx  38651  pfxfv  38652  pfxswrd  38666  swrdpfx  38667  pfxpfx  38668  pfxpfxid  38669  pfxccat3  38679  pfxccatpfx1  38680  pfxccat3a  38682  repswpfx  38689  pfxco  38691  2elfz3nn0  38745  fz0addcom  38746  2elfz2melfz  38747  fz0addge0  38748  altgsumbc  39407  altgsumbcALT  39408  ply1mulgsumlem2  39453  ply1mulgsum  39456  nn0sumshdiglemA  39704  nn0sumshdiglemB  39705  aacllem  39814
  Copyright terms: Public domain W3C validator