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

Theorem elfznn 10866
Description: A member of a finite set of sequential integers starting at 1 is a natural number. (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 10845 . 2  |-  ( K  e.  ( 1 ... N )  ->  K  e.  ZZ )
2 elfzle1 10846 . 2  |-  ( K  e.  ( 1 ... N )  ->  1  <_  K )
3 elnnz1 10096 . 2  |-  ( K  e.  NN  <->  ( K  e.  ZZ  /\  1  <_  K ) )
41, 2, 3sylanbrc 645 1  |-  ( K  e.  ( 1 ... N )  ->  K  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1701   class class class wbr 4060  (class class class)co 5900   1c1 8783    <_ cle 8913   NNcn 9791   ZZcz 10071   ...cfz 10829
This theorem is referenced by:  elfz1end  10867  bcm1k  11374  bcpasc  11380  seqcoll  11448  isercolllem2  12186  isercolllem3  12187  isercoll  12188  sumeq2ii  12213  summolem3  12234  summolem2a  12235  fsum  12240  sumz  12242  fsumconst  12299  o1fsum  12318  binomlem  12334  incexc2  12344  climcndslem1  12355  climcndslem2  12356  climcnds  12357  harmonic  12364  arisum2  12366  trireciplem  12367  geo2sum  12376  geo2lim  12378  rpnnen2lem10  12549  fzm1ndvds  12627  phicl  12884  prmdivdiv  12902  pcfac  12994  pcbc  12995  prmreclem2  13011  prmreclem3  13012  prmreclem4  13013  prmreclem5  13014  prmreclem6  13015  prmrec  13016  4sqlem13  13051  vdwlem2  13076  vdwlem3  13077  vdwlem10  13084  vdwlem12  13086  mulgnnsubcl  14628  mulgnn0z  14636  mulgnndir  14638  oddvdsnn0  14908  odnncl  14909  gexcl3  14947  efgsres  15096  mulgnn0di  15174  gsumconst  15258  1stcfb  17227  1stckgenlem  17304  lebnumii  18517  ovollb2lem  18900  ovolunlem1a  18908  ovoliunlem1  18914  ovoliunlem2  18915  ovoliun2  18918  ovolscalem1  18925  ovolicc2lem4  18932  voliunlem1  18960  volsup  18966  ioombl1lem4  18971  uniioovol  18987  uniioombllem3a  18992  uniioombllem3  18993  uniioombllem4  18994  uniioombllem5  18995  uniioombllem6  18996  dvply1  19717  aaliou3lem5  19780  aaliou3lem6  19781  dvtaylp  19802  taylthlem2  19806  pserdvlem2  19857  logfac  20007  atantayl  20286  birthdaylem2  20300  emcllem1  20342  emcllem2  20343  emcllem3  20344  emcllem5  20346  emcllem7  20348  harmoniclbnd  20355  harmonicubnd  20356  harmonicbnd4  20357  fsumharmonic  20358  wilthlem1  20359  wilthlem2  20360  ftalem5  20367  basellem1  20371  basellem8  20378  chpf  20414  efchpcl  20416  chpp1  20446  chpwordi  20448  prmorcht  20469  dvdsflf1o  20480  dvdsflsumcom  20481  chtlepsi  20498  fsumvma2  20506  pclogsum  20507  vmasum  20508  logfac2  20509  chpval2  20510  chpchtsum  20511  logfaclbnd  20514  logexprlim  20517  logfacrlim2  20518  pcbcctr  20568  bposlem1  20576  bposlem2  20577  lgscllem  20595  lgsval2lem  20598  lgsval4a  20610  lgsneg  20611  lgsdir  20622  lgsdilem2  20623  lgsdi  20624  lgsne0  20625  lgsqrlem2  20634  lgseisenlem1  20641  lgseisenlem2  20642  lgseisenlem3  20643  lgseisenlem4  20644  lgseisen  20645  lgsquadlem1  20646  lgsquadlem2  20647  lgsquadlem3  20648  chebbnd1lem1  20671  vmadivsum  20684  vmadivsumb  20685  rplogsumlem2  20687  dchrisum0lem1a  20688  rpvmasumlem  20689  dchrisumlem2  20692  dchrmusum2  20696  dchrvmasumlem1  20697  dchrvmasum2lem  20698  dchrvmasum2if  20699  dchrvmasumlem2  20700  dchrvmasumlem3  20701  dchrvmasumiflem1  20703  dchrvmasumiflem2  20704  dchrisum0fno1  20713  rpvmasum2  20714  dchrisum0re  20715  dchrisum0lem1b  20717  dchrisum0lem1  20718  dchrisum0lem2a  20719  dchrisum0lem2  20720  dchrisum0lem3  20721  dchrisum0  20722  dchrmusumlem  20724  dchrvmasumlem  20725  rplogsum  20729  mudivsum  20732  mulogsumlem  20733  mulogsum  20734  mulog2sumlem1  20736  mulog2sumlem2  20737  mulog2sumlem3  20738  vmalogdivsum2  20740  vmalogdivsum  20741  2vmadivsumlem  20742  log2sumbnd  20746  selberglem1  20747  selberglem2  20748  selberglem3  20749  selberg  20750  selbergb  20751  selberg2lem  20752  selberg2  20753  selberg2b  20754  chpdifbndlem1  20755  logdivbnd  20758  selberg3lem1  20759  selberg3lem2  20760  selberg3  20761  selberg4lem1  20762  selberg4  20763  pntrsumo1  20767  pntrsumbnd  20768  pntrsumbnd2  20769  selbergr  20770  selberg3r  20771  selberg4r  20772  selberg34r  20773  pntsf  20775  pntsval2  20778  pntrlog2bndlem1  20779  pntrlog2bndlem2  20780  pntrlog2bndlem3  20781  pntrlog2bndlem4  20782  pntrlog2bndlem5  20783  pntrlog2bndlem6  20785  pntrlog2bnd  20786  pntpbnd2  20789  pntlemf  20807  pntlemk  20808  pntlemo  20809  dipcl  21343  dipcn  21351  sspival  21369  fzossnn  23299  esumpcvgval  23644  esumpmono  23645  esumcvg  23652  ballotlemfc0  23924  ballotlemfcc  23925  ballotlemimin  23937  ballotlemic  23938  ballotlem1c  23939  ballotlemsgt1  23942  ballotlemsel1i  23944  ballotlemsf1o  23945  erdszelem4  24009  erdszelem8  24013  erdsze2lem2  24019  cvmliftlem2  24101  cvmliftlem6  24105  cvmliftlem8  24107  cvmliftlem9  24108  cvmliftlem10  24109  iseupa  24165  eupares  24183  eupap1  24184  prodeq2ii  24416  prodmolem3  24436  prodmolem2a  24437  fprod  24444  prod1  24447  fprodfac  24469  faclim  24484  bpolydiflem  25175  eldioph3b  25992  diophin  26000  diophun  26001  eldiophss  26002  fz1ssnn  26040  irrapxlem4  26058  stoweidlem34  26931  wallispilem4  26965  wallispi  26967  wallispi2lem1  26968  wallispi2  26970  stirlinglem5  26975  stirlinglem10  26980  stirlinglem12  26982
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-er 6702  df-en 6907  df-dom 6908  df-sdom 6909  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-z 10072  df-uz 10278  df-fz 10830
  Copyright terms: Public domain W3C validator