Theorem elfznn0 13644

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  (class class class)co 7410  0cc0 11095   ≤ cle 11239  ℕ₀cn0 12499  ...cfz 13530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-n0 12500  df-z 12587  df-uz 12858  df-fz 13531

This theorem is referenced by:  fz0ssnn0  13646  fz0fzdiffz0  13661  difelfzle  13665  bcrpcl  14340  bccmpl  14341  bcp1n  14348  bcp1nk  14349  bcval5  14350  permnn  14358  pfxmpt  14712  pfxfv  14716  pfxlen  14717  addlenpfx  14724  pfxswrd  14739  swrdpfx  14740  pfxpfx  14741  pfxpfxid  14742  lenrevpfxcctswrd  14745  swrdccatin1  14758  pfxccat3  14767  pfxccatpfx1  14769  pfxccat3a  14771  swrdccat3blem  14772  splfv2a  14789  repswpfx  14818  2cshwcshw  14858  cshwcsh2id  14861  pfxco  14871  binomlem  15879  binom1p  15881  binom1dif  15883  bcxmas  15885  climcnds  15901  arisum  15910  arisum2  15911  pwdif  15918  geolim  15920  geo2sum  15923  mertenslem1  15934  mertenslem2  15935  mertens  15936  risefacval2  16060  fallfacval2  16061  fallfacval3  16062  risefaccllem  16063  fallfaccllem  16064  risefacp1  16078  fallfacp1  16079  fallfacfwd  16085  binomfallfaclem1  16088  binomfallfaclem2  16089  binomrisefac  16091  bcfallfac  16093  bpolylem  16097  bpolysum  16102  bpolydiflem  16103  fsumkthpow  16105  bpoly4  16108  efcvgfsum  16135  efcj  16141  efaddlem  16142  effsumlt  16162  eirrlem  16255  3dvds  16384  pwp1fsum  16444  prmdiveq  16840  hashgcdlem  16842  pcbc  16955  vdwapf  17027  vdwlem2  17037  vdwlem6  17041  vdwlem8  17043  psgnunilem2  19560  efgcpbllemb  19820  srgbinomlem3  20305  srgbinomlem4  20306  srgbinomlem  20307  freshmansdream  21724  coe1mul2  22430  coe1tmmul2  22437  coe1tmmul  22438  cply1mul  22456  gsummoncoe1  22468  m2pmfzgsumcl  22905  decpmatmul  22929  pmatcollpw3fi1lem1  22943  mp2pm2mplem4  22966  pm2mpmhmlem2  22976  chpscmatgsumbin  23001  chpscmatgsummon  23002  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  cpmadugsumlemB  23031  cpmadugsumlemC  23032  cpmadugsumlemF  23033  cpmadugsumfi  23034  mbfi1fseqlem3  25876  mbfi1fseqlem4  25877  itg0  25939  itgz  25940  itgcl  25943  iblabsr  25989  iblmulc2  25990  itgsplit  25995  dvn2bss  26089  coe1mul3  26256  elply2  26353  plyf  26355  elplyd  26359  ply1termlem  26360  plyeq0lem  26367  plypf1  26369  plyaddlem1  26370  plymullem1  26371  plyaddlem  26372  plymullem  26373  coeeulem  26381  coeidlem  26394  coeid3  26397  plyco  26398  coeeq2  26399  dgreq  26401  coefv0  26405  coeaddlem  26406  coemullem  26407  coemulhi  26411  coemulc  26412  coe1termlem  26415  plycn  26418  plycjlem  26433  plycj  26434  plycjOLD  26436  plyrecj  26438  plyn0mulidp  26442  dvply1  26445  dvply2g  26446  vieta1lem2  26472  elqaalem2  26481  elqaalem3  26482  aareccl  26489  aalioulem1  26495  taylply2  26531  taylply  26532  dvtaylp  26533  dvntaylp0  26535  taylthlem2  26537  pserulm  26585  psercn2  26586  pserdvlem2  26591  abelthlem6  26599  abelthlem7  26601  abelthlem8  26602  advlogexp  26820  cxpeq  26922  log2tlbnd  27110  log2ublem2  27112  log2ub  27114  birthdaylem2  27117  birthdaylem3  27118  ftalem1  27237  ftalem5  27241  basellem2  27246  basellem3  27247  dvdsppwf1o  27350  musum  27355  sgmppw  27361  1sgmprm  27363  logexprlim  27389  mersenne  27391  lgseisenlem1  27539  dchrisum0flblem1  27672  pntpbnd2  27751  crctcshwlkn0  30170  bcm1n  33140  gsummptrev  33376  gsummulsubdishift1  33388  esplyfv1  33959  esplyfv  33960  esplysply  33961  vietalem  33969  vieta  33970  signsplypnf  34937  signstres  34962  subfacval2  35679  subfaclim  35680  cvmliftlem7  35783  bccolsum  36231  knoppcnlem7  37088  knoppcnlem8  37089  knoppndvlem5  37105  knoppndvlem11  37111  knoppndvlem14  37114  knoppndvlem15  37115  poimirlem3  38274  poimirlem4  38275  poimirlem12  38283  poimirlem15  38286  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem23  38294  poimirlem24  38295  poimirlem25  38296  poimirlem28  38299  poimirlem29  38300  poimirlem31  38302  iblmulc2nc  38336  lcmineqlem1  42796  lcmineqlem2  42797  lcmineqlem3  42798  lcmineqlem4  42799  lcmineqlem6  42801  aks6d1c2lem3  42893  bcled  42945  jm2.22  43722  jm2.23  43723  hbt  43857  cnsrplycl  43894  bcc0  45050  binomcxplemnn0  45059  binomcxplemfrat  45061  binomcxplemradcnv  45062  dvnmptdivc  46652  dvnmul  46657  dvnprodlem1  46660  dvnprodlem2  46661  dvnprodlem3  46662  iblsplit  46680  elaa2lem  46947  etransclem2  46950  etransclem23  46971  etransclem28  46976  etransclem29  46977  etransclem32  46980  etransclem33  46981  etransclem35  46983  etransclem38  46986  etransclem39  46987  etransclem43  46991  etransclem44  46992  etransclem45  46993  etransclem46  46994  etransclem47  46995  etransclem48  46996  2elfz3nn0  48053  fz0addcom  48054  2elfz2melfz  48055  fz0addge0  48056  facnn0dvdsfac  48122  fmtnorec2lem  48294  fmtnodvds  48296  fmtnorec3  48300  lighneallem3  48359  lighneallem4b  48361  lighneallem4  48362  altgsumbc  49132  altgsumbcALT  49133  ply1mulgsumlem2  49167  ply1mulgsum  49170  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  aacllem  50621