Theorem elfznn0 13534

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5105  (class class class)co 7357  0cc0 11051   ≤ cle 11190  ℕ₀cn0 12413  ...cfz 13424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425

This theorem is referenced by:  fz0ssnn0  13536  fz0fzdiffz0  13550  difelfzle  13554  bcrpcl  14208  bccmpl  14209  bcp1n  14216  bcp1nk  14217  bcval5  14218  permnn  14226  pfxmpt  14566  pfxfv  14570  pfxlen  14571  addlenpfx  14579  pfxswrd  14594  swrdpfx  14595  pfxpfx  14596  pfxpfxid  14597  swrdccatin1  14613  pfxccat3  14622  pfxccatpfx1  14624  pfxccat3a  14626  swrdccat3blem  14627  splfv2a  14644  repswpfx  14673  2cshwcshw  14714  cshwcsh2id  14717  pfxco  14727  binomlem  15714  binom1p  15716  binom1dif  15718  bcxmas  15720  climcnds  15736  arisum  15745  arisum2  15746  pwdif  15753  geolim  15755  geo2sum  15758  mertenslem1  15769  mertenslem2  15770  mertens  15771  risefacval2  15893  fallfacval2  15894  fallfacval3  15895  risefaccllem  15896  fallfaccllem  15897  risefacp1  15912  fallfacp1  15913  fallfacfwd  15919  binomfallfaclem1  15922  binomfallfaclem2  15923  binomrisefac  15925  bcfallfac  15927  bpolylem  15931  bpolysum  15936  bpolydiflem  15937  fsumkthpow  15939  bpoly4  15942  efcvgfsum  15968  efcj  15974  efaddlem  15975  effsumlt  15993  eirrlem  16086  3dvds  16213  pwp1fsum  16273  prmdiveq  16658  hashgcdlem  16660  pcbc  16772  vdwapf  16844  vdwlem2  16854  vdwlem6  16858  vdwlem8  16860  psgnunilem2  19277  efgcpbllemb  19537  srgbinomlem3  19959  srgbinomlem4  19960  srgbinomlem  19961  coe1mul2  21640  coe1tmmul2  21647  coe1tmmul  21648  cply1mul  21665  gsummoncoe1  21675  m2pmfzgsumcl  22097  decpmatmul  22121  pmatcollpw3fi1lem1  22135  mp2pm2mplem4  22158  pm2mpmhmlem2  22168  chpscmatgsumbin  22193  chpscmatgsummon  22194  chfacfscmulgsum  22209  chfacfpmmulgsum  22213  cpmadugsumlemB  22223  cpmadugsumlemC  22224  cpmadugsumlemF  22225  cpmadugsumfi  22226  mbfi1fseqlem3  25082  mbfi1fseqlem4  25083  itg0  25144  itgz  25145  itgcl  25148  iblabsr  25194  iblmulc2  25195  itgsplit  25200  dvn2bss  25294  coe1mul3  25464  elply2  25557  plyf  25559  elplyd  25563  ply1termlem  25564  plyeq0lem  25571  plypf1  25573  plyaddlem1  25574  plymullem1  25575  plyaddlem  25576  plymullem  25577  coeeulem  25585  coeidlem  25598  coeid3  25601  plyco  25602  coeeq2  25603  dgreq  25605  coefv0  25609  coeaddlem  25610  coemullem  25611  coemulhi  25615  coemulc  25616  coe1termlem  25619  plycn  25622  plycjlem  25637  plycj  25638  plyrecj  25640  dvply1  25644  dvply2g  25645  vieta1lem2  25671  elqaalem2  25680  elqaalem3  25681  aareccl  25686  aalioulem1  25692  taylply2  25727  taylply  25728  dvtaylp  25729  dvntaylp0  25731  taylthlem2  25733  pserulm  25781  psercn2  25782  pserdvlem2  25787  abelthlem6  25795  abelthlem7  25797  abelthlem8  25798  advlogexp  26010  cxpeq  26110  log2tlbnd  26295  log2ublem2  26297  log2ub  26299  birthdaylem2  26302  birthdaylem3  26303  ftalem1  26422  ftalem5  26426  basellem2  26431  basellem3  26432  dvdsppwf1o  26535  musum  26540  sgmppw  26545  1sgmprm  26547  logexprlim  26573  mersenne  26575  lgseisenlem1  26723  dchrisum0flblem1  26856  pntpbnd2  26935  crctcshwlkn0  28766  bcm1n  31698  freshmansdream  32067  plymulx0  33159  signsplypnf  33162  signstres  33187  subfacval2  33781  subfaclim  33782  cvmliftlem7  33885  bccolsum  34312  knoppcnlem7  34962  knoppcnlem8  34963  knoppndvlem5  34979  knoppndvlem11  34985  knoppndvlem14  34988  knoppndvlem15  34989  poimirlem3  36081  poimirlem4  36082  poimirlem12  36090  poimirlem15  36093  poimirlem16  36094  poimirlem17  36095  poimirlem19  36097  poimirlem20  36098  poimirlem23  36101  poimirlem24  36102  poimirlem25  36103  poimirlem28  36106  poimirlem29  36107  poimirlem31  36109  iblmulc2nc  36143  lcmineqlem1  40486  lcmineqlem2  40487  lcmineqlem3  40488  lcmineqlem4  40489  lcmineqlem6  40491  jm2.22  41305  jm2.23  41306  hbt  41443  cnsrplycl  41480  bcc0  42610  binomcxplemnn0  42619  binomcxplemfrat  42621  binomcxplemradcnv  42622  dvnmptdivc  44169  dvnmul  44174  dvnprodlem1  44177  dvnprodlem2  44178  dvnprodlem3  44179  iblsplit  44197  elaa2lem  44464  etransclem2  44467  etransclem23  44488  etransclem28  44493  etransclem29  44494  etransclem32  44497  etransclem33  44498  etransclem35  44500  etransclem38  44503  etransclem39  44504  etransclem43  44508  etransclem44  44509  etransclem45  44510  etransclem46  44511  etransclem47  44512  etransclem48  44513  2elfz3nn0  45538  fz0addcom  45539  2elfz2melfz  45540  fz0addge0  45541  fmtnorec2lem  45724  fmtnodvds  45726  fmtnorec3  45730  lighneallem3  45789  lighneallem4b  45791  lighneallem4  45792  altgsumbc  46418  altgsumbcALT  46419  ply1mulgsumlem2  46458  ply1mulgsum  46461  nn0sumshdiglemA  46695  nn0sumshdiglemB  46696  aacllem  47238