MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfznn0 Structured version   Unicode version

Theorem elfznn0 11470
Description: A member of a finite set of sequential integers starting at 0 is a nonnegative integer. (Contributed by NM, 5-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfznn0  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )

Proof of Theorem elfznn0
StepHypRef Expression
1 elfz2nn0 11469 . 2  |-  ( K  e.  ( 0 ... N )  <->  ( K  e.  NN0  /\  N  e. 
NN0  /\  K  <_  N ) )
21simp1bi 998 1  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1757   class class class wbr 4282  (class class class)co 6082   0cc0 9272    <_ cle 9409   NN0cn0 10569   ...cfz 11426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-1st 6568  df-2nd 6569  df-recs 6820  df-rdg 6854  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-nn 10313  df-n0 10570  df-z 10637  df-uz 10852  df-fz 11427
This theorem is referenced by:  fz0fzdiffz0  11478  fzo0ssnn0  11597  bcrpcl  12070  bccmpl  12071  bcp1n  12078  bcp1nk  12079  bcval5  12080  permnn  12088  swrd0len  12304  swrd0fv  12321  swrd0swrd  12341  swrdswrd0  12342  swrd0swrd0  12343  swrd0swrdid  12344  wrdcctswrd  12345  swrdccat3  12369  swrdccat3a  12371  swrdccat3blem  12372  splfv2a  12384  binomlem  13277  binom1p  13279  binom1dif  13281  bcxmas  13283  climcnds  13299  arisum  13307  arisum2  13308  geolim  13315  geo2sum  13318  mertenslem1  13329  mertenslem2  13330  mertens  13331  efcvgfsum  13356  efcj  13362  efaddlem  13363  effsumlt  13380  eirrlem  13471  fzo0dvdseq  13571  3dvds  13581  prmdiveq  13846  pcbc  13947  vdwapf  14018  vdwlem2  14028  vdwlem6  14032  vdwlem8  14034  psgnunilem2  15983  efgcpbllemb  16234  psrbaglefi  17377  psrbaglefiOLD  17378  coe1mul2lem2  17622  coe1mul2  17623  coe1tmmul2  17629  coe1tmmul  17630  mbfi1fseqlem3  21039  mbfi1fseqlem4  21040  itg0  21101  itgz  21102  itgcl  21105  iblabsr  21151  iblmulc2  21152  itgsplit  21157  dvn2bss  21248  coe1mul3  21458  elply2  21551  plyf  21553  elplyd  21557  ply1termlem  21558  plyeq0lem  21565  plypf1  21567  plyaddlem1  21568  plymullem1  21569  plyaddlem  21570  plymullem  21571  coeeulem  21579  coeidlem  21592  coeid3  21595  plyco  21596  coeeq2  21597  dgreq  21599  coefv0  21602  coeaddlem  21603  coemullem  21604  coemulhi  21608  coemulc  21609  coe1termlem  21612  plycn  21615  plycjlem  21630  plycj  21631  plyrecj  21633  dvply1  21637  dvply2g  21638  vieta1lem2  21664  elqaalem2  21673  elqaalem3  21674  aareccl  21679  aannenlem1  21681  aalioulem1  21685  taylply2  21720  taylply  21721  dvtaylp  21722  dvntaylp0  21724  taylthlem2  21726  pserulm  21774  psercn2  21775  pserdvlem2  21780  abelthlem6  21788  abelthlem7  21790  abelthlem8  21791  advlogexp  21987  cxpeq  22082  log2tlbnd  22227  log2ublem2  22229  log2ub  22231  birthdaylem2  22233  birthdaylem3  22234  ftalem1  22297  ftalem5  22301  basellem2  22306  basellem3  22307  dvdsppwf1o  22413  musum  22418  sgmppw  22423  1sgmprm  22425  logexprlim  22451  mersenne  22453  lgseisenlem1  22575  dchrisum0flblem1  22644  pntpbnd2  22723  iseupa  23411  eupares  23421  bcm1n  25904  plymulx0  26798  signsplypnf  26801  signstres  26826  subfacval2  26925  subfaclim  26926  cvmliftlem7  27030  risefacval2  27362  fallfacval2  27363  fallfacval3  27364  risefaccllem  27365  fallfaccllem  27366  risefacp1  27381  fallfacp1  27382  fallfacfwd  27388  binomfallfaclem1  27391  binomfallfaclem2  27392  binomrisefac  27394  bcfallfac  27396  bpolylem  28040  bpolysum  28045  bpolydiflem  28046  fsumkthpow  28048  bpoly4  28051  iblmulc2nc  28303  jm2.22  29191  jm2.23  29192  hbt  29333  cnsrplycl  29371  hashgcdlem  29412  2elfz3nn0  30047  fz0addcom  30048  2elfz2melfz  30050  fz0addge0  30051  erclwwlktr0  30327  difelfzle  30335  cshwlemma1  30337
  Copyright terms: Public domain W3C validator