Theorem elfznn0 13523

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  (class class class)co 7349  0cc0 11009   ≤ cle 11150  ℕ₀cn0 12384  ...cfz 13410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-n0 12385  df-z 12472  df-uz 12736  df-fz 13411

This theorem is referenced by:  fz0ssnn0  13525  fz0fzdiffz0  13540  difelfzle  13544  bcrpcl  14215  bccmpl  14216  bcp1n  14223  bcp1nk  14224  bcval5  14225  permnn  14233  pfxmpt  14585  pfxfv  14589  pfxlen  14590  addlenpfx  14597  pfxswrd  14612  swrdpfx  14613  pfxpfx  14614  pfxpfxid  14615  lenrevpfxcctswrd  14618  swrdccatin1  14631  pfxccat3  14640  pfxccatpfx1  14642  pfxccat3a  14644  swrdccat3blem  14645  splfv2a  14662  repswpfx  14691  2cshwcshw  14732  cshwcsh2id  14735  pfxco  14745  binomlem  15736  binom1p  15738  binom1dif  15740  bcxmas  15742  climcnds  15758  arisum  15767  arisum2  15768  pwdif  15775  geolim  15777  geo2sum  15780  mertenslem1  15791  mertenslem2  15792  mertens  15793  risefacval2  15917  fallfacval2  15918  fallfacval3  15919  risefaccllem  15920  fallfaccllem  15921  risefacp1  15936  fallfacp1  15937  fallfacfwd  15943  binomfallfaclem1  15946  binomfallfaclem2  15947  binomrisefac  15949  bcfallfac  15951  bpolylem  15955  bpolysum  15960  bpolydiflem  15961  fsumkthpow  15963  bpoly4  15966  efcvgfsum  15993  efcj  15999  efaddlem  16000  effsumlt  16020  eirrlem  16113  3dvds  16242  pwp1fsum  16302  prmdiveq  16697  hashgcdlem  16699  pcbc  16812  vdwapf  16884  vdwlem2  16894  vdwlem6  16898  vdwlem8  16900  psgnunilem2  19374  efgcpbllemb  19634  srgbinomlem3  20113  srgbinomlem4  20114  srgbinomlem  20115  freshmansdream  21481  coe1mul2  22153  coe1tmmul2  22160  coe1tmmul  22161  cply1mul  22181  gsummoncoe1  22193  m2pmfzgsumcl  22633  decpmatmul  22657  pmatcollpw3fi1lem1  22671  mp2pm2mplem4  22694  pm2mpmhmlem2  22704  chpscmatgsumbin  22729  chpscmatgsummon  22730  chfacfscmulgsum  22745  chfacfpmmulgsum  22749  cpmadugsumlemB  22759  cpmadugsumlemC  22760  cpmadugsumlemF  22761  cpmadugsumfi  22762  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  itg0  25679  itgz  25680  itgcl  25683  iblabsr  25729  iblmulc2  25730  itgsplit  25735  dvn2bss  25830  coe1mul3  26002  elply2  26099  plyf  26101  elplyd  26105  ply1termlem  26106  plyeq0lem  26113  plypf1  26115  plyaddlem1  26116  plymullem1  26117  plyaddlem  26118  plymullem  26119  coeeulem  26127  coeidlem  26140  coeid3  26143  plyco  26144  coeeq2  26145  dgreq  26147  coefv0  26151  coeaddlem  26152  coemullem  26153  coemulhi  26157  coemulc  26158  coe1termlem  26161  plycn  26164  plycnOLD  26165  plycjlem  26180  plycj  26181  plycjOLD  26183  plyrecj  26185  dvply1  26189  dvply2g  26190  dvply2gOLD  26191  vieta1lem2  26217  elqaalem2  26226  elqaalem3  26227  aareccl  26232  aalioulem1  26238  taylply2  26273  taylply2OLD  26274  taylply  26275  dvtaylp  26276  dvntaylp0  26278  taylthlem2  26280  taylthlem2OLD  26281  pserulm  26329  psercn2  26330  psercn2OLD  26331  pserdvlem2  26336  abelthlem6  26344  abelthlem7  26346  abelthlem8  26347  advlogexp  26562  cxpeq  26665  log2tlbnd  26853  log2ublem2  26855  log2ub  26857  birthdaylem2  26860  birthdaylem3  26861  ftalem1  26981  ftalem5  26985  basellem2  26990  basellem3  26991  dvdsppwf1o  27094  musum  27099  sgmppw  27106  1sgmprm  27108  logexprlim  27134  mersenne  27136  lgseisenlem1  27284  dchrisum0flblem1  27417  pntpbnd2  27496  crctcshwlkn0  29766  bcm1n  32738  plymulx0  34515  signsplypnf  34518  signstres  34543  subfacval2  35164  subfaclim  35165  cvmliftlem7  35268  bccolsum  35716  knoppcnlem7  36477  knoppcnlem8  36478  knoppndvlem5  36494  knoppndvlem11  36500  knoppndvlem14  36503  knoppndvlem15  36504  poimirlem3  37607  poimirlem4  37608  poimirlem12  37616  poimirlem15  37619  poimirlem16  37620  poimirlem17  37621  poimirlem19  37623  poimirlem20  37624  poimirlem23  37627  poimirlem24  37628  poimirlem25  37629  poimirlem28  37632  poimirlem29  37633  poimirlem31  37635  iblmulc2nc  37669  lcmineqlem1  42006  lcmineqlem2  42007  lcmineqlem3  42008  lcmineqlem4  42009  lcmineqlem6  42011  aks6d1c2lem3  42103  bcled  42155  jm2.22  42972  jm2.23  42973  hbt  43107  cnsrplycl  43144  bcc0  44317  binomcxplemnn0  44326  binomcxplemfrat  44328  binomcxplemradcnv  44329  dvnmptdivc  45923  dvnmul  45928  dvnprodlem1  45931  dvnprodlem2  45932  dvnprodlem3  45933  iblsplit  45951  elaa2lem  46218  etransclem2  46221  etransclem23  46242  etransclem28  46247  etransclem29  46248  etransclem32  46251  etransclem33  46252  etransclem35  46254  etransclem38  46257  etransclem39  46258  etransclem43  46262  etransclem44  46263  etransclem45  46264  etransclem46  46265  etransclem47  46266  etransclem48  46267  2elfz3nn0  47304  fz0addcom  47305  2elfz2melfz  47306  fz0addge0  47307  fmtnorec2lem  47530  fmtnodvds  47532  fmtnorec3  47536  lighneallem3  47595  lighneallem4b  47597  lighneallem4  47598  altgsumbc  48340  altgsumbcALT  48341  ply1mulgsumlem2  48376  ply1mulgsum  48379  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  aacllem  49790