Theorem elfznn0 13761

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  (class class class)co 7424  0cc0 11207   ≤ cle 11351  ℕ₀cn0 12613  ...cfz 13646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-1st 8005  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-rdg 8426  df-er 8725  df-en 8982  df-dom 8983  df-sdom 8984  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-nn 12343  df-n0 12614  df-z 12701  df-uz 12973  df-fz 13647

This theorem is used by:  fz0ssnn0  13763  fz0fzdiffz0  13778  difelfzle  13782  bcrpcl  14459  bccmpl  14460  bcp1n  14467  bcp1nk  14468  bcval5  14469  permnn  14477  pfxmpt  14836  pfxfv  14840  pfxlen  14841  addlenpfx  14848  pfxswrd  14863  swrdpfx  14864  pfxpfx  14865  pfxpfxid  14866  lenrevpfxcctswrd  14869  swrdccatin1  14882  pfxccat3  14891  pfxccatpfx1  14893  pfxccat3a  14895  swrdccat3blem  14896  splfv2a  14913  repswpfx  14944  2cshwcshw  14984  cshwcsh2id  14987  pfxco  14997  binomlem  16007  binom1p  16009  binom1dif  16011  bcxmas  16013  climcnds  16029  arisum  16038  arisum2  16039  pwdif  16046  geolim  16048  geo2sum  16051  mertenslem1  16062  mertenslem2  16063  mertens  16064  risefacval2  16186  fallfacval2  16187  fallfacval3  16188  risefaccllem  16189  fallfaccllem  16190  risefacp1  16204  fallfacp1  16205  fallfacfwd  16211  binomfallfaclem1  16214  binomfallfaclem2  16215  binomrisefac  16217  bcfallfac  16219  bpolylem  16223  bpolysum  16228  bpolydiflem  16229  fsumkthpow  16231  bpoly4  16234  efcvgfsum  16261  efcj  16267  efaddlem  16268  effsumlt  16288  eirrlem  16381  3dvds  16510  pwp1fsum  16570  prmdiveq  16972  hashgcdlem  16974  pcbc  17087  vdwapf  17159  vdwlem2  17169  vdwlem6  17173  vdwlem8  17175  psgnunilem2  19718  efgcpbllemb  19978  srgbinomlem3  20463  srgbinomlem4  20464  srgbinomlem  20465  freshmansdream  21889  coe1mul2  22597  coe1tmmul2  22604  coe1tmmul  22605  cply1mul  22623  gsummoncoe1  22635  m2pmfzgsumcl  23075  decpmatmul  23099  pmatcollpw3fi1lem1  23113  mp2pm2mplem4  23136  pm2mpmhmlem2  23146  chpscmatgsumbin  23171  chpscmatgsummon  23172  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  cpmadugsumlemB  23201  cpmadugsumlemC  23202  cpmadugsumlemF  23203  cpmadugsumfi  23204  mbfi1fseqlem3  26047  mbfi1fseqlem4  26048  itg0  26109  itgz  26110  itgcl  26113  iblabsr  26159  iblmulc2  26160  itgsplit  26165  dvn2bss  26259  coe1mul3  26426  elply2  26523  plyf  26525  elplyd  26529  ply1termlem  26530  plyeq0lem  26538  plypf1  26540  plyaddlem1  26541  plymullem1  26542  plyaddlem  26543  plymullem  26544  coeeulem  26552  coeidlem  26565  coeid3  26568  plyco  26569  coeeq2  26570  dgreq  26572  coefv0  26576  coeaddlem  26577  coemullem  26578  coemulhi  26582  coemulc  26583  coe1termlem  26586  plycn  26589  plycjlem  26604  plycj  26605  plyrecj  26607  plyn0mulidp  26611  dvply1  26614  dvply2g  26615  vieta1lem2  26643  elqaalem2  26652  elqaalem3  26653  aareccl  26662  aalioulem1  26668  taylply2  26704  taylply  26705  dvtaylp  26706  dvntaylp0  26708  taylthlem2  26710  pserulm  26758  psercn2  26759  pserdvlem2  26764  abelthlem6  26772  abelthlem7  26774  abelthlem8  26775  advlogexp  26992  cxpeq  27094  log2tlbnd  27282  log2ublem2  27284  log2ub  27286  birthdaylem2  27289  birthdaylem3  27290  ftalem1  27409  ftalem5  27413  basellem2  27418  basellem3  27419  dvdsppwf1o  27522  musum  27527  sgmppw  27533  1sgmprm  27535  logexprlim  27561  mersenne  27563  lgseisenlem1  27711  dchrisum0flblem1  27844  pntpbnd2  27923  crctcshwlkn0  30419  bcm1n  33437  gsummptrev  33667  gsummulsubdishift1  33679  esplyfv1  34251  esplyfv  34252  esplysply  34253  vietalem  34261  vieta  34262  signsplypnf  35229  signstres  35254  subfacval2  36070  subfaclim  36071  cvmliftlem7  36174  bccolsum  36628  knoppcnlem7  37489  knoppcnlem8  37490  knoppndvlem5  37506  knoppndvlem11  37512  knoppndvlem14  37515  knoppndvlem15  37516  poimirlem3  38678  poimirlem4  38679  poimirlem12  38687  poimirlem15  38690  poimirlem16  38691  poimirlem17  38692  poimirlem19  38694  poimirlem20  38695  poimirlem23  38698  poimirlem24  38699  poimirlem25  38700  poimirlem28  38703  poimirlem29  38704  poimirlem31  38706  iblmulc2nc  38740  lcmineqlem1  43216  lcmineqlem2  43217  lcmineqlem3  43218  lcmineqlem4  43219  lcmineqlem6  43221  aks6d1c2lem3  43313  bcled  43365  jm2.22  44139  jm2.23  44140  hbt  44269  cnsrplycl  44306  bcc0  45461  binomcxplemnn0  45470  binomcxplemfrat  45472  binomcxplemradcnv  45473  dvnmptdivc  47084  dvnmul  47089  dvnprodlem1  47092  dvnprodlem2  47093  dvnprodlem3  47094  iblsplit  47112  elaa2lem  47379  etransclem2  47382  etransclem23  47403  etransclem28  47408  etransclem29  47409  etransclem32  47412  etransclem33  47413  etransclem35  47415  etransclem38  47418  etransclem39  47419  etransclem43  47423  etransclem44  47424  etransclem45  47425  etransclem46  47426  etransclem47  47427  etransclem48  47428  2elfz3nn0  48522  fz0addcom  48523  2elfz2melfz  48524  fz0addge0  48525  facnn0dvdsfac  48591  fmtnorec2lem  48763  fmtnodvds  48765  fmtnorec3  48769  lighneallem3  48828  lighneallem4b  48830  lighneallem4  48831  altgsumbc  49600  altgsumbcALT  49601  ply1mulgsumlem2  49635  ply1mulgsum  49638  nn0sumshdiglemA  49867  nn0sumshdiglemB  49868  aacllem  51150