Theorem elfznn0 13536

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  (class class class)co 7358  0cc0 11026   ≤ cle 11167  ℕ₀cn0 12401  ...cfz 13423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  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 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-n0 12402  df-z 12489  df-uz 12752  df-fz 13424

This theorem is referenced by:  fz0ssnn0  13538  fz0fzdiffz0  13553  difelfzle  13557  bcrpcl  14231  bccmpl  14232  bcp1n  14239  bcp1nk  14240  bcval5  14241  permnn  14249  pfxmpt  14602  pfxfv  14606  pfxlen  14607  addlenpfx  14614  pfxswrd  14629  swrdpfx  14630  pfxpfx  14631  pfxpfxid  14632  lenrevpfxcctswrd  14635  swrdccatin1  14648  pfxccat3  14657  pfxccatpfx1  14659  pfxccat3a  14661  swrdccat3blem  14662  splfv2a  14679  repswpfx  14708  2cshwcshw  14748  cshwcsh2id  14751  pfxco  14761  binomlem  15752  binom1p  15754  binom1dif  15756  bcxmas  15758  climcnds  15774  arisum  15783  arisum2  15784  pwdif  15791  geolim  15793  geo2sum  15796  mertenslem1  15807  mertenslem2  15808  mertens  15809  risefacval2  15933  fallfacval2  15934  fallfacval3  15935  risefaccllem  15936  fallfaccllem  15937  risefacp1  15952  fallfacp1  15953  fallfacfwd  15959  binomfallfaclem1  15962  binomfallfaclem2  15963  binomrisefac  15965  bcfallfac  15967  bpolylem  15971  bpolysum  15976  bpolydiflem  15977  fsumkthpow  15979  bpoly4  15982  efcvgfsum  16009  efcj  16015  efaddlem  16016  effsumlt  16036  eirrlem  16129  3dvds  16258  pwp1fsum  16318  prmdiveq  16713  hashgcdlem  16715  pcbc  16828  vdwapf  16900  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  psgnunilem2  19424  efgcpbllemb  19684  srgbinomlem3  20163  srgbinomlem4  20164  srgbinomlem  20165  freshmansdream  21529  coe1mul2  22211  coe1tmmul2  22218  coe1tmmul  22219  cply1mul  22240  gsummoncoe1  22252  m2pmfzgsumcl  22692  decpmatmul  22716  pmatcollpw3fi1lem1  22730  mp2pm2mplem4  22753  pm2mpmhmlem2  22763  chpscmatgsumbin  22788  chpscmatgsummon  22789  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cpmadugsumfi  22821  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  itg0  25737  itgz  25738  itgcl  25741  iblabsr  25787  iblmulc2  25788  itgsplit  25793  dvn2bss  25888  coe1mul3  26060  elply2  26157  plyf  26159  elplyd  26163  ply1termlem  26164  plyeq0lem  26171  plypf1  26173  plyaddlem1  26174  plymullem1  26175  plyaddlem  26176  plymullem  26177  coeeulem  26185  coeidlem  26198  coeid3  26201  plyco  26202  coeeq2  26203  dgreq  26205  coefv0  26209  coeaddlem  26210  coemullem  26211  coemulhi  26215  coemulc  26216  coe1termlem  26219  plycn  26222  plycnOLD  26223  plycjlem  26238  plycj  26239  plycjOLD  26241  plyrecj  26243  dvply1  26247  dvply2g  26248  dvply2gOLD  26249  vieta1lem2  26275  elqaalem2  26284  elqaalem3  26285  aareccl  26290  aalioulem1  26296  taylply2  26331  taylply2OLD  26332  taylply  26333  dvtaylp  26334  dvntaylp0  26336  taylthlem2  26338  taylthlem2OLD  26339  pserulm  26387  psercn2  26388  psercn2OLD  26389  pserdvlem2  26394  abelthlem6  26402  abelthlem7  26404  abelthlem8  26405  advlogexp  26620  cxpeq  26723  log2tlbnd  26911  log2ublem2  26913  log2ub  26915  birthdaylem2  26918  birthdaylem3  26919  ftalem1  27039  ftalem5  27043  basellem2  27048  basellem3  27049  dvdsppwf1o  27152  musum  27157  sgmppw  27164  1sgmprm  27166  logexprlim  27192  mersenne  27194  lgseisenlem1  27342  dchrisum0flblem1  27475  pntpbnd2  27554  crctcshwlkn0  29894  bcm1n  32875  gsummptrev  33139  gsummulsubdishift1  33151  esplyfv1  33727  esplyfv  33728  esplysply  33729  vietalem  33735  vieta  33736  plymulx0  34704  signsplypnf  34707  signstres  34732  subfacval2  35381  subfaclim  35382  cvmliftlem7  35485  bccolsum  35933  knoppcnlem7  36699  knoppcnlem8  36700  knoppndvlem5  36716  knoppndvlem11  36722  knoppndvlem14  36725  knoppndvlem15  36726  poimirlem3  37824  poimirlem4  37825  poimirlem12  37833  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem28  37849  poimirlem29  37850  poimirlem31  37852  iblmulc2nc  37886  lcmineqlem1  42283  lcmineqlem2  42284  lcmineqlem3  42285  lcmineqlem4  42286  lcmineqlem6  42288  aks6d1c2lem3  42380  bcled  42432  jm2.22  43237  jm2.23  43238  hbt  43372  cnsrplycl  43409  bcc0  44581  binomcxplemnn0  44590  binomcxplemfrat  44592  binomcxplemradcnv  44593  dvnmptdivc  46182  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  iblsplit  46210  elaa2lem  46477  etransclem2  46480  etransclem23  46501  etransclem28  46506  etransclem29  46507  etransclem32  46510  etransclem33  46511  etransclem35  46513  etransclem38  46516  etransclem39  46517  etransclem43  46521  etransclem44  46522  etransclem45  46523  etransclem46  46524  etransclem47  46525  etransclem48  46526  2elfz3nn0  47562  fz0addcom  47563  2elfz2melfz  47564  fz0addge0  47565  fmtnorec2lem  47788  fmtnodvds  47790  fmtnorec3  47794  lighneallem3  47853  lighneallem4b  47855  lighneallem4  47856  altgsumbc  48598  altgsumbcALT  48599  ply1mulgsumlem2  48633  ply1mulgsum  48636  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  aacllem  50046