Theorem elfznn0 13598

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5148  (class class class)co 7411  0cc0 11112   ≤ cle 11253  ℕ₀cn0 12476  ...cfz 13488

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-n0 12477  df-z 12563  df-uz 12827  df-fz 13489

This theorem is referenced by:  fz0ssnn0  13600  fz0fzdiffz0  13614  difelfzle  13618  bcrpcl  14272  bccmpl  14273  bcp1n  14280  bcp1nk  14281  bcval5  14282  permnn  14290  pfxmpt  14632  pfxfv  14636  pfxlen  14637  addlenpfx  14645  pfxswrd  14660  swrdpfx  14661  pfxpfx  14662  pfxpfxid  14663  swrdccatin1  14679  pfxccat3  14688  pfxccatpfx1  14690  pfxccat3a  14692  swrdccat3blem  14693  splfv2a  14710  repswpfx  14739  2cshwcshw  14780  cshwcsh2id  14783  pfxco  14793  binomlem  15779  binom1p  15781  binom1dif  15783  bcxmas  15785  climcnds  15801  arisum  15810  arisum2  15811  pwdif  15818  geolim  15820  geo2sum  15823  mertenslem1  15834  mertenslem2  15835  mertens  15836  risefacval2  15958  fallfacval2  15959  fallfacval3  15960  risefaccllem  15961  fallfaccllem  15962  risefacp1  15977  fallfacp1  15978  fallfacfwd  15984  binomfallfaclem1  15987  binomfallfaclem2  15988  binomrisefac  15990  bcfallfac  15992  bpolylem  15996  bpolysum  16001  bpolydiflem  16002  fsumkthpow  16004  bpoly4  16007  efcvgfsum  16033  efcj  16039  efaddlem  16040  effsumlt  16058  eirrlem  16151  3dvds  16278  pwp1fsum  16338  prmdiveq  16723  hashgcdlem  16725  pcbc  16837  vdwapf  16909  vdwlem2  16919  vdwlem6  16923  vdwlem8  16925  psgnunilem2  19404  efgcpbllemb  19664  srgbinomlem3  20122  srgbinomlem4  20123  srgbinomlem  20124  coe1mul2  22011  coe1tmmul2  22018  coe1tmmul  22019  cply1mul  22038  gsummoncoe1  22048  m2pmfzgsumcl  22470  decpmatmul  22494  pmatcollpw3fi1lem1  22508  mp2pm2mplem4  22531  pm2mpmhmlem2  22541  chpscmatgsumbin  22566  chpscmatgsummon  22567  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  cpmadugsumlemB  22596  cpmadugsumlemC  22597  cpmadugsumlemF  22598  cpmadugsumfi  22599  mbfi1fseqlem3  25459  mbfi1fseqlem4  25460  itg0  25521  itgz  25522  itgcl  25525  iblabsr  25571  iblmulc2  25572  itgsplit  25577  dvn2bss  25671  coe1mul3  25841  elply2  25934  plyf  25936  elplyd  25940  ply1termlem  25941  plyeq0lem  25948  plypf1  25950  plyaddlem1  25951  plymullem1  25952  plyaddlem  25953  plymullem  25954  coeeulem  25962  coeidlem  25975  coeid3  25978  plyco  25979  coeeq2  25980  dgreq  25982  coefv0  25986  coeaddlem  25987  coemullem  25988  coemulhi  25992  coemulc  25993  coe1termlem  25996  plycn  25999  plycjlem  26014  plycj  26015  plyrecj  26017  dvply1  26021  dvply2g  26022  vieta1lem2  26048  elqaalem2  26057  elqaalem3  26058  aareccl  26063  aalioulem1  26069  taylply2  26104  taylply  26105  dvtaylp  26106  dvntaylp0  26108  taylthlem2  26110  pserulm  26158  psercn2  26159  pserdvlem2  26164  abelthlem6  26172  abelthlem7  26174  abelthlem8  26175  advlogexp  26387  cxpeq  26489  log2tlbnd  26674  log2ublem2  26676  log2ub  26678  birthdaylem2  26681  birthdaylem3  26682  ftalem1  26801  ftalem5  26805  basellem2  26810  basellem3  26811  dvdsppwf1o  26914  musum  26919  sgmppw  26924  1sgmprm  26926  logexprlim  26952  mersenne  26954  lgseisenlem1  27102  dchrisum0flblem1  27235  pntpbnd2  27314  crctcshwlkn0  29330  bcm1n  32261  freshmansdream  32639  plymulx0  33844  signsplypnf  33847  signstres  33872  subfacval2  34464  subfaclim  34465  cvmliftlem7  34568  bccolsum  35001  gg-plycn  35463  gg-psercn2  35464  knoppcnlem7  35678  knoppcnlem8  35679  knoppndvlem5  35695  knoppndvlem11  35701  knoppndvlem14  35704  knoppndvlem15  35705  poimirlem3  36794  poimirlem4  36795  poimirlem12  36803  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem23  36814  poimirlem24  36815  poimirlem25  36816  poimirlem28  36819  poimirlem29  36820  poimirlem31  36822  iblmulc2nc  36856  lcmineqlem1  41200  lcmineqlem2  41201  lcmineqlem3  41202  lcmineqlem4  41203  lcmineqlem6  41205  jm2.22  42036  jm2.23  42037  hbt  42174  cnsrplycl  42211  bcc0  43401  binomcxplemnn0  43410  binomcxplemfrat  43412  binomcxplemradcnv  43413  dvnmptdivc  44953  dvnmul  44958  dvnprodlem1  44961  dvnprodlem2  44962  dvnprodlem3  44963  iblsplit  44981  elaa2lem  45248  etransclem2  45251  etransclem23  45272  etransclem28  45277  etransclem29  45278  etransclem32  45281  etransclem33  45282  etransclem35  45284  etransclem38  45287  etransclem39  45288  etransclem43  45292  etransclem44  45293  etransclem45  45294  etransclem46  45295  etransclem47  45296  etransclem48  45297  2elfz3nn0  46323  fz0addcom  46324  2elfz2melfz  46325  fz0addge0  46326  fmtnorec2lem  46509  fmtnodvds  46511  fmtnorec3  46515  lighneallem3  46574  lighneallem4b  46576  lighneallem4  46577  altgsumbc  47117  altgsumbcALT  47118  ply1mulgsumlem2  47156  ply1mulgsum  47159  nn0sumshdiglemA  47393  nn0sumshdiglemB  47394  aacllem  47936