Theorem elfznn0 13568

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  (class class class)co 7361  0cc0 11032   ≤ cle 11174  ℕ₀cn0 12431  ...cfz 13455

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432  df-z 12519  df-uz 12783  df-fz 13456

This theorem is referenced by:  fz0ssnn0  13570  fz0fzdiffz0  13585  difelfzle  13589  bcrpcl  14264  bccmpl  14265  bcp1n  14272  bcp1nk  14273  bcval5  14274  permnn  14282  pfxmpt  14635  pfxfv  14639  pfxlen  14640  addlenpfx  14647  pfxswrd  14662  swrdpfx  14663  pfxpfx  14664  pfxpfxid  14665  lenrevpfxcctswrd  14668  swrdccatin1  14681  pfxccat3  14690  pfxccatpfx1  14692  pfxccat3a  14694  swrdccat3blem  14695  splfv2a  14712  repswpfx  14741  2cshwcshw  14781  cshwcsh2id  14784  pfxco  14794  binomlem  15788  binom1p  15790  binom1dif  15792  bcxmas  15794  climcnds  15810  arisum  15819  arisum2  15820  pwdif  15827  geolim  15829  geo2sum  15832  mertenslem1  15843  mertenslem2  15844  mertens  15845  risefacval2  15969  fallfacval2  15970  fallfacval3  15971  risefaccllem  15972  fallfaccllem  15973  risefacp1  15988  fallfacp1  15989  fallfacfwd  15995  binomfallfaclem1  15998  binomfallfaclem2  15999  binomrisefac  16001  bcfallfac  16003  bpolylem  16007  bpolysum  16012  bpolydiflem  16013  fsumkthpow  16015  bpoly4  16018  efcvgfsum  16045  efcj  16051  efaddlem  16052  effsumlt  16072  eirrlem  16165  3dvds  16294  pwp1fsum  16354  prmdiveq  16750  hashgcdlem  16752  pcbc  16865  vdwapf  16937  vdwlem2  16947  vdwlem6  16951  vdwlem8  16953  psgnunilem2  19464  efgcpbllemb  19724  srgbinomlem3  20203  srgbinomlem4  20204  srgbinomlem  20205  freshmansdream  21567  coe1mul2  22247  coe1tmmul2  22254  coe1tmmul  22255  cply1mul  22274  gsummoncoe1  22286  m2pmfzgsumcl  22726  decpmatmul  22750  pmatcollpw3fi1lem1  22764  mp2pm2mplem4  22787  pm2mpmhmlem2  22797  chpscmatgsumbin  22822  chpscmatgsummon  22823  chfacfscmulgsum  22838  chfacfpmmulgsum  22842  cpmadugsumlemB  22852  cpmadugsumlemC  22853  cpmadugsumlemF  22854  cpmadugsumfi  22855  mbfi1fseqlem3  25697  mbfi1fseqlem4  25698  itg0  25760  itgz  25761  itgcl  25764  iblabsr  25810  iblmulc2  25811  itgsplit  25816  dvn2bss  25910  coe1mul3  26077  elply2  26174  plyf  26176  elplyd  26180  ply1termlem  26181  plyeq0lem  26188  plypf1  26190  plyaddlem1  26191  plymullem1  26192  plyaddlem  26193  plymullem  26194  coeeulem  26202  coeidlem  26215  coeid3  26218  plyco  26219  coeeq2  26220  dgreq  26222  coefv0  26226  coeaddlem  26227  coemullem  26228  coemulhi  26232  coemulc  26233  coe1termlem  26236  plycn  26239  plycjlem  26254  plycj  26255  plycjOLD  26257  plyrecj  26259  dvply1  26263  dvply2g  26264  dvply2gOLD  26265  vieta1lem2  26291  elqaalem2  26300  elqaalem3  26301  aareccl  26306  aalioulem1  26312  taylply2  26347  taylply2OLD  26348  taylply  26349  dvtaylp  26350  dvntaylp0  26352  taylthlem2  26354  taylthlem2OLD  26355  pserulm  26403  psercn2  26404  pserdvlem2  26409  abelthlem6  26417  abelthlem7  26419  abelthlem8  26420  advlogexp  26635  cxpeq  26737  log2tlbnd  26925  log2ublem2  26927  log2ub  26929  birthdaylem2  26932  birthdaylem3  26933  ftalem1  27053  ftalem5  27057  basellem2  27062  basellem3  27063  dvdsppwf1o  27166  musum  27171  sgmppw  27177  1sgmprm  27179  logexprlim  27205  mersenne  27207  lgseisenlem1  27355  dchrisum0flblem1  27488  pntpbnd2  27567  crctcshwlkn0  29907  bcm1n  32886  gsummptrev  33135  gsummulsubdishift1  33147  esplyfv1  33731  esplyfv  33732  esplysply  33733  vietalem  33741  vieta  33742  plymulx0  34710  signsplypnf  34713  signstres  34738  subfacval2  35388  subfaclim  35389  cvmliftlem7  35492  bccolsum  35940  knoppcnlem7  36778  knoppcnlem8  36779  knoppndvlem5  36795  knoppndvlem11  36801  knoppndvlem14  36804  knoppndvlem15  36805  poimirlem3  37961  poimirlem4  37962  poimirlem12  37970  poimirlem15  37973  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem23  37981  poimirlem24  37982  poimirlem25  37983  poimirlem28  37986  poimirlem29  37987  poimirlem31  37989  iblmulc2nc  38023  lcmineqlem1  42485  lcmineqlem2  42486  lcmineqlem3  42487  lcmineqlem4  42488  lcmineqlem6  42490  aks6d1c2lem3  42582  bcled  42634  jm2.22  43444  jm2.23  43445  hbt  43579  cnsrplycl  43616  bcc0  44788  binomcxplemnn0  44797  binomcxplemfrat  44799  binomcxplemradcnv  44800  dvnmptdivc  46387  dvnmul  46392  dvnprodlem1  46395  dvnprodlem2  46396  dvnprodlem3  46397  iblsplit  46415  elaa2lem  46682  etransclem2  46685  etransclem23  46706  etransclem28  46711  etransclem29  46712  etransclem32  46715  etransclem33  46716  etransclem35  46718  etransclem38  46721  etransclem39  46722  etransclem43  46726  etransclem44  46727  etransclem45  46728  etransclem46  46729  etransclem47  46730  etransclem48  46731  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