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

Theorem elfznn 11828
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 11800 . 2  |-  ( K  e.  ( 1 ... N )  ->  K  e.  ZZ )
2 elfzle1 11802 . 2  |-  ( K  e.  ( 1 ... N )  ->  1  <_  K )
3 elnnz1 10963 . 2  |-  ( K  e.  NN  <->  ( K  e.  ZZ  /\  1  <_  K ) )
41, 2, 3sylanbrc 670 1  |-  ( K  e.  ( 1 ... N )  ->  K  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   class class class wbr 4402  (class class class)co 6290   1c1 9540    <_ cle 9676   NNcn 10609   ZZcz 10937   ...cfz 11784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-z 10938  df-uz 11160  df-fz 11785
This theorem is referenced by:  elfz1end  11829  fz1ssnn  11830  fzossnn  11964  bcm1k  12500  bcpasc  12506  seqcoll  12627  swrd0fv0  12796  swrd0fvlsw  12799  isercolllem2  13729  isercolllem3  13730  isercoll  13731  sumeq2ii  13759  summolem3  13780  summolem2a  13781  fsum  13786  sumz  13788  fsumconst  13851  o1fsum  13873  binomlem  13887  incexc2  13896  climcndslem1  13907  climcndslem2  13908  climcnds  13909  harmonic  13917  arisum2  13919  trireciplem  13920  geo2sum  13929  geo2lim  13931  prodeq2ii  13967  prodmolem3  13987  prodmolem2a  13988  fprod  13995  prod1  13998  fprodfac  14027  fprodconst  14032  risefallfac  14077  risefacfac  14088  fallfacval4  14096  bpolydiflem  14107  rpnnen2lem10  14276  fzm1ndvds  14357  lcmslefacOLD  14586  lcmflefac  14621  phicl  14717  prmdivdiv  14735  pcfac  14844  pcbc  14845  prmreclem2  14861  prmreclem3  14862  prmreclem4  14863  prmreclem5  14864  prmreclem6  14865  prmrec  14866  4sqlem13OLD  14901  4sqlem13  14907  vdwlem2  14932  vdwlem3  14933  vdwlem10  14940  vdwlem12  14942  prmocl  14992  prmop1  14996  fvprmselelfz  15002  fvprmselgcd1  15003  prmolefac  15004  prmodvdslcmf  15005  prmormapnnOLD  15014  prmdvdsprmorOLD  15015  prmorlefacOLD  15018  prmgapprmo  15033  mulgnnsubcl  16770  mulgnn0z  16778  mulgnndir  16780  oddvdsnn0  17193  odnncl  17194  gexcl3  17239  efgsres  17388  mulgnn0di  17466  gsumconst  17567  srgbinomlem4  17776  chfacfscmulgsum  19884  chfacfpmmulgsum  19888  chfacfpmmulgsum2  19889  cayhamlem1  19890  cpmadugsumlemF  19900  1stcfb  20460  1stckgenlem  20568  lebnumii  21997  ovollb2lem  22441  ovolunlem1a  22449  ovoliunlem1  22455  ovoliunlem2  22456  ovoliun2  22459  ovolscalem1  22466  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  voliunlem1  22503  volsup  22509  ioombl1lem4  22514  uniioovol  22536  uniioombllem3a  22542  uniioombllem3  22543  uniioombllem4  22544  uniioombllem5  22545  uniioombllem6  22546  dvply1  23237  aaliou3lem5  23303  aaliou3lem6  23304  dvtaylp  23325  taylthlem2  23329  pserdvlem2  23383  logfac  23550  atantayl  23863  birthdaylem2  23878  emcllem1  23921  emcllem2  23922  emcllem3  23923  emcllem5  23925  emcllem7  23927  harmoniclbnd  23934  harmonicubnd  23935  harmonicbnd4  23936  fsumharmonic  23937  lgamgulm2  23961  lgamcvglem  23965  lgamcvg2  23980  gamcvg2lem  23984  wilthlem1  23993  wilthlem2  23994  ftalem5  24001  ftalem5OLD  24003  basellem1  24007  basellem8  24014  chpf  24050  efchpcl  24052  chpp1  24082  chpwordi  24084  prmorcht  24105  dvdsflf1o  24116  dvdsflsumcom  24117  chtlepsi  24134  fsumvma2  24142  pclogsum  24143  vmasum  24144  logfac2  24145  chpval2  24146  chpchtsum  24147  logfaclbnd  24150  logexprlim  24153  logfacrlim2  24154  pcbcctr  24204  bposlem1  24212  bposlem2  24213  lgscllem  24231  lgsval2lem  24234  lgsval4a  24246  lgsneg  24247  lgsdir  24258  lgsdilem2  24259  lgsdi  24260  lgsne0  24261  lgsqrlem2  24270  lgseisenlem1  24277  lgseisenlem2  24278  lgseisenlem3  24279  lgseisenlem4  24280  lgseisen  24281  lgsquadlem1  24282  lgsquadlem2  24283  lgsquadlem3  24284  chebbnd1lem1  24307  vmadivsum  24320  vmadivsumb  24321  rplogsumlem2  24323  dchrisum0lem1a  24324  rpvmasumlem  24325  dchrisumlem2  24328  dchrmusum2  24332  dchrvmasumlem1  24333  dchrvmasum2lem  24334  dchrvmasum2if  24335  dchrvmasumlem2  24336  dchrvmasumlem3  24337  dchrvmasumiflem1  24339  dchrvmasumiflem2  24340  dchrisum0fno1  24349  rpvmasum2  24350  dchrisum0re  24351  dchrisum0lem1b  24353  dchrisum0lem1  24354  dchrisum0lem2a  24355  dchrisum0lem2  24356  dchrisum0lem3  24357  dchrisum0  24358  dchrmusumlem  24360  dchrvmasumlem  24361  rplogsum  24365  mudivsum  24368  mulogsumlem  24369  mulogsum  24370  mulog2sumlem1  24372  mulog2sumlem2  24373  mulog2sumlem3  24374  vmalogdivsum2  24376  vmalogdivsum  24377  2vmadivsumlem  24378  log2sumbnd  24382  selberglem1  24383  selberglem2  24384  selberglem3  24385  selberg  24386  selbergb  24387  selberg2lem  24388  selberg2  24389  selberg2b  24390  chpdifbndlem1  24391  logdivbnd  24394  selberg3lem1  24395  selberg3lem2  24396  selberg3  24397  selberg4lem1  24398  selberg4  24399  pntrsumo1  24403  pntrsumbnd  24404  pntrsumbnd2  24405  selbergr  24406  selberg3r  24407  selberg4r  24408  selberg34r  24409  pntsf  24411  pntsval2  24414  pntrlog2bndlem1  24415  pntrlog2bndlem2  24416  pntrlog2bndlem3  24417  pntrlog2bndlem4  24418  pntrlog2bndlem5  24419  pntrlog2bndlem6  24421  pntrlog2bnd  24422  pntpbnd2  24425  pntlemf  24443  pntlemk  24444  pntlemo  24445  iseupa  25693  eupares  25703  eupap1  25704  dipcl  26351  dipcn  26359  sspival  26377  esumpcvgval  28899  esumpmono  28900  esumcvg  28907  esumcvgsum  28909  eulerpartlemgc  29195  ballotlemfc0  29325  ballotlemfcc  29326  ballotlemimin  29338  ballotlemic  29339  ballotlem1c  29340  ballotlemsel1i  29345  ballotlemsf1o  29346  ballotlemiminOLD  29376  ballotlemicOLD  29377  ballotlem1cOLD  29378  ballotlemsel1iOLD  29383  ballotlemsf1oOLD  29384  erdszelem4  29917  erdszelem8  29921  erdsze2lem2  29927  cvmliftlem2  30009  cvmliftlem6  30013  cvmliftlem8  30015  cvmliftlem9  30016  cvmliftlem10  30017  bcprod  30374  faclim  30382  poimirlem6  31946  poimirlem7  31947  poimirlem8  31948  poimirlem9  31949  poimirlem11  31951  poimirlem13  31953  poimirlem14  31954  poimirlem15  31955  poimirlem16  31956  poimirlem17  31957  poimirlem18  31958  poimirlem22  31962  poimirlem32  31972  mblfinlem2  31978  eldioph3b  35607  diophin  35615  diophun  35616  eldiophss  35617  irrapxlem4  35669  sumnnodd  37710  stoweidlem34  37895  wallispilem4  37930  wallispi  37932  wallispi2lem1  37933  wallispi2  37935  stirlinglem5  37940  stirlinglem7  37942  stirlinglem10  37945  stirlinglem12  37947  fourierdlem83  38053  fourierdlem112  38082  caratheodorylem2  38348  hoidmvlelem2  38418  hoidmvlelem3  38419  pfxfv0  38941  pfxfvlsw  38944  altgsumbcALT  40187  nn0sumshdiglemA  40483  nn0sumshdiglemB  40484
  Copyright terms: Public domain W3C validator