Theorem elfznn0 13667

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5111  (class class class)co 7419  0cc0 11117   ≤ cle 11261  ℕ₀cn0 12521  ...cfz 13553

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11173  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-nn 12251  df-n0 12522  df-z 12609  df-uz 12881  df-fz 13554

This theorem is used by:  fz0ssnn0  13669  fz0fzdiffz0  13684  difelfzle  13688  bcrpcl  14364  bccmpl  14365  bcp1n  14372  bcp1nk  14373  bcval5  14374  permnn  14382  pfxmpt  14740  pfxfv  14744  pfxlen  14745  addlenpfx  14752  pfxswrd  14767  swrdpfx  14768  pfxpfx  14769  pfxpfxid  14770  lenrevpfxcctswrd  14773  swrdccatin1  14786  pfxccat3  14795  pfxccatpfx1  14797  pfxccat3a  14799  swrdccat3blem  14800  splfv2a  14817  repswpfx  14848  2cshwcshw  14888  cshwcsh2id  14891  pfxco  14901  binomlem  15908  binom1p  15910  binom1dif  15912  bcxmas  15914  climcnds  15930  arisum  15939  arisum2  15940  pwdif  15947  geolim  15949  geo2sum  15952  mertenslem1  15963  mertenslem2  15964  mertens  15965  risefacval2  16089  fallfacval2  16090  fallfacval3  16091  risefaccllem  16092  fallfaccllem  16093  risefacp1  16107  fallfacp1  16108  fallfacfwd  16114  binomfallfaclem1  16117  binomfallfaclem2  16118  binomrisefac  16120  bcfallfac  16122  bpolylem  16126  bpolysum  16131  bpolydiflem  16132  fsumkthpow  16134  bpoly4  16137  efcvgfsum  16164  efcj  16170  efaddlem  16171  effsumlt  16191  eirrlem  16284  3dvds  16413  pwp1fsum  16473  prmdiveq  16869  hashgcdlem  16871  pcbc  16984  vdwapf  17056  vdwlem2  17066  vdwlem6  17070  vdwlem8  17072  psgnunilem2  19611  efgcpbllemb  19871  srgbinomlem3  20356  srgbinomlem4  20357  srgbinomlem  20358  freshmansdream  21776  coe1mul2  22482  coe1tmmul2  22489  coe1tmmul  22490  cply1mul  22508  gsummoncoe1  22520  m2pmfzgsumcl  22957  decpmatmul  22981  pmatcollpw3fi1lem1  22995  mp2pm2mplem4  23018  pm2mpmhmlem2  23028  chpscmatgsumbin  23053  chpscmatgsummon  23054  chfacfscmulgsum  23069  chfacfpmmulgsum  23073  cpmadugsumlemB  23083  cpmadugsumlemC  23084  cpmadugsumlemF  23085  cpmadugsumfi  23086  mbfi1fseqlem3  25929  mbfi1fseqlem4  25930  itg0  25992  itgz  25993  itgcl  25996  iblabsr  26042  iblmulc2  26043  itgsplit  26048  dvn2bss  26142  coe1mul3  26309  elply2  26406  plyf  26408  elplyd  26412  ply1termlem  26413  plyeq0lem  26420  plypf1  26422  plyaddlem1  26423  plymullem1  26424  plyaddlem  26425  plymullem  26426  coeeulem  26434  coeidlem  26447  coeid3  26450  plyco  26451  coeeq2  26452  dgreq  26454  coefv0  26458  coeaddlem  26459  coemullem  26460  coemulhi  26464  coemulc  26465  coe1termlem  26468  plycn  26471  plycjlem  26486  plycj  26487  plycjOLD  26489  plyrecj  26491  plyn0mulidp  26495  dvply1  26498  dvply2g  26499  vieta1lem2  26525  elqaalem2  26534  elqaalem3  26535  aareccl  26542  aalioulem1  26548  taylply2  26584  taylply  26585  dvtaylp  26586  dvntaylp0  26588  taylthlem2  26590  pserulm  26638  psercn2  26639  pserdvlem2  26644  abelthlem6  26652  abelthlem7  26654  abelthlem8  26655  advlogexp  26873  cxpeq  26975  log2tlbnd  27163  log2ublem2  27165  log2ub  27167  birthdaylem2  27170  birthdaylem3  27171  ftalem1  27290  ftalem5  27294  basellem2  27299  basellem3  27300  dvdsppwf1o  27403  musum  27408  sgmppw  27414  1sgmprm  27416  logexprlim  27442  mersenne  27444  lgseisenlem1  27592  dchrisum0flblem1  27725  pntpbnd2  27804  crctcshwlkn0  30239  bcm1n  33212  gsummptrev  33442  gsummulsubdishift1  33454  esplyfv1  34025  esplyfv  34026  esplysply  34027  vietalem  34035  vieta  34036  signsplypnf  35004  signstres  35029  subfacval2  35718  subfaclim  35719  cvmliftlem7  35822  bccolsum  36270  knoppcnlem7  37147  knoppcnlem8  37148  knoppndvlem5  37164  knoppndvlem11  37170  knoppndvlem14  37173  knoppndvlem15  37174  poimirlem3  38333  poimirlem4  38334  poimirlem12  38342  poimirlem15  38345  poimirlem16  38346  poimirlem17  38347  poimirlem19  38349  poimirlem20  38350  poimirlem23  38353  poimirlem24  38354  poimirlem25  38355  poimirlem28  38358  poimirlem29  38359  poimirlem31  38361  iblmulc2nc  38395  lcmineqlem1  42856  lcmineqlem2  42857  lcmineqlem3  42858  lcmineqlem4  42859  lcmineqlem6  42861  aks6d1c2lem3  42953  bcled  43005  jm2.22  43782  jm2.23  43783  hbt  43917  cnsrplycl  43954  bcc0  45110  binomcxplemnn0  45119  binomcxplemfrat  45121  binomcxplemradcnv  45122  dvnmptdivc  46712  dvnmul  46717  dvnprodlem1  46720  dvnprodlem2  46721  dvnprodlem3  46722  iblsplit  46740  elaa2lem  47007  etransclem2  47010  etransclem23  47031  etransclem28  47036  etransclem29  47037  etransclem32  47040  etransclem33  47041  etransclem35  47043  etransclem38  47046  etransclem39  47047  etransclem43  47051  etransclem44  47052  etransclem45  47053  etransclem46  47054  etransclem47  47055  etransclem48  47056  2elfz3nn0  48113  fz0addcom  48114  2elfz2melfz  48115  fz0addge0  48116  facnn0dvdsfac  48182  fmtnorec2lem  48354  fmtnodvds  48356  fmtnorec3  48360  lighneallem3  48419  lighneallem4b  48421  lighneallem4  48422  altgsumbc  49191  altgsumbcALT  49192  ply1mulgsumlem2  49226  ply1mulgsum  49229  nn0sumshdiglemA  49458  nn0sumshdiglemB  49459  aacllem  50680