Theorem elfznn0 13625

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

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  (class class class)co 7396  0cc0 11073   ≤ cle 11217  ℕ₀cn0 12481  ...cfz 13512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-n0 12482  df-z 12569  df-uz 12840  df-fz 13513

This theorem is referenced by:  fz0ssnn0  13627  fz0fzdiffz0  13642  difelfzle  13646  bcrpcl  14321  bccmpl  14322  bcp1n  14329  bcp1nk  14330  bcval5  14331  permnn  14339  pfxmpt  14692  pfxfv  14696  pfxlen  14697  addlenpfx  14704  pfxswrd  14719  swrdpfx  14720  pfxpfx  14721  pfxpfxid  14722  lenrevpfxcctswrd  14725  swrdccatin1  14738  pfxccat3  14747  pfxccatpfx1  14749  pfxccat3a  14751  swrdccat3blem  14752  splfv2a  14769  repswpfx  14798  2cshwcshw  14838  cshwcsh2id  14841  pfxco  14851  binomlem  15859  binom1p  15861  binom1dif  15863  bcxmas  15865  climcnds  15881  arisum  15890  arisum2  15891  pwdif  15898  geolim  15900  geo2sum  15903  mertenslem1  15914  mertenslem2  15915  mertens  15916  risefacval2  16040  fallfacval2  16041  fallfacval3  16042  risefaccllem  16043  fallfaccllem  16044  risefacp1  16059  fallfacp1  16060  fallfacfwd  16066  binomfallfaclem1  16069  binomfallfaclem2  16070  binomrisefac  16072  bcfallfac  16074  bpolylem  16078  bpolysum  16083  bpolydiflem  16084  fsumkthpow  16086  bpoly4  16089  efcvgfsum  16116  efcj  16122  efaddlem  16123  effsumlt  16143  eirrlem  16236  3dvds  16365  pwp1fsum  16425  prmdiveq  16821  hashgcdlem  16823  pcbc  16936  vdwapf  17008  vdwlem2  17018  vdwlem6  17022  vdwlem8  17024  psgnunilem2  19535  efgcpbllemb  19795  srgbinomlem3  20278  srgbinomlem4  20279  srgbinomlem  20280  freshmansdream  21626  coe1mul2  22332  coe1tmmul2  22339  coe1tmmul  22340  cply1mul  22359  gsummoncoe1  22371  m2pmfzgsumcl  22808  decpmatmul  22832  pmatcollpw3fi1lem1  22846  mp2pm2mplem4  22869  pm2mpmhmlem2  22879  chpscmatgsumbin  22904  chpscmatgsummon  22905  chfacfscmulgsum  22920  chfacfpmmulgsum  22924  cpmadugsumlemB  22934  cpmadugsumlemC  22935  cpmadugsumlemF  22936  cpmadugsumfi  22937  mbfi1fseqlem3  25779  mbfi1fseqlem4  25780  itg0  25842  itgz  25843  itgcl  25846  iblabsr  25892  iblmulc2  25893  itgsplit  25898  dvn2bss  25992  coe1mul3  26159  elply2  26256  plyf  26258  elplyd  26262  ply1termlem  26263  plyeq0lem  26270  plypf1  26272  plyaddlem1  26273  plymullem1  26274  plyaddlem  26275  plymullem  26276  coeeulem  26284  coeidlem  26297  coeid3  26300  plyco  26301  coeeq2  26302  dgreq  26304  coefv0  26308  coeaddlem  26309  coemullem  26310  coemulhi  26314  coemulc  26315  coe1termlem  26318  plycn  26321  plycjlem  26336  plycj  26337  plycjOLD  26339  plyrecj  26341  plyn0mulidp  26345  dvply1  26348  dvply2g  26349  vieta1lem2  26375  elqaalem2  26384  elqaalem3  26385  aareccl  26390  aalioulem1  26396  taylply2  26431  taylply  26432  dvtaylp  26433  dvntaylp0  26435  taylthlem2  26437  pserulm  26485  psercn2  26486  pserdvlem2  26491  abelthlem6  26499  abelthlem7  26501  abelthlem8  26502  advlogexp  26720  cxpeq  26822  log2tlbnd  27010  log2ublem2  27012  log2ub  27014  birthdaylem2  27017  birthdaylem3  27018  ftalem1  27137  ftalem5  27141  basellem2  27146  basellem3  27147  dvdsppwf1o  27250  musum  27255  sgmppw  27261  1sgmprm  27263  logexprlim  27289  mersenne  27291  lgseisenlem1  27439  dchrisum0flblem1  27572  pntpbnd2  27651  crctcshwlkn0  30021  bcm1n  32997  gsummptrev  33236  gsummulsubdishift1  33248  esplyfv1  33866  esplyfv  33867  esplysply  33868  vietalem  33876  vieta  33877  signsplypnf  34844  signstres  34869  subfacval2  35537  subfaclim  35538  cvmliftlem7  35641  bccolsum  36089  knoppcnlem7  36937  knoppcnlem8  36938  knoppndvlem5  36954  knoppndvlem11  36960  knoppndvlem14  36963  knoppndvlem15  36964  poimirlem3  38122  poimirlem4  38123  poimirlem12  38131  poimirlem15  38134  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem23  38142  poimirlem24  38143  poimirlem25  38144  poimirlem28  38147  poimirlem29  38148  poimirlem31  38150  iblmulc2nc  38184  lcmineqlem1  42646  lcmineqlem2  42647  lcmineqlem3  42648  lcmineqlem4  42649  lcmineqlem6  42651  aks6d1c2lem3  42743  bcled  42795  jm2.22  43572  jm2.23  43573  hbt  43707  cnsrplycl  43744  bcc0  44916  binomcxplemnn0  44925  binomcxplemfrat  44927  binomcxplemradcnv  44928  dvnmptdivc  46512  dvnmul  46517  dvnprodlem1  46520  dvnprodlem2  46521  dvnprodlem3  46522  iblsplit  46540  elaa2lem  46807  etransclem2  46810  etransclem23  46831  etransclem28  46836  etransclem29  46837  etransclem32  46840  etransclem33  46841  etransclem35  46843  etransclem38  46846  etransclem39  46847  etransclem43  46851  etransclem44  46852  etransclem45  46853  etransclem46  46854  etransclem47  46855  etransclem48  46856  2elfz3nn0  47910  fz0addcom  47911  2elfz2melfz  47912  fz0addge0  47913  facnn0dvdsfac  47979  fmtnorec2lem  48151  fmtnodvds  48153  fmtnorec3  48157  lighneallem3  48216  lighneallem4b  48218  lighneallem4  48219  altgsumbc  48974  altgsumbcALT  48975  ply1mulgsumlem2  49009  ply1mulgsum  49012  nn0sumshdiglemA  49241  nn0sumshdiglemB  49242  aacllem  50422