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

Theorem elfznn0 12471
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 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)

Proof of Theorem elfznn0
StepHypRef Expression
1 elfz2nn0 12469 . 2 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁))
21simp1bi 1096 1 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030   class class class wbr 4685  (class class class)co 6690  0cc0 9974  cle 10113  0cn0 11330  ...cfz 12364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365
This theorem is referenced by:  fz0ssnn0  12473  fz0fzdiffz0  12487  difelfzle  12491  fzo0ssnn0OLD  12589  bcrpcl  13135  bccmpl  13136  bcp1n  13143  bcp1nk  13144  bcval5  13145  permnn  13153  swrd0len  13467  swrd0f  13473  swrd0fv  13485  swrd0swrd  13507  swrdswrd0  13508  swrd0swrd0  13509  swrd0swrdid  13510  wrdcctswrd  13511  swrdccat3  13538  swrdccat3a  13540  swrdccat3blem  13541  splfv2a  13553  2cshwcshw  13617  cshwcsh2id  13620  binomlem  14605  binom1p  14607  binom1dif  14609  bcxmas  14611  climcnds  14627  arisum  14636  arisum2  14637  pwm1geoser  14644  geolim  14645  geo2sum  14648  mertenslem1  14660  mertenslem2  14661  mertens  14662  risefacval2  14785  fallfacval2  14786  fallfacval3  14787  risefaccllem  14788  fallfaccllem  14789  risefacp1  14804  fallfacp1  14805  fallfacfwd  14811  binomfallfaclem1  14814  binomfallfaclem2  14815  binomrisefac  14817  bcfallfac  14819  bpolylem  14823  bpolysum  14828  bpolydiflem  14829  fsumkthpow  14831  bpoly4  14834  efcvgfsum  14860  efcj  14866  efaddlem  14867  effsumlt  14885  eirrlem  14976  3dvds  15099  3dvdsOLD  15100  pwp1fsum  15161  prmdiveq  15538  hashgcdlem  15540  pcbc  15651  vdwapf  15723  vdwlem2  15733  vdwlem6  15737  vdwlem8  15739  psgnunilem2  17961  efgcpbllemb  18214  srgbinomlem3  18588  srgbinomlem4  18589  srgbinomlem  18590  coe1mul2  19687  coe1tmmul2  19694  coe1tmmul  19695  cply1mul  19712  gsummoncoe1  19722  m2pmfzgsumcl  20601  decpmatmul  20625  pmatcollpw3fi1lem1  20639  mp2pm2mplem4  20662  pm2mpmhmlem2  20672  chpscmatgsumbin  20697  chpscmatgsummon  20698  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  cpmadugsumfi  20730  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  itg0  23591  itgz  23592  itgcl  23595  iblabsr  23641  iblmulc2  23642  itgsplit  23647  dvn2bss  23738  coe1mul3  23904  elply2  23997  plyf  23999  elplyd  24003  ply1termlem  24004  plyeq0lem  24011  plypf1  24013  plyaddlem1  24014  plymullem1  24015  plyaddlem  24016  plymullem  24017  coeeulem  24025  coeidlem  24038  coeid3  24041  plyco  24042  coeeq2  24043  dgreq  24045  coefv0  24049  coeaddlem  24050  coemullem  24051  coemulhi  24055  coemulc  24056  coe1termlem  24059  plycn  24062  plycjlem  24077  plycj  24078  plyrecj  24080  dvply1  24084  dvply2g  24085  vieta1lem2  24111  elqaalem2  24120  elqaalem3  24121  aareccl  24126  aalioulem1  24132  taylply2  24167  taylply  24168  dvtaylp  24169  dvntaylp0  24171  taylthlem2  24173  pserulm  24221  psercn2  24222  pserdvlem2  24227  abelthlem6  24235  abelthlem7  24237  abelthlem8  24238  advlogexp  24446  cxpeq  24543  log2tlbnd  24717  log2ublem2  24719  log2ub  24721  birthdaylem2  24724  birthdaylem3  24725  ftalem1  24844  ftalem5  24848  basellem2  24853  basellem3  24854  dvdsppwf1o  24957  musum  24962  sgmppw  24967  1sgmprm  24969  logexprlim  24995  mersenne  24997  lgseisenlem1  25145  dchrisum0flblem1  25242  pntpbnd2  25321  crctcshwlkn0  26769  bcm1n  29682  plymulx0  30752  signsplypnf  30755  signstres  30780  subfacval2  31295  subfaclim  31296  cvmliftlem7  31399  bccolsum  31751  knoppcnlem7  32614  knoppcnlem8  32615  knoppndvlem5  32632  knoppndvlem11  32638  knoppndvlem14  32641  knoppndvlem15  32642  poimirlem3  33542  poimirlem4  33543  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  iblmulc2nc  33605  jm2.22  37879  jm2.23  37880  hbt  38017  cnsrplycl  38054  bcc0  38856  binomcxplemnn0  38865  binomcxplemfrat  38867  binomcxplemradcnv  38868  dvnmptdivc  40471  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  iblsplit  40500  elaa2lem  40768  etransclem2  40771  etransclem23  40792  etransclem28  40797  etransclem29  40798  etransclem32  40801  etransclem33  40802  etransclem35  40804  etransclem38  40807  etransclem39  40808  etransclem43  40812  etransclem44  40813  etransclem45  40814  etransclem46  40815  etransclem47  40816  etransclem48  40817  2elfz3nn0  41651  fz0addcom  41652  2elfz2melfz  41653  fz0addge0  41654  pfxmpt  41712  pfxlen  41716  addlenpfx  41723  pfxfv  41724  pfxswrd  41738  swrdpfx  41739  pfxpfx  41740  pfxpfxid  41741  pfxccat3  41751  pfxccatpfx1  41752  pfxccat3a  41754  repswpfx  41761  pfxco  41763  fmtnorec2lem  41779  fmtnodvds  41781  fmtnorec3  41785  pwdif  41826  lighneallem3  41849  lighneallem4b  41851  lighneallem4  41852  altgsumbc  42455  altgsumbcALT  42456  ply1mulgsumlem2  42500  ply1mulgsum  42503  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739  aacllem  42875
  Copyright terms: Public domain W3C validator