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

Theorem elfznn0 12429
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 12427 . 2 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁))
21simp1bi 1075 1 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989   class class class wbr 4651  (class class class)co 6647  0cc0 9933  cle 10072  0cn0 11289  ...cfz 12323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-er 7739  df-en 7953  df-dom 7954  df-sdom 7955  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-nn 11018  df-n0 11290  df-z 11375  df-uz 11685  df-fz 12324
This theorem is referenced by:  fz0ssnn0  12431  fz0fzdiffz0  12444  difelfzle  12448  fzo0ssnn0OLD  12545  bcrpcl  13090  bccmpl  13091  bcp1n  13098  bcp1nk  13099  bcval5  13100  permnn  13108  swrd0len  13416  swrd0f  13421  swrd0fv  13433  swrd0swrd  13455  swrdswrd0  13456  swrd0swrd0  13457  swrd0swrdid  13458  wrdcctswrd  13459  swrdccat3  13486  swrdccat3a  13488  swrdccat3blem  13489  splfv2a  13501  2cshwcshw  13565  cshwcsh2id  13568  binomlem  14555  binom1p  14557  binom1dif  14559  bcxmas  14561  climcnds  14577  arisum  14586  arisum2  14587  pwm1geoser  14594  geolim  14595  geo2sum  14598  mertenslem1  14610  mertenslem2  14611  mertens  14612  risefacval2  14735  fallfacval2  14736  fallfacval3  14737  risefaccllem  14738  fallfaccllem  14739  risefacp1  14754  fallfacp1  14755  fallfacfwd  14761  binomfallfaclem1  14764  binomfallfaclem2  14765  binomrisefac  14767  bcfallfac  14769  bpolylem  14773  bpolysum  14778  bpolydiflem  14779  fsumkthpow  14781  bpoly4  14784  efcvgfsum  14810  efcj  14816  efaddlem  14817  effsumlt  14835  eirrlem  14926  3dvds  15046  3dvdsOLD  15047  pwp1fsum  15108  prmdiveq  15485  hashgcdlem  15487  pcbc  15598  vdwapf  15670  vdwlem2  15680  vdwlem6  15684  vdwlem8  15686  psgnunilem2  17909  efgcpbllemb  18162  srgbinomlem3  18536  srgbinomlem4  18537  srgbinomlem  18538  coe1mul2  19633  coe1tmmul2  19640  coe1tmmul  19641  cply1mul  19658  gsummoncoe1  19668  m2pmfzgsumcl  20547  decpmatmul  20571  pmatcollpw3fi1lem1  20585  mp2pm2mplem4  20608  pm2mpmhmlem2  20618  chpscmatgsumbin  20643  chpscmatgsummon  20644  chfacfscmulgsum  20659  chfacfpmmulgsum  20663  cpmadugsumlemB  20673  cpmadugsumlemC  20674  cpmadugsumlemF  20675  cpmadugsumfi  20676  mbfi1fseqlem3  23478  mbfi1fseqlem4  23479  itg0  23540  itgz  23541  itgcl  23544  iblabsr  23590  iblmulc2  23591  itgsplit  23596  dvn2bss  23687  coe1mul3  23853  elply2  23946  plyf  23948  elplyd  23952  ply1termlem  23953  plyeq0lem  23960  plypf1  23962  plyaddlem1  23963  plymullem1  23964  plyaddlem  23965  plymullem  23966  coeeulem  23974  coeidlem  23987  coeid3  23990  plyco  23991  coeeq2  23992  dgreq  23994  coefv0  23998  coeaddlem  23999  coemullem  24000  coemulhi  24004  coemulc  24005  coe1termlem  24008  plycn  24011  plycjlem  24026  plycj  24027  plyrecj  24029  dvply1  24033  dvply2g  24034  vieta1lem2  24060  elqaalem2  24069  elqaalem3  24070  aareccl  24075  aalioulem1  24081  taylply2  24116  taylply  24117  dvtaylp  24118  dvntaylp0  24120  taylthlem2  24122  pserulm  24170  psercn2  24171  pserdvlem2  24176  abelthlem6  24184  abelthlem7  24186  abelthlem8  24187  advlogexp  24395  cxpeq  24492  log2tlbnd  24666  log2ublem2  24668  log2ub  24670  birthdaylem2  24673  birthdaylem3  24674  ftalem1  24793  ftalem5  24797  basellem2  24802  basellem3  24803  dvdsppwf1o  24906  musum  24911  sgmppw  24916  1sgmprm  24918  logexprlim  24944  mersenne  24946  lgseisenlem1  25094  dchrisum0flblem1  25191  pntpbnd2  25270  crctcshwlkn0  26707  bcm1n  29539  plymulx0  30609  signsplypnf  30612  signstres  30637  subfacval2  31154  subfaclim  31155  cvmliftlem7  31258  bccolsum  31611  knoppcnlem7  32473  knoppcnlem8  32474  knoppndvlem5  32491  knoppndvlem11  32497  knoppndvlem14  32500  knoppndvlem15  32501  poimirlem3  33392  poimirlem4  33393  poimirlem12  33401  poimirlem15  33404  poimirlem16  33405  poimirlem17  33406  poimirlem19  33408  poimirlem20  33409  poimirlem23  33412  poimirlem24  33413  poimirlem25  33414  poimirlem28  33417  poimirlem29  33418  poimirlem31  33420  iblmulc2nc  33455  jm2.22  37388  jm2.23  37389  hbt  37526  cnsrplycl  37563  bcc0  38365  binomcxplemnn0  38374  binomcxplemfrat  38376  binomcxplemradcnv  38377  dvnmptdivc  39922  dvnmul  39927  dvnprodlem1  39930  dvnprodlem2  39931  dvnprodlem3  39932  iblsplit  39951  elaa2lem  40219  etransclem2  40222  etransclem23  40243  etransclem28  40248  etransclem29  40249  etransclem32  40252  etransclem33  40253  etransclem35  40255  etransclem38  40258  etransclem39  40259  etransclem43  40263  etransclem44  40264  etransclem45  40265  etransclem46  40266  etransclem47  40267  etransclem48  40268  2elfz3nn0  41095  fz0addcom  41096  2elfz2melfz  41097  fz0addge0  41098  pfxmpt  41158  pfxlen  41162  addlenpfx  41169  pfxfv  41170  pfxswrd  41184  swrdpfx  41185  pfxpfx  41186  pfxpfxid  41187  pfxccat3  41197  pfxccatpfx1  41198  pfxccat3a  41200  repswpfx  41207  pfxco  41209  fmtnorec2lem  41225  fmtnodvds  41227  fmtnorec3  41231  pwdif  41272  lighneallem3  41295  lighneallem4b  41297  lighneallem4  41298  altgsumbc  41901  altgsumbcALT  41902  ply1mulgsumlem2  41946  ply1mulgsum  41949  nn0sumshdiglemA  42184  nn0sumshdiglemB  42185  aacllem  42318
  Copyright terms: Public domain W3C validator