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

Theorem elfznn 11815
Description: A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.)
Assertion
Ref Expression
elfznn  |-  ( K  e.  ( 1 ... N )  ->  K  e.  NN )

Proof of Theorem elfznn
StepHypRef Expression
1 elfzelz 11787 . 2  |-  ( K  e.  ( 1 ... N )  ->  K  e.  ZZ )
2 elfzle1 11789 . 2  |-  ( K  e.  ( 1 ... N )  ->  1  <_  K )
3 elnnz1 10952 . 2  |-  ( K  e.  NN  <->  ( K  e.  ZZ  /\  1  <_  K ) )
41, 2, 3sylanbrc 668 1  |-  ( K  e.  ( 1 ... N )  ->  K  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   class class class wbr 4417  (class class class)co 6296   1c1 9529    <_ cle 9665   NNcn 10598   ZZcz 10926   ...cfz 11771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-nn 10599  df-z 10927  df-uz 11149  df-fz 11772
This theorem is referenced by:  elfz1end  11816  fz1ssnn  11817  fzossnn  11950  bcm1k  12486  bcpasc  12492  seqcoll  12610  swrd0fv0  12770  swrd0fvlsw  12773  isercolllem2  13696  isercolllem3  13697  isercoll  13698  sumeq2ii  13726  summolem3  13747  summolem2a  13748  fsum  13753  sumz  13755  fsumconst  13818  o1fsum  13840  binomlem  13854  incexc2  13863  climcndslem1  13874  climcndslem2  13875  climcnds  13876  harmonic  13884  arisum2  13886  trireciplem  13887  geo2sum  13896  geo2lim  13898  prodeq2ii  13934  prodmolem3  13954  prodmolem2a  13955  fprod  13962  prod1  13965  fprodfac  13994  fprodconst  13999  risefallfac  14044  risefacfac  14055  fallfacval4  14063  bpolydiflem  14074  rpnnen2lem10  14243  fzm1ndvds  14324  lcmslefacOLD  14546  lcmflefac  14581  phicl  14675  prmdivdiv  14693  pcfac  14796  pcbc  14797  prmreclem2  14813  prmreclem3  14814  prmreclem4  14815  prmreclem5  14816  prmreclem6  14817  prmrec  14818  4sqlem13OLD  14853  4sqlem13  14859  vdwlem2  14884  vdwlem3  14885  vdwlem10  14892  vdwlem12  14894  prmocl  14944  prmop1  14948  fvprmselelfz  14954  fvprmselgcd1  14955  prmolefac  14956  prmodvdslcmf  14957  prmormapnnOLD  14966  prmdvdsprmorOLD  14967  prmorlefacOLD  14970  prmgapprmo  14985  mulgnnsubcl  16714  mulgnn0z  16722  mulgnndir  16724  oddvdsnn0  17128  odnncl  17129  gexcl3  17167  efgsres  17316  mulgnn0di  17394  gsumconst  17495  srgbinomlem4  17704  chfacfscmulgsum  19808  chfacfpmmulgsum  19812  chfacfpmmulgsum2  19813  cayhamlem1  19814  cpmadugsumlemF  19824  1stcfb  20384  1stckgenlem  20492  lebnumii  21883  ovollb2lem  22315  ovolunlem1a  22323  ovoliunlem1  22329  ovoliunlem2  22330  ovoliun2  22333  ovolscalem1  22340  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  voliunlem1  22377  volsup  22383  ioombl1lem4  22388  uniioovol  22410  uniioombllem3a  22416  uniioombllem3  22417  uniioombllem4  22418  uniioombllem5  22419  uniioombllem6  22420  dvply1  23102  aaliou3lem5  23165  aaliou3lem6  23166  dvtaylp  23187  taylthlem2  23191  pserdvlem2  23245  logfac  23412  atantayl  23725  birthdaylem2  23740  emcllem1  23783  emcllem2  23784  emcllem3  23785  emcllem5  23787  emcllem7  23789  harmoniclbnd  23796  harmonicubnd  23797  harmonicbnd4  23798  fsumharmonic  23799  lgamgulm2  23823  lgamcvglem  23827  lgamcvg2  23842  gamcvg2lem  23846  wilthlem1  23855  wilthlem2  23856  ftalem5  23863  basellem1  23867  basellem8  23874  chpf  23910  efchpcl  23912  chpp1  23942  chpwordi  23944  prmorcht  23965  dvdsflf1o  23976  dvdsflsumcom  23977  chtlepsi  23994  fsumvma2  24002  pclogsum  24003  vmasum  24004  logfac2  24005  chpval2  24006  chpchtsum  24007  logfaclbnd  24010  logexprlim  24013  logfacrlim2  24014  pcbcctr  24064  bposlem1  24072  bposlem2  24073  lgscllem  24091  lgsval2lem  24094  lgsval4a  24106  lgsneg  24107  lgsdir  24118  lgsdilem2  24119  lgsdi  24120  lgsne0  24121  lgsqrlem2  24130  lgseisenlem1  24137  lgseisenlem2  24138  lgseisenlem3  24139  lgseisenlem4  24140  lgseisen  24141  lgsquadlem1  24142  lgsquadlem2  24143  lgsquadlem3  24144  chebbnd1lem1  24167  vmadivsum  24180  vmadivsumb  24181  rplogsumlem2  24183  dchrisum0lem1a  24184  rpvmasumlem  24185  dchrisumlem2  24188  dchrmusum2  24192  dchrvmasumlem1  24193  dchrvmasum2lem  24194  dchrvmasum2if  24195  dchrvmasumlem2  24196  dchrvmasumlem3  24197  dchrvmasumiflem1  24199  dchrvmasumiflem2  24200  dchrisum0fno1  24209  rpvmasum2  24210  dchrisum0re  24211  dchrisum0lem1b  24213  dchrisum0lem1  24214  dchrisum0lem2a  24215  dchrisum0lem2  24216  dchrisum0lem3  24217  dchrisum0  24218  dchrmusumlem  24220  dchrvmasumlem  24221  rplogsum  24225  mudivsum  24228  mulogsumlem  24229  mulogsum  24230  mulog2sumlem1  24232  mulog2sumlem2  24233  mulog2sumlem3  24234  vmalogdivsum2  24236  vmalogdivsum  24237  2vmadivsumlem  24238  log2sumbnd  24242  selberglem1  24243  selberglem2  24244  selberglem3  24245  selberg  24246  selbergb  24247  selberg2lem  24248  selberg2  24249  selberg2b  24250  chpdifbndlem1  24251  logdivbnd  24254  selberg3lem1  24255  selberg3lem2  24256  selberg3  24257  selberg4lem1  24258  selberg4  24259  pntrsumo1  24263  pntrsumbnd  24264  pntrsumbnd2  24265  selbergr  24266  selberg3r  24267  selberg4r  24268  selberg34r  24269  pntsf  24271  pntsval2  24274  pntrlog2bndlem1  24275  pntrlog2bndlem2  24276  pntrlog2bndlem3  24277  pntrlog2bndlem4  24278  pntrlog2bndlem5  24279  pntrlog2bndlem6  24281  pntrlog2bnd  24282  pntpbnd2  24285  pntlemf  24303  pntlemk  24304  pntlemo  24305  iseupa  25535  eupares  25545  eupap1  25546  dipcl  26193  dipcn  26201  sspival  26219  esumpcvgval  28735  esumpmono  28736  esumcvg  28743  esumcvgsum  28745  eulerpartlemgc  29018  ballotlemfc0  29148  ballotlemfcc  29149  ballotlemimin  29161  ballotlemic  29162  ballotlem1c  29163  ballotlemsel1i  29168  ballotlemsf1o  29169  erdszelem4  29702  erdszelem8  29706  erdsze2lem2  29712  cvmliftlem2  29794  cvmliftlem6  29798  cvmliftlem8  29800  cvmliftlem9  29801  cvmliftlem10  29802  bcprod  30158  faclim  30166  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem9  31653  poimirlem11  31655  poimirlem13  31657  poimirlem14  31658  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem18  31662  poimirlem22  31666  poimirlem32  31676  mblfinlem2  31682  eldioph3b  35316  diophin  35324  diophun  35325  eldiophss  35326  irrapxlem4  35379  sumnnodd  37286  stoweidlem34  37468  wallispilem4  37503  wallispi  37505  wallispi2lem1  37506  wallispi2  37508  stirlinglem5  37513  stirlinglem7  37515  stirlinglem10  37518  stirlinglem12  37520  fourierdlem83  37625  fourierdlem112  37654  caratheodorylem2  37861  pfxfv0  38344  pfxfvlsw  38347  altgsumbcALT  38907  nn0sumshdiglemA  39204  nn0sumshdiglemB  39205
  Copyright terms: Public domain W3C validator