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

Theorem elfznn0 12983
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 12981 . 2 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁))
21simp1bi 1142 1 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115   class class class wbr 5039  (class class class)co 7130  0cc0 10514  cle 10653  0cn0 11875  ...cfz 12875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-om 7556  df-1st 7664  df-2nd 7665  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-er 8264  df-en 8485  df-dom 8486  df-sdom 8487  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-nn 11616  df-n0 11876  df-z 11960  df-uz 12222  df-fz 12876
This theorem is referenced by:  fz0ssnn0  12985  fz0fzdiffz0  12999  difelfzle  13003  bcrpcl  13652  bccmpl  13653  bcp1n  13660  bcp1nk  13661  bcval5  13662  permnn  13670  pfxmpt  14019  pfxfv  14023  pfxlen  14024  addlenpfx  14032  pfxswrd  14047  swrdpfx  14048  pfxpfx  14049  pfxpfxid  14050  swrdccatin1  14066  pfxccat3  14075  pfxccatpfx1  14077  pfxccat3a  14079  swrdccat3blem  14080  splfv2a  14097  repswpfx  14126  2cshwcshw  14166  cshwcsh2id  14169  pfxco  14179  binomlem  15163  binom1p  15165  binom1dif  15167  bcxmas  15169  climcnds  15185  arisum  15194  arisum2  15195  pwdif  15202  pwm1geoserOLD  15204  geolim  15205  geo2sum  15208  mertenslem1  15219  mertenslem2  15220  mertens  15221  risefacval2  15343  fallfacval2  15344  fallfacval3  15345  risefaccllem  15346  fallfaccllem  15347  risefacp1  15362  fallfacp1  15363  fallfacfwd  15369  binomfallfaclem1  15372  binomfallfaclem2  15373  binomrisefac  15375  bcfallfac  15377  bpolylem  15381  bpolysum  15386  bpolydiflem  15387  fsumkthpow  15389  bpoly4  15392  efcvgfsum  15418  efcj  15424  efaddlem  15425  effsumlt  15443  eirrlem  15536  3dvds  15659  pwp1fsum  15719  prmdiveq  16100  hashgcdlem  16102  pcbc  16213  vdwapf  16285  vdwlem2  16295  vdwlem6  16299  vdwlem8  16301  psgnunilem2  18601  efgcpbllemb  18859  srgbinomlem3  19270  srgbinomlem4  19271  srgbinomlem  19272  coe1mul2  20412  coe1tmmul2  20419  coe1tmmul  20420  cply1mul  20437  gsummoncoe1  20447  m2pmfzgsumcl  21331  decpmatmul  21355  pmatcollpw3fi1lem1  21369  mp2pm2mplem4  21392  pm2mpmhmlem2  21402  chpscmatgsumbin  21427  chpscmatgsummon  21428  chfacfscmulgsum  21443  chfacfpmmulgsum  21447  cpmadugsumlemB  21457  cpmadugsumlemC  21458  cpmadugsumlemF  21459  cpmadugsumfi  21460  mbfi1fseqlem3  24299  mbfi1fseqlem4  24300  itg0  24361  itgz  24362  itgcl  24365  iblabsr  24411  iblmulc2  24412  itgsplit  24417  dvn2bss  24511  coe1mul3  24678  elply2  24771  plyf  24773  elplyd  24777  ply1termlem  24778  plyeq0lem  24785  plypf1  24787  plyaddlem1  24788  plymullem1  24789  plyaddlem  24790  plymullem  24791  coeeulem  24799  coeidlem  24812  coeid3  24815  plyco  24816  coeeq2  24817  dgreq  24819  coefv0  24823  coeaddlem  24824  coemullem  24825  coemulhi  24829  coemulc  24830  coe1termlem  24833  plycn  24836  plycjlem  24851  plycj  24852  plyrecj  24854  dvply1  24858  dvply2g  24859  vieta1lem2  24885  elqaalem2  24894  elqaalem3  24895  aareccl  24900  aalioulem1  24906  taylply2  24941  taylply  24942  dvtaylp  24943  dvntaylp0  24945  taylthlem2  24947  pserulm  24995  psercn2  24996  pserdvlem2  25001  abelthlem6  25009  abelthlem7  25011  abelthlem8  25012  advlogexp  25224  cxpeq  25324  log2tlbnd  25509  log2ublem2  25511  log2ub  25513  birthdaylem2  25516  birthdaylem3  25517  ftalem1  25636  ftalem5  25640  basellem2  25645  basellem3  25646  dvdsppwf1o  25749  musum  25754  sgmppw  25759  1sgmprm  25761  logexprlim  25787  mersenne  25789  lgseisenlem1  25937  dchrisum0flblem1  26070  pntpbnd2  26149  crctcshwlkn0  27585  bcm1n  30504  freshmansdream  30866  plymulx0  31824  signsplypnf  31827  signstres  31852  subfacval2  32441  subfaclim  32442  cvmliftlem7  32545  bccolsum  32978  knoppcnlem7  33845  knoppcnlem8  33846  knoppndvlem5  33862  knoppndvlem11  33868  knoppndvlem14  33871  knoppndvlem15  33872  poimirlem3  34938  poimirlem4  34939  poimirlem12  34947  poimirlem15  34950  poimirlem16  34951  poimirlem17  34952  poimirlem19  34954  poimirlem20  34955  poimirlem23  34958  poimirlem24  34959  poimirlem25  34960  poimirlem28  34963  poimirlem29  34964  poimirlem31  34966  iblmulc2nc  35000  lcmineqlem1  39183  lcmineqlem2  39184  lcmineqlem3  39185  lcmineqlem4  39186  lcmineqlem6  39188  jm2.22  39731  jm2.23  39732  hbt  39869  cnsrplycl  39906  bcc0  40827  binomcxplemnn0  40836  binomcxplemfrat  40838  binomcxplemradcnv  40839  dvnmptdivc  42371  dvnmul  42376  dvnprodlem1  42379  dvnprodlem2  42380  dvnprodlem3  42381  iblsplit  42399  elaa2lem  42666  etransclem2  42669  etransclem23  42690  etransclem28  42695  etransclem29  42696  etransclem32  42699  etransclem33  42700  etransclem35  42702  etransclem38  42705  etransclem39  42706  etransclem43  42710  etransclem44  42711  etransclem45  42712  etransclem46  42713  etransclem47  42714  etransclem48  42715  2elfz3nn0  43664  fz0addcom  43665  2elfz2melfz  43666  fz0addge0  43667  fmtnorec2lem  43850  fmtnodvds  43852  fmtnorec3  43856  lighneallem3  43917  lighneallem4b  43919  lighneallem4  43920  altgsumbc  44545  altgsumbcALT  44546  ply1mulgsumlem2  44586  ply1mulgsum  44589  nn0sumshdiglemA  44824  nn0sumshdiglemB  44825  aacllem  45089
  Copyright terms: Public domain W3C validator