Theorem elfznn0 13349

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 13347	. 2 ⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁))
2	1	simp1bi 1144	1 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5074  (class class class)co 7275  0cc0 10871   ≤ cle 11010  ℕ₀cn0 12233  ...cfz 13239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240

This theorem is referenced by:  fz0ssnn0  13351  fz0fzdiffz0  13365  difelfzle  13369  bcrpcl  14022  bccmpl  14023  bcp1n  14030  bcp1nk  14031  bcval5  14032  permnn  14040  pfxmpt  14391  pfxfv  14395  pfxlen  14396  addlenpfx  14404  pfxswrd  14419  swrdpfx  14420  pfxpfx  14421  pfxpfxid  14422  swrdccatin1  14438  pfxccat3  14447  pfxccatpfx1  14449  pfxccat3a  14451  swrdccat3blem  14452  splfv2a  14469  repswpfx  14498  2cshwcshw  14538  cshwcsh2id  14541  pfxco  14551  binomlem  15541  binom1p  15543  binom1dif  15545  bcxmas  15547  climcnds  15563  arisum  15572  arisum2  15573  pwdif  15580  geolim  15582  geo2sum  15585  mertenslem1  15596  mertenslem2  15597  mertens  15598  risefacval2  15720  fallfacval2  15721  fallfacval3  15722  risefaccllem  15723  fallfaccllem  15724  risefacp1  15739  fallfacp1  15740  fallfacfwd  15746  binomfallfaclem1  15749  binomfallfaclem2  15750  binomrisefac  15752  bcfallfac  15754  bpolylem  15758  bpolysum  15763  bpolydiflem  15764  fsumkthpow  15766  bpoly4  15769  efcvgfsum  15795  efcj  15801  efaddlem  15802  effsumlt  15820  eirrlem  15913  3dvds  16040  pwp1fsum  16100  prmdiveq  16487  hashgcdlem  16489  pcbc  16601  vdwapf  16673  vdwlem2  16683  vdwlem6  16687  vdwlem8  16689  psgnunilem2  19103  efgcpbllemb  19361  srgbinomlem3  19778  srgbinomlem4  19779  srgbinomlem  19780  coe1mul2  21440  coe1tmmul2  21447  coe1tmmul  21448  cply1mul  21465  gsummoncoe1  21475  m2pmfzgsumcl  21897  decpmatmul  21921  pmatcollpw3fi1lem1  21935  mp2pm2mplem4  21958  pm2mpmhmlem2  21968  chpscmatgsumbin  21993  chpscmatgsummon  21994  chfacfscmulgsum  22009  chfacfpmmulgsum  22013  cpmadugsumlemB  22023  cpmadugsumlemC  22024  cpmadugsumlemF  22025  cpmadugsumfi  22026  mbfi1fseqlem3  24882  mbfi1fseqlem4  24883  itg0  24944  itgz  24945  itgcl  24948  iblabsr  24994  iblmulc2  24995  itgsplit  25000  dvn2bss  25094  coe1mul3  25264  elply2  25357  plyf  25359  elplyd  25363  ply1termlem  25364  plyeq0lem  25371  plypf1  25373  plyaddlem1  25374  plymullem1  25375  plyaddlem  25376  plymullem  25377  coeeulem  25385  coeidlem  25398  coeid3  25401  plyco  25402  coeeq2  25403  dgreq  25405  coefv0  25409  coeaddlem  25410  coemullem  25411  coemulhi  25415  coemulc  25416  coe1termlem  25419  plycn  25422  plycjlem  25437  plycj  25438  plyrecj  25440  dvply1  25444  dvply2g  25445  vieta1lem2  25471  elqaalem2  25480  elqaalem3  25481  aareccl  25486  aalioulem1  25492  taylply2  25527  taylply  25528  dvtaylp  25529  dvntaylp0  25531  taylthlem2  25533  pserulm  25581  psercn2  25582  pserdvlem2  25587  abelthlem6  25595  abelthlem7  25597  abelthlem8  25598  advlogexp  25810  cxpeq  25910  log2tlbnd  26095  log2ublem2  26097  log2ub  26099  birthdaylem2  26102  birthdaylem3  26103  ftalem1  26222  ftalem5  26226  basellem2  26231  basellem3  26232  dvdsppwf1o  26335  musum  26340  sgmppw  26345  1sgmprm  26347  logexprlim  26373  mersenne  26375  lgseisenlem1  26523  dchrisum0flblem1  26656  pntpbnd2  26735  crctcshwlkn0  28186  bcm1n  31116  freshmansdream  31484  plymulx0  32526  signsplypnf  32529  signstres  32554  subfacval2  33149  subfaclim  33150  cvmliftlem7  33253  bccolsum  33705  knoppcnlem7  34679  knoppcnlem8  34680  knoppndvlem5  34696  knoppndvlem11  34702  knoppndvlem14  34705  knoppndvlem15  34706  poimirlem3  35780  poimirlem4  35781  poimirlem12  35789  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem20  35797  poimirlem23  35800  poimirlem24  35801  poimirlem25  35802  poimirlem28  35805  poimirlem29  35806  poimirlem31  35808  iblmulc2nc  35842  lcmineqlem1  40037  lcmineqlem2  40038  lcmineqlem3  40039  lcmineqlem4  40040  lcmineqlem6  40042  jm2.22  40817  jm2.23  40818  hbt  40955  cnsrplycl  40992  bcc0  41958  binomcxplemnn0  41967  binomcxplemfrat  41969  binomcxplemradcnv  41970  dvnmptdivc  43479  dvnmul  43484  dvnprodlem1  43487  dvnprodlem2  43488  dvnprodlem3  43489  iblsplit  43507  elaa2lem  43774  etransclem2  43777  etransclem23  43798  etransclem28  43803  etransclem29  43804  etransclem32  43807  etransclem33  43808  etransclem35  43810  etransclem38  43813  etransclem39  43814  etransclem43  43818  etransclem44  43819  etransclem45  43820  etransclem46  43821  etransclem47  43822  etransclem48  43823  2elfz3nn0  44808  fz0addcom  44809  2elfz2melfz  44810  fz0addge0  44811  fmtnorec2lem  44994  fmtnodvds  44996  fmtnorec3  45000  lighneallem3  45059  lighneallem4b  45061  lighneallem4  45062  altgsumbc  45688  altgsumbcALT  45689  ply1mulgsumlem2  45728  ply1mulgsum  45731  nn0sumshdiglemA  45965  nn0sumshdiglemB  45966  aacllem  46505