Theorem elfznn0 13574

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5085  (class class class)co 7367  0cc0 11038   ≤ cle 11180  ℕ₀cn0 12437  ...cfz 13461

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525  df-uz 12789  df-fz 13462

This theorem is referenced by:  fz0ssnn0  13576  fz0fzdiffz0  13591  difelfzle  13595  bcrpcl  14270  bccmpl  14271  bcp1n  14278  bcp1nk  14279  bcval5  14280  permnn  14288  pfxmpt  14641  pfxfv  14645  pfxlen  14646  addlenpfx  14653  pfxswrd  14668  swrdpfx  14669  pfxpfx  14670  pfxpfxid  14671  lenrevpfxcctswrd  14674  swrdccatin1  14687  pfxccat3  14696  pfxccatpfx1  14698  pfxccat3a  14700  swrdccat3blem  14701  splfv2a  14718  repswpfx  14747  2cshwcshw  14787  cshwcsh2id  14790  pfxco  14800  binomlem  15794  binom1p  15796  binom1dif  15798  bcxmas  15800  climcnds  15816  arisum  15825  arisum2  15826  pwdif  15833  geolim  15835  geo2sum  15838  mertenslem1  15849  mertenslem2  15850  mertens  15851  risefacval2  15975  fallfacval2  15976  fallfacval3  15977  risefaccllem  15978  fallfaccllem  15979  risefacp1  15994  fallfacp1  15995  fallfacfwd  16001  binomfallfaclem1  16004  binomfallfaclem2  16005  binomrisefac  16007  bcfallfac  16009  bpolylem  16013  bpolysum  16018  bpolydiflem  16019  fsumkthpow  16021  bpoly4  16024  efcvgfsum  16051  efcj  16057  efaddlem  16058  effsumlt  16078  eirrlem  16171  3dvds  16300  pwp1fsum  16360  prmdiveq  16756  hashgcdlem  16758  pcbc  16871  vdwapf  16943  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  psgnunilem2  19470  efgcpbllemb  19730  srgbinomlem3  20209  srgbinomlem4  20210  srgbinomlem  20211  freshmansdream  21554  coe1mul2  22234  coe1tmmul2  22241  coe1tmmul  22242  cply1mul  22261  gsummoncoe1  22273  m2pmfzgsumcl  22713  decpmatmul  22737  pmatcollpw3fi1lem1  22751  mp2pm2mplem4  22774  pm2mpmhmlem2  22784  chpscmatgsumbin  22809  chpscmatgsummon  22810  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cpmadugsumfi  22842  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  itg0  25747  itgz  25748  itgcl  25751  iblabsr  25797  iblmulc2  25798  itgsplit  25803  dvn2bss  25897  coe1mul3  26064  elply2  26161  plyf  26163  elplyd  26167  ply1termlem  26168  plyeq0lem  26175  plypf1  26177  plyaddlem1  26178  plymullem1  26179  plyaddlem  26180  plymullem  26181  coeeulem  26189  coeidlem  26202  coeid3  26205  plyco  26206  coeeq2  26207  dgreq  26209  coefv0  26213  coeaddlem  26214  coemullem  26215  coemulhi  26219  coemulc  26220  coe1termlem  26223  plycn  26226  plycjlem  26241  plycj  26242  plycjOLD  26244  plyrecj  26246  dvply1  26250  dvply2g  26251  vieta1lem2  26277  elqaalem2  26286  elqaalem3  26287  aareccl  26292  aalioulem1  26298  taylply2  26333  taylply  26334  dvtaylp  26335  dvntaylp0  26337  taylthlem2  26339  pserulm  26387  psercn2  26388  pserdvlem2  26393  abelthlem6  26401  abelthlem7  26403  abelthlem8  26404  advlogexp  26619  cxpeq  26721  log2tlbnd  26909  log2ublem2  26911  log2ub  26913  birthdaylem2  26916  birthdaylem3  26917  ftalem1  27036  ftalem5  27040  basellem2  27045  basellem3  27046  dvdsppwf1o  27149  musum  27154  sgmppw  27160  1sgmprm  27162  logexprlim  27188  mersenne  27190  lgseisenlem1  27338  dchrisum0flblem1  27471  pntpbnd2  27550  crctcshwlkn0  29889  bcm1n  32868  gsummptrev  33117  gsummulsubdishift1  33129  esplyfv1  33713  esplyfv  33714  esplysply  33715  vietalem  33723  vieta  33724  plymulx0  34691  signsplypnf  34694  signstres  34719  subfacval2  35369  subfaclim  35370  cvmliftlem7  35473  bccolsum  35921  knoppcnlem7  36759  knoppcnlem8  36760  knoppndvlem5  36776  knoppndvlem11  36782  knoppndvlem14  36785  knoppndvlem15  36786  poimirlem3  37944  poimirlem4  37945  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  iblmulc2nc  38006  lcmineqlem1  42468  lcmineqlem2  42469  lcmineqlem3  42470  lcmineqlem4  42471  lcmineqlem6  42473  aks6d1c2lem3  42565  bcled  42617  jm2.22  43423  jm2.23  43424  hbt  43558  cnsrplycl  43595  bcc0  44767  binomcxplemnn0  44776  binomcxplemfrat  44778  binomcxplemradcnv  44779  dvnmptdivc  46366  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  iblsplit  46394  elaa2lem  46661  etransclem2  46664  etransclem23  46685  etransclem28  46690  etransclem29  46691  etransclem32  46694  etransclem33  46695  etransclem35  46697  etransclem38  46700  etransclem39  46701  etransclem43  46705  etransclem44  46706  etransclem45  46707  etransclem46  46708  etransclem47  46709  etransclem48  46710  2elfz3nn0  47764  fz0addcom  47765  2elfz2melfz  47766  fz0addge0  47767  facnn0dvdsfac  47833  fmtnorec2lem  48005  fmtnodvds  48007  fmtnorec3  48011  lighneallem3  48070  lighneallem4b  48072  lighneallem4  48073  altgsumbc  48828  altgsumbcALT  48829  ply1mulgsumlem2  48863  ply1mulgsum  48866  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  aacllem  50276