Theorem elfznn0 13565

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

Step	Hyp	Ref	Expression
1		elfz2nn0 13563	. 2 ⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁))
2	1	simp1bi 1151	1 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5072  (class class class)co 7356  0cc0 11029   ≤ cle 11171  ℕ₀cn0 12428  ...cfz 13452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780  df-fz 13453

This theorem is referenced by:  fz0ssnn0  13567  fz0fzdiffz0  13582  difelfzle  13586  bcrpcl  14261  bccmpl  14262  bcp1n  14269  bcp1nk  14270  bcval5  14271  permnn  14279  pfxmpt  14632  pfxfv  14636  pfxlen  14637  addlenpfx  14644  pfxswrd  14659  swrdpfx  14660  pfxpfx  14661  pfxpfxid  14662  lenrevpfxcctswrd  14665  swrdccatin1  14678  pfxccat3  14687  pfxccatpfx1  14689  pfxccat3a  14691  swrdccat3blem  14692  splfv2a  14709  repswpfx  14738  2cshwcshw  14778  cshwcsh2id  14781  pfxco  14791  binomlem  15785  binom1p  15787  binom1dif  15789  bcxmas  15791  climcnds  15807  arisum  15816  arisum2  15817  pwdif  15824  geolim  15826  geo2sum  15829  mertenslem1  15840  mertenslem2  15841  mertens  15842  risefacval2  15966  fallfacval2  15967  fallfacval3  15968  risefaccllem  15969  fallfaccllem  15970  risefacp1  15985  fallfacp1  15986  fallfacfwd  15992  binomfallfaclem1  15995  binomfallfaclem2  15996  binomrisefac  15998  bcfallfac  16000  bpolylem  16004  bpolysum  16009  bpolydiflem  16010  fsumkthpow  16012  bpoly4  16015  efcvgfsum  16042  efcj  16048  efaddlem  16049  effsumlt  16069  eirrlem  16162  3dvds  16291  pwp1fsum  16351  prmdiveq  16747  hashgcdlem  16749  pcbc  16862  vdwapf  16934  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  psgnunilem2  19461  efgcpbllemb  19721  srgbinomlem3  20200  srgbinomlem4  20201  srgbinomlem  20202  freshmansdream  21549  coe1mul2  22255  coe1tmmul2  22262  coe1tmmul  22263  cply1mul  22282  gsummoncoe1  22294  m2pmfzgsumcl  22731  decpmatmul  22755  pmatcollpw3fi1lem1  22769  mp2pm2mplem4  22792  pm2mpmhmlem2  22802  chpscmatgsumbin  22827  chpscmatgsummon  22828  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  cpmadugsumlemB  22857  cpmadugsumlemC  22858  cpmadugsumlemF  22859  cpmadugsumfi  22860  mbfi1fseqlem3  25702  mbfi1fseqlem4  25703  itg0  25765  itgz  25766  itgcl  25769  iblabsr  25815  iblmulc2  25816  itgsplit  25821  dvn2bss  25915  coe1mul3  26082  elply2  26179  plyf  26181  elplyd  26185  ply1termlem  26186  plyeq0lem  26193  plypf1  26195  plyaddlem1  26196  plymullem1  26197  plyaddlem  26198  plymullem  26199  coeeulem  26207  coeidlem  26220  coeid3  26223  plyco  26224  coeeq2  26225  dgreq  26227  coefv0  26231  coeaddlem  26232  coemullem  26233  coemulhi  26237  coemulc  26238  coe1termlem  26241  plycn  26244  plycjlem  26259  plycj  26260  plycjOLD  26262  plyrecj  26264  dvply1  26268  dvply2g  26269  vieta1lem2  26295  elqaalem2  26304  elqaalem3  26305  aareccl  26310  aalioulem1  26316  taylply2  26351  taylply  26352  dvtaylp  26353  dvntaylp0  26355  taylthlem2  26357  pserulm  26405  psercn2  26406  pserdvlem2  26411  abelthlem6  26419  abelthlem7  26421  abelthlem8  26422  advlogexp  26637  cxpeq  26739  log2tlbnd  26927  log2ublem2  26929  log2ub  26931  birthdaylem2  26934  birthdaylem3  26935  ftalem1  27054  ftalem5  27058  basellem2  27063  basellem3  27064  dvdsppwf1o  27167  musum  27172  sgmppw  27178  1sgmprm  27180  logexprlim  27206  mersenne  27208  lgseisenlem1  27356  dchrisum0flblem1  27489  pntpbnd2  27568  crctcshwlkn0  29907  bcm1n  32887  gsummptrev  33137  gsummulsubdishift1  33149  esplyfv1  33753  esplyfv  33754  esplysply  33755  vietalem  33763  vieta  33764  plymulx0  34731  signsplypnf  34734  signstres  34759  subfacval2  35415  subfaclim  35416  cvmliftlem7  35519  bccolsum  35967  knoppcnlem7  36805  knoppcnlem8  36806  knoppndvlem5  36822  knoppndvlem11  36828  knoppndvlem14  36831  knoppndvlem15  36832  poimirlem3  37990  poimirlem4  37991  poimirlem12  37999  poimirlem15  38002  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem28  38015  poimirlem29  38016  poimirlem31  38018  iblmulc2nc  38052  lcmineqlem1  42514  lcmineqlem2  42515  lcmineqlem3  42516  lcmineqlem4  42517  lcmineqlem6  42519  aks6d1c2lem3  42611  bcled  42663  jm2.22  43440  jm2.23  43441  hbt  43575  cnsrplycl  43612  bcc0  44784  binomcxplemnn0  44793  binomcxplemfrat  44795  binomcxplemradcnv  44796  dvnmptdivc  46381  dvnmul  46386  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  iblsplit  46409  elaa2lem  46676  etransclem2  46679  etransclem23  46700  etransclem28  46705  etransclem29  46706  etransclem32  46709  etransclem33  46710  etransclem35  46712  etransclem38  46715  etransclem39  46716  etransclem43  46720  etransclem44  46721  etransclem45  46722  etransclem46  46723  etransclem47  46724  etransclem48  46725  2elfz3nn0  47779  fz0addcom  47780  2elfz2melfz  47781  fz0addge0  47782  facnn0dvdsfac  47848  fmtnorec2lem  48020  fmtnodvds  48022  fmtnorec3  48026  lighneallem3  48085  lighneallem4b  48087  lighneallem4  48088  altgsumbc  48843  altgsumbcALT  48844  ply1mulgsumlem2  48878  ply1mulgsum  48881  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  aacllem  50291