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

Theorem elfznn 11072
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 11051 . 2  |-  ( K  e.  ( 1 ... N )  ->  K  e.  ZZ )
2 elfzle1 11052 . 2  |-  ( K  e.  ( 1 ... N )  ->  1  <_  K )
3 elnnz1 10299 . 2  |-  ( K  e.  NN  <->  ( K  e.  ZZ  /\  1  <_  K ) )
41, 2, 3sylanbrc 646 1  |-  ( K  e.  ( 1 ... N )  ->  K  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   class class class wbr 4204  (class class class)co 6073   1c1 8983    <_ cle 9113   NNcn 9992   ZZcz 10274   ...cfz 11035
This theorem is referenced by:  elfz1end  11073  fzossnn  11164  bcm1k  11598  bcpasc  11604  seqcoll  11704  isercolllem2  12451  isercolllem3  12452  isercoll  12453  sumeq2ii  12479  summolem3  12500  summolem2a  12501  fsum  12506  sumz  12508  fsumconst  12565  o1fsum  12584  binomlem  12600  incexc2  12610  climcndslem1  12621  climcndslem2  12622  climcnds  12623  harmonic  12630  arisum2  12632  trireciplem  12633  geo2sum  12642  geo2lim  12644  rpnnen2lem10  12815  fzm1ndvds  12893  phicl  13150  prmdivdiv  13168  pcfac  13260  pcbc  13261  prmreclem2  13277  prmreclem3  13278  prmreclem4  13279  prmreclem5  13280  prmreclem6  13281  prmrec  13282  4sqlem13  13317  vdwlem2  13342  vdwlem3  13343  vdwlem10  13350  vdwlem12  13352  mulgnnsubcl  14894  mulgnn0z  14902  mulgnndir  14904  oddvdsnn0  15174  odnncl  15175  gexcl3  15213  efgsres  15362  mulgnn0di  15440  gsumconst  15524  1stcfb  17500  1stckgenlem  17577  lebnumii  18983  ovollb2lem  19376  ovolunlem1a  19384  ovoliunlem1  19390  ovoliunlem2  19391  ovoliun2  19394  ovolscalem1  19401  ovolicc2lem4  19408  voliunlem1  19436  volsup  19442  ioombl1lem4  19447  uniioovol  19463  uniioombllem3a  19468  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  uniioombllem6  19472  dvply1  20193  aaliou3lem5  20256  aaliou3lem6  20257  dvtaylp  20278  taylthlem2  20282  pserdvlem2  20336  logfac  20487  atantayl  20769  birthdaylem2  20783  emcllem1  20826  emcllem2  20827  emcllem3  20828  emcllem5  20830  emcllem7  20832  harmoniclbnd  20839  harmonicubnd  20840  harmonicbnd4  20841  fsumharmonic  20842  wilthlem1  20843  wilthlem2  20844  ftalem5  20851  basellem1  20855  basellem8  20862  chpf  20898  efchpcl  20900  chpp1  20930  chpwordi  20932  prmorcht  20953  dvdsflf1o  20964  dvdsflsumcom  20965  chtlepsi  20982  fsumvma2  20990  pclogsum  20991  vmasum  20992  logfac2  20993  chpval2  20994  chpchtsum  20995  logfaclbnd  20998  logexprlim  21001  logfacrlim2  21002  pcbcctr  21052  bposlem1  21060  bposlem2  21061  lgscllem  21079  lgsval2lem  21082  lgsval4a  21094  lgsneg  21095  lgsdir  21106  lgsdilem2  21107  lgsdi  21108  lgsne0  21109  lgsqrlem2  21118  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem3  21127  lgseisenlem4  21128  lgseisen  21129  lgsquadlem1  21130  lgsquadlem2  21131  lgsquadlem3  21132  chebbnd1lem1  21155  vmadivsum  21168  vmadivsumb  21169  rplogsumlem2  21171  dchrisum0lem1a  21172  rpvmasumlem  21173  dchrisumlem2  21176  dchrmusum2  21180  dchrvmasumlem1  21181  dchrvmasum2lem  21182  dchrvmasum2if  21183  dchrvmasumlem2  21184  dchrvmasumlem3  21185  dchrvmasumiflem1  21187  dchrvmasumiflem2  21188  dchrisum0fno1  21197  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lem1b  21201  dchrisum0lem1  21202  dchrisum0lem2a  21203  dchrisum0lem2  21204  dchrisum0lem3  21205  dchrisum0  21206  dchrmusumlem  21208  dchrvmasumlem  21209  rplogsum  21213  mudivsum  21216  mulogsumlem  21217  mulogsum  21218  mulog2sumlem1  21220  mulog2sumlem2  21221  mulog2sumlem3  21222  vmalogdivsum2  21224  vmalogdivsum  21225  2vmadivsumlem  21226  log2sumbnd  21230  selberglem1  21231  selberglem2  21232  selberglem3  21233  selberg  21234  selbergb  21235  selberg2lem  21236  selberg2  21237  selberg2b  21238  chpdifbndlem1  21239  logdivbnd  21242  selberg3lem1  21243  selberg3lem2  21244  selberg3  21245  selberg4lem1  21246  selberg4  21247  pntrsumo1  21251  pntrsumbnd  21252  pntrsumbnd2  21253  selbergr  21254  selberg3r  21255  selberg4r  21256  selberg34r  21257  pntsf  21259  pntsval2  21262  pntrlog2bndlem1  21263  pntrlog2bndlem2  21264  pntrlog2bndlem3  21265  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntrlog2bndlem6  21269  pntrlog2bnd  21270  pntpbnd2  21273  pntlemf  21291  pntlemk  21292  pntlemo  21293  iseupa  21679  eupares  21689  eupap1  21690  dipcl  22203  dipcn  22211  sspival  22229  esumpcvgval  24460  esumpmono  24461  esumcvg  24468  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemimin  24755  ballotlemic  24756  ballotlem1c  24757  ballotlemsel1i  24762  ballotlemsf1o  24763  lgamgulm2  24812  lgamcvglem  24816  lgamcvg2  24831  gamcvg2lem  24835  erdszelem4  24872  erdszelem8  24876  erdsze2lem2  24882  cvmliftlem2  24965  cvmliftlem6  24969  cvmliftlem8  24971  cvmliftlem9  24972  cvmliftlem10  24973  prodeq2ii  25231  prodmolem3  25251  prodmolem2a  25252  fprod  25259  prod1  25262  fprodfac  25288  fprodconst  25294  risefallfac  25332  risefacfac  25343  fallfacval4  25351  faclim  25357  bpolydiflem  26092  mblfinlem  26234  eldioph3b  26814  diophin  26822  diophun  26823  eldiophss  26824  fz1ssnn  26862  irrapxlem4  26879  stoweidlem34  27750  wallispilem4  27784  wallispi  27786  wallispi2lem1  27787  wallispi2  27789  stirlinglem5  27794  stirlinglem7  27796  stirlinglem10  27799  stirlinglem12  27801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9038  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-mulcom 9046  ax-addass 9047  ax-mulass 9048  ax-distr 9049  ax-i2m1 9050  ax-1ne0 9051  ax-1rid 9052  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055  ax-pre-lttri 9056  ax-pre-lttrn 9057  ax-pre-ltadd 9058  ax-pre-mulgt0 9059
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-sub 9285  df-neg 9286  df-nn 9993  df-z 10275  df-uz 10481  df-fz 11036
  Copyright terms: Public domain W3C validator