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

Theorem elfznn 11579
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 11554 . 2  |-  ( K  e.  ( 1 ... N )  ->  K  e.  ZZ )
2 elfzle1 11555 . 2  |-  ( K  e.  ( 1 ... N )  ->  1  <_  K )
3 elnnz1 10773 . 2  |-  ( K  e.  NN  <->  ( K  e.  ZZ  /\  1  <_  K ) )
41, 2, 3sylanbrc 664 1  |-  ( K  e.  ( 1 ... N )  ->  K  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   class class class wbr 4390  (class class class)co 6190   1c1 9384    <_ cle 9520   NNcn 10423   ZZcz 10747   ...cfz 11538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-om 6577  df-1st 6677  df-2nd 6678  df-recs 6932  df-rdg 6966  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-nn 10424  df-z 10748  df-uz 10963  df-fz 11539
This theorem is referenced by:  elfz1end  11580  fzossnn  11695  bcm1k  12192  bcpasc  12198  seqcoll  12318  swrd0fv0  12438  swrd0fvlsw  12441  isercolllem2  13245  isercolllem3  13246  isercoll  13247  sumeq2ii  13272  summolem3  13293  summolem2a  13294  fsum  13299  sumz  13301  fsumconst  13359  o1fsum  13378  binomlem  13394  incexc2  13403  climcndslem1  13414  climcndslem2  13415  climcnds  13416  harmonic  13423  arisum2  13425  trireciplem  13426  geo2sum  13435  geo2lim  13437  rpnnen2lem10  13608  fzm1ndvds  13687  phicl  13946  prmdivdiv  13964  pcfac  14063  pcbc  14064  prmreclem2  14080  prmreclem3  14081  prmreclem4  14082  prmreclem5  14083  prmreclem6  14084  prmrec  14085  4sqlem13  14120  vdwlem2  14145  vdwlem3  14146  vdwlem10  14153  vdwlem12  14155  mulgnnsubcl  15741  mulgnn0z  15749  mulgnndir  15751  oddvdsnn0  16151  odnncl  16152  gexcl3  16190  efgsres  16339  mulgnn0di  16417  gsumconst  16532  srgbinomlem4  16747  1stcfb  19165  1stckgenlem  19242  lebnumii  20654  ovollb2lem  21087  ovolunlem1a  21095  ovoliunlem1  21101  ovoliunlem2  21102  ovoliun2  21105  ovolscalem1  21112  ovolicc2lem4  21119  voliunlem1  21147  volsup  21153  ioombl1lem4  21158  uniioovol  21175  uniioombllem3a  21180  uniioombllem3  21181  uniioombllem4  21182  uniioombllem5  21183  uniioombllem6  21184  dvply1  21866  aaliou3lem5  21929  aaliou3lem6  21930  dvtaylp  21951  taylthlem2  21955  pserdvlem2  22009  logfac  22165  atantayl  22448  birthdaylem2  22462  emcllem1  22505  emcllem2  22506  emcllem3  22507  emcllem5  22509  emcllem7  22511  harmoniclbnd  22518  harmonicubnd  22519  harmonicbnd4  22520  fsumharmonic  22521  wilthlem1  22522  wilthlem2  22523  ftalem5  22530  basellem1  22534  basellem8  22541  chpf  22577  efchpcl  22579  chpp1  22609  chpwordi  22611  prmorcht  22632  dvdsflf1o  22643  dvdsflsumcom  22644  chtlepsi  22661  fsumvma2  22669  pclogsum  22670  vmasum  22671  logfac2  22672  chpval2  22673  chpchtsum  22674  logfaclbnd  22677  logexprlim  22680  logfacrlim2  22681  pcbcctr  22731  bposlem1  22739  bposlem2  22740  lgscllem  22758  lgsval2lem  22761  lgsval4a  22773  lgsneg  22774  lgsdir  22785  lgsdilem2  22786  lgsdi  22787  lgsne0  22788  lgsqrlem2  22797  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem3  22806  lgseisenlem4  22807  lgseisen  22808  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  chebbnd1lem1  22834  vmadivsum  22847  vmadivsumb  22848  rplogsumlem2  22850  dchrisum0lem1a  22851  rpvmasumlem  22852  dchrisumlem2  22855  dchrmusum2  22859  dchrvmasumlem1  22860  dchrvmasum2lem  22861  dchrvmasum2if  22862  dchrvmasumlem2  22863  dchrvmasumlem3  22864  dchrvmasumiflem1  22866  dchrvmasumiflem2  22867  dchrisum0fno1  22876  rpvmasum2  22877  dchrisum0re  22878  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0lem3  22884  dchrisum0  22885  dchrmusumlem  22887  dchrvmasumlem  22888  rplogsum  22892  mudivsum  22895  mulogsumlem  22896  mulogsum  22897  mulog2sumlem1  22899  mulog2sumlem2  22900  mulog2sumlem3  22901  vmalogdivsum2  22903  vmalogdivsum  22904  2vmadivsumlem  22905  log2sumbnd  22909  selberglem1  22910  selberglem2  22911  selberglem3  22912  selberg  22913  selbergb  22914  selberg2lem  22915  selberg2  22916  selberg2b  22917  chpdifbndlem1  22918  logdivbnd  22921  selberg3lem1  22922  selberg3lem2  22923  selberg3  22924  selberg4lem1  22925  selberg4  22926  pntrsumo1  22930  pntrsumbnd  22931  pntrsumbnd2  22932  selbergr  22933  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntsf  22938  pntsval2  22941  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntpbnd2  22952  pntlemf  22970  pntlemk  22971  pntlemo  22972  iseupa  23721  eupares  23731  eupap1  23732  dipcl  24245  dipcn  24253  sspival  24271  esumpcvgval  26661  esumpmono  26662  esumcvg  26669  eulerpartlemgc  26879  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemimin  27022  ballotlemic  27023  ballotlem1c  27024  ballotlemsel1i  27029  ballotlemsf1o  27030  lgamgulm2  27156  lgamcvglem  27160  lgamcvg2  27175  gamcvg2lem  27179  erdszelem4  27216  erdszelem8  27220  erdsze2lem2  27226  cvmliftlem2  27309  cvmliftlem6  27313  cvmliftlem8  27315  cvmliftlem9  27316  cvmliftlem10  27317  prodeq2ii  27560  prodmolem3  27580  prodmolem2a  27581  fprod  27588  prod1  27591  fprodfac  27617  fprodconst  27623  risefallfac  27661  risefacfac  27672  fallfacval4  27680  faclim  27686  bpolydiflem  28331  mblfinlem2  28567  eldioph3b  29241  diophin  29249  diophun  29250  eldiophss  29251  fz1ssnn  29287  irrapxlem4  29304  stoweidlem34  29967  wallispilem4  30001  wallispi  30003  wallispi2lem1  30004  wallispi2  30006  stirlinglem5  30011  stirlinglem7  30013  stirlinglem10  30016  stirlinglem12  30018  altgsumbcALT  30888  chfacfscmulgsum  31314  chfacfpmmulgsum  31318  chfacfpmmulgsum2  31319  cayhamlem1  31320  cpmadugsumlemF  31330
  Copyright terms: Public domain W3C validator