Theorem elfznn0 13647

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  (class class class)co 7411  0cc0 11099   ≤ cle 11243  ℕ₀cn0 12503  ...cfz 13534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-n0 12504  df-z 12591  df-uz 12862  df-fz 13535

This theorem is referenced by:  fz0ssnn0  13649  fz0fzdiffz0  13664  difelfzle  13668  bcrpcl  14343  bccmpl  14344  bcp1n  14351  bcp1nk  14352  bcval5  14353  permnn  14361  pfxmpt  14715  pfxfv  14719  pfxlen  14720  addlenpfx  14727  pfxswrd  14742  swrdpfx  14743  pfxpfx  14744  pfxpfxid  14745  lenrevpfxcctswrd  14748  swrdccatin1  14761  pfxccat3  14770  pfxccatpfx1  14772  pfxccat3a  14774  swrdccat3blem  14775  splfv2a  14792  repswpfx  14821  2cshwcshw  14861  cshwcsh2id  14864  pfxco  14874  binomlem  15882  binom1p  15884  binom1dif  15886  bcxmas  15888  climcnds  15904  arisum  15913  arisum2  15914  pwdif  15921  geolim  15923  geo2sum  15926  mertenslem1  15937  mertenslem2  15938  mertens  15939  risefacval2  16063  fallfacval2  16064  fallfacval3  16065  risefaccllem  16066  fallfaccllem  16067  risefacp1  16082  fallfacp1  16083  fallfacfwd  16089  binomfallfaclem1  16092  binomfallfaclem2  16093  binomrisefac  16095  bcfallfac  16097  bpolylem  16101  bpolysum  16106  bpolydiflem  16107  fsumkthpow  16109  bpoly4  16112  efcvgfsum  16139  efcj  16145  efaddlem  16146  effsumlt  16166  eirrlem  16259  3dvds  16388  pwp1fsum  16448  prmdiveq  16844  hashgcdlem  16846  pcbc  16959  vdwapf  17031  vdwlem2  17041  vdwlem6  17045  vdwlem8  17047  psgnunilem2  19564  efgcpbllemb  19824  srgbinomlem3  20309  srgbinomlem4  20310  srgbinomlem  20311  freshmansdream  21692  coe1mul2  22398  coe1tmmul2  22405  coe1tmmul  22406  cply1mul  22424  gsummoncoe1  22436  m2pmfzgsumcl  22873  decpmatmul  22897  pmatcollpw3fi1lem1  22911  mp2pm2mplem4  22934  pm2mpmhmlem2  22944  chpscmatgsumbin  22969  chpscmatgsummon  22970  chfacfscmulgsum  22985  chfacfpmmulgsum  22989  cpmadugsumlemB  22999  cpmadugsumlemC  23000  cpmadugsumlemF  23001  cpmadugsumfi  23002  mbfi1fseqlem3  25844  mbfi1fseqlem4  25845  itg0  25907  itgz  25908  itgcl  25911  iblabsr  25957  iblmulc2  25958  itgsplit  25963  dvn2bss  26057  coe1mul3  26224  elply2  26321  plyf  26323  elplyd  26327  ply1termlem  26328  plyeq0lem  26335  plypf1  26337  plyaddlem1  26338  plymullem1  26339  plyaddlem  26340  plymullem  26341  coeeulem  26349  coeidlem  26362  coeid3  26365  plyco  26366  coeeq2  26367  dgreq  26369  coefv0  26373  coeaddlem  26374  coemullem  26375  coemulhi  26379  coemulc  26380  coe1termlem  26383  plycn  26386  plycjlem  26401  plycj  26402  plycjOLD  26404  plyrecj  26406  plyn0mulidp  26410  dvply1  26413  dvply2g  26414  vieta1lem2  26440  elqaalem2  26449  elqaalem3  26450  aareccl  26455  aalioulem1  26461  taylply2  26496  taylply  26497  dvtaylp  26498  dvntaylp0  26500  taylthlem2  26502  pserulm  26550  psercn2  26551  pserdvlem2  26556  abelthlem6  26564  abelthlem7  26566  abelthlem8  26567  advlogexp  26785  cxpeq  26887  log2tlbnd  27075  log2ublem2  27077  log2ub  27079  birthdaylem2  27082  birthdaylem3  27083  ftalem1  27202  ftalem5  27206  basellem2  27211  basellem3  27212  dvdsppwf1o  27315  musum  27320  sgmppw  27326  1sgmprm  27328  logexprlim  27354  mersenne  27356  lgseisenlem1  27504  dchrisum0flblem1  27637  pntpbnd2  27716  crctcshwlkn0  30110  bcm1n  33080  gsummptrev  33316  gsummulsubdishift1  33328  esplyfv1  33903  esplyfv  33904  esplysply  33905  vietalem  33913  vieta  33914  signsplypnf  34881  signstres  34906  subfacval2  35577  subfaclim  35578  cvmliftlem7  35681  bccolsum  36129  knoppcnlem7  36976  knoppcnlem8  36977  knoppndvlem5  36993  knoppndvlem11  36999  knoppndvlem14  37002  knoppndvlem15  37003  poimirlem3  38161  poimirlem4  38162  poimirlem12  38170  poimirlem15  38173  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem23  38181  poimirlem24  38182  poimirlem25  38183  poimirlem28  38186  poimirlem29  38187  poimirlem31  38189  iblmulc2nc  38223  lcmineqlem1  42685  lcmineqlem2  42686  lcmineqlem3  42687  lcmineqlem4  42688  lcmineqlem6  42690  aks6d1c2lem3  42782  bcled  42834  jm2.22  43613  jm2.23  43614  hbt  43748  cnsrplycl  43785  bcc0  44941  binomcxplemnn0  44950  binomcxplemfrat  44952  binomcxplemradcnv  44953  dvnmptdivc  46543  dvnmul  46548  dvnprodlem1  46551  dvnprodlem2  46552  dvnprodlem3  46553  iblsplit  46571  elaa2lem  46838  etransclem2  46841  etransclem23  46862  etransclem28  46867  etransclem29  46868  etransclem32  46871  etransclem33  46872  etransclem35  46874  etransclem38  46877  etransclem39  46878  etransclem43  46882  etransclem44  46883  etransclem45  46884  etransclem46  46885  etransclem47  46886  etransclem48  46887  2elfz3nn0  47941  fz0addcom  47942  2elfz2melfz  47943  fz0addge0  47944  facnn0dvdsfac  48010  fmtnorec2lem  48182  fmtnodvds  48184  fmtnorec3  48188  lighneallem3  48247  lighneallem4b  48249  lighneallem4  48250  altgsumbc  49016  altgsumbcALT  49017  ply1mulgsumlem2  49051  ply1mulgsum  49054  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  aacllem  50474