Theorem elfznn0 12727

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

Syntax hints:   → wi 4   ∈ wcel 2164   class class class wbr 4873  (class class class)co 6905  0cc0 10252   ≤ cle 10392  ℕ₀cn0 11618  ...cfz 12619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-nn 11351  df-n0 11619  df-z 11705  df-uz 11969  df-fz 12620

This theorem is referenced by:  fz0ssnn0  12729  fz0fzdiffz0  12743  difelfzle  12747  bcrpcl  13388  bccmpl  13389  bcp1n  13396  bcp1nk  13397  bcval5  13398  permnn  13406  swrd0lenOLD  13708  swrd0fOLD  13714  swrd0fvOLD  13728  pfxmpt  13757  pfxfv  13761  pfxlen  13762  addlenpfx  13770  swrd0swrdOLD  13785  pfxswrd  13786  swrdswrd0OLD  13787  swrdpfx  13788  swrd0swrd0OLD  13789  pfxpfx  13790  swrd0swrdidOLD  13791  pfxpfxid  13792  wrdcctswrdOLD  13794  pfxccat3  13833  swrdccat3OLD  13834  pfxccatpfx1  13837  pfxccat3a  13839  swrdccat3aOLD  13840  swrdccat3blem  13841  splfv2a  13870  splfv2aOLD  13871  repswpfx  13901  2cshwcshw  13946  cshwcsh2id  13949  pfxco  13959  binomlem  14935  binom1p  14937  binom1dif  14939  bcxmas  14941  climcnds  14957  arisum  14966  arisum2  14967  pwm1geoser  14974  geolim  14975  geo2sum  14978  mertenslem1  14989  mertenslem2  14990  mertens  14991  risefacval2  15113  fallfacval2  15114  fallfacval3  15115  risefaccllem  15116  fallfaccllem  15117  risefacp1  15132  fallfacp1  15133  fallfacfwd  15139  binomfallfaclem1  15142  binomfallfaclem2  15143  binomrisefac  15145  bcfallfac  15147  bpolylem  15151  bpolysum  15156  bpolydiflem  15157  fsumkthpow  15159  bpoly4  15162  efcvgfsum  15188  efcj  15194  efaddlem  15195  effsumlt  15213  eirrlem  15306  3dvds  15429  pwp1fsum  15488  prmdiveq  15862  hashgcdlem  15864  pcbc  15975  vdwapf  16047  vdwlem2  16057  vdwlem6  16061  vdwlem8  16063  psgnunilem2  18266  efgcpbllemb  18521  srgbinomlem3  18896  srgbinomlem4  18897  srgbinomlem  18898  coe1mul2  19999  coe1tmmul2  20006  coe1tmmul  20007  cply1mul  20024  gsummoncoe1  20034  m2pmfzgsumcl  20923  decpmatmul  20947  pmatcollpw3fi1lem1  20961  mp2pm2mplem4  20984  pm2mpmhmlem2  20994  chpscmatgsumbin  21019  chpscmatgsummon  21020  chfacfscmulgsum  21035  chfacfpmmulgsum  21039  cpmadugsumlemB  21049  cpmadugsumlemC  21050  cpmadugsumlemF  21051  cpmadugsumfi  21052  mbfi1fseqlem3  23883  mbfi1fseqlem4  23884  itg0  23945  itgz  23946  itgcl  23949  iblabsr  23995  iblmulc2  23996  itgsplit  24001  dvn2bss  24092  coe1mul3  24258  elply2  24351  plyf  24353  elplyd  24357  ply1termlem  24358  plyeq0lem  24365  plypf1  24367  plyaddlem1  24368  plymullem1  24369  plyaddlem  24370  plymullem  24371  coeeulem  24379  coeidlem  24392  coeid3  24395  plyco  24396  coeeq2  24397  dgreq  24399  coefv0  24403  coeaddlem  24404  coemullem  24405  coemulhi  24409  coemulc  24410  coe1termlem  24413  plycn  24416  plycjlem  24431  plycj  24432  plyrecj  24434  dvply1  24438  dvply2g  24439  vieta1lem2  24465  elqaalem2  24474  elqaalem3  24475  aareccl  24480  aalioulem1  24486  taylply2  24521  taylply  24522  dvtaylp  24523  dvntaylp0  24525  taylthlem2  24527  pserulm  24575  psercn2  24576  pserdvlem2  24581  abelthlem6  24589  abelthlem7  24591  abelthlem8  24592  advlogexp  24800  cxpeq  24900  log2tlbnd  25085  log2ublem2  25087  log2ub  25089  birthdaylem2  25092  birthdaylem3  25093  ftalem1  25212  ftalem5  25216  basellem2  25221  basellem3  25222  dvdsppwf1o  25325  musum  25330  sgmppw  25335  1sgmprm  25337  logexprlim  25363  mersenne  25365  lgseisenlem1  25513  dchrisum0flblem1  25610  pntpbnd2  25689  crctcshwlkn0  27120  bcm1n  30090  plymulx0  31160  signsplypnf  31163  signstres  31189  subfacval2  31704  subfaclim  31705  cvmliftlem7  31808  bccolsum  32156  knoppcnlem7  33011  knoppcnlem8  33012  knoppndvlem5  33028  knoppndvlem11  33034  knoppndvlem14  33037  knoppndvlem15  33038  poimirlem3  33949  poimirlem4  33950  poimirlem12  33958  poimirlem15  33961  poimirlem16  33962  poimirlem17  33963  poimirlem19  33965  poimirlem20  33966  poimirlem23  33969  poimirlem24  33970  poimirlem25  33971  poimirlem28  33974  poimirlem29  33975  poimirlem31  33977  iblmulc2nc  34011  jm2.22  38398  jm2.23  38399  hbt  38536  cnsrplycl  38573  bcc0  39372  binomcxplemnn0  39381  binomcxplemfrat  39383  binomcxplemradcnv  39384  dvnmptdivc  40941  dvnmul  40946  dvnprodlem1  40949  dvnprodlem2  40950  dvnprodlem3  40951  iblsplit  40969  elaa2lem  41237  etransclem2  41240  etransclem23  41261  etransclem28  41266  etransclem29  41267  etransclem32  41270  etransclem33  41271  etransclem35  41273  etransclem38  41276  etransclem39  41277  etransclem43  41281  etransclem44  41282  etransclem45  41283  etransclem46  41284  etransclem47  41285  etransclem48  41286  2elfz3nn0  42207  fz0addcom  42208  2elfz2melfz  42209  fz0addge0  42210  fmtnorec2lem  42277  fmtnodvds  42279  fmtnorec3  42283  pwdif  42324  lighneallem3  42347  lighneallem4b  42349  lighneallem4  42350  altgsumbc  42970  altgsumbcALT  42971  ply1mulgsumlem2  43015  ply1mulgsum  43018  nn0sumshdiglemA  43253  nn0sumshdiglemB  43254  aacllem  43436