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

Theorem elfznn 13476
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 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Proof of Theorem elfznn
StepHypRef Expression
1 elfzelz 13447 . 2 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2 elfzle1 13450 . 2 (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3 elnnz1 12534 . 2 (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
41, 2, 3sylanbrc 584 1 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5106  (class class class)co 7358  1c1 11057  cle 11195  cn 12158  cz 12504  ...cfz 13430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-nn 12159  df-z 12505  df-uz 12769  df-fz 13431
This theorem is referenced by:  elfz1end  13477  fz1ssnn  13478  bcm1k  14221  bcpasc  14227  seqcoll  14369  pfxfv0  14586  pfxfvlsw  14589  isercolllem2  15556  isercolllem3  15557  isercoll  15558  sumeq2ii  15583  summolem3  15604  summolem2a  15605  fsum  15610  sumz  15612  fsumconst  15680  o1fsum  15703  binomlem  15719  incexc2  15728  climcndslem1  15739  climcndslem2  15740  climcnds  15741  harmonic  15749  arisum2  15751  trireciplem  15752  pwdif  15758  geo2sum  15763  geo2lim  15765  prodeq2ii  15801  prodmolem3  15821  prodmolem2a  15822  fprod  15829  prod1  15832  fprodfac  15861  fprodconst  15866  risefallfac  15912  risefacfac  15923  fallfacval4  15931  bpolydiflem  15942  rpnnen2lem10  16110  fzm1ndvds  16209  pwp1fsum  16278  lcmflefac  16529  phicl  16646  prmdivdiv  16664  pcfac  16776  pcbc  16777  prmreclem2  16794  prmreclem3  16795  prmreclem4  16796  prmreclem5  16797  prmreclem6  16798  prmrec  16799  4sqlem13  16834  vdwlem2  16859  vdwlem3  16860  vdwlem10  16867  vdwlem12  16869  prmocl  16911  prmop1  16915  fvprmselelfz  16921  fvprmselgcd1  16922  prmolefac  16923  prmodvdslcmf  16924  prmgapprmo  16939  mulgnngsum  18886  mulgnnsubcl  18893  mulgnn0z  18908  mulgnndir  18910  oddvdsnn0  19331  odnncl  19332  gexcl3  19374  efgsres  19525  mulgnn0di  19609  gsumconst  19716  srgbinomlem4  19965  chfacfscmulgsum  22225  chfacfpmmulgsum  22229  chfacfpmmulgsum2  22230  cayhamlem1  22231  cpmadugsumlemF  22241  lebnumii  24345  ovollb2lem  24868  ovolunlem1a  24876  ovoliunlem1  24882  ovoliunlem2  24883  ovoliun2  24886  ovolscalem1  24893  ovolicc2lem4  24900  voliunlem1  24930  volsup  24936  ioombl1lem4  24941  uniioovol  24959  uniioombllem3a  24964  uniioombllem3  24965  uniioombllem4  24966  uniioombllem5  24967  uniioombllem6  24968  dvply1  25660  aaliou3lem5  25723  aaliou3lem6  25724  dvtaylp  25745  taylthlem2  25749  pserdvlem2  25803  logfac  25972  atantayl  26303  birthdaylem2  26318  emcllem1  26361  emcllem2  26362  emcllem3  26363  emcllem5  26365  emcllem7  26367  harmoniclbnd  26374  harmonicubnd  26375  harmonicbnd4  26376  fsumharmonic  26377  lgamcvg2  26420  gamcvg2lem  26424  wilthlem1  26433  wilthlem2  26434  ftalem5  26442  basellem1  26446  basellem8  26453  chpf  26488  efchpcl  26490  chpp1  26520  chpwordi  26522  prmorcht  26543  dvdsflf1o  26552  dvdsflsumcom  26553  chtlepsi  26570  fsumvma2  26578  pclogsum  26579  vmasum  26580  logfac2  26581  chpval2  26582  chpchtsum  26583  logfaclbnd  26586  logexprlim  26589  logfacrlim2  26590  pcbcctr  26640  bposlem1  26648  bposlem2  26649  lgscllem  26668  lgsval2lem  26671  lgsval4a  26683  lgsneg  26685  lgsdir  26696  lgsdilem2  26697  lgsdi  26698  lgsne0  26699  lgsqrlem2  26711  lgseisenlem1  26739  lgseisenlem2  26740  lgseisenlem3  26741  lgseisenlem4  26742  lgseisen  26743  lgsquadlem1  26744  lgsquadlem2  26745  lgsquadlem3  26746  2lgslem1a1  26753  chebbnd1lem1  26833  vmadivsum  26846  vmadivsumb  26847  rplogsumlem2  26849  dchrisum0lem1a  26850  rpvmasumlem  26851  dchrisumlem2  26854  dchrmusum2  26858  dchrvmasumlem1  26859  dchrvmasum2lem  26860  dchrvmasum2if  26861  dchrvmasumlem2  26862  dchrvmasumlem3  26863  dchrvmasumiflem1  26865  dchrvmasumiflem2  26866  dchrisum0fno1  26875  rpvmasum2  26876  dchrisum0re  26877  dchrisum0lem1b  26879  dchrisum0lem1  26880  dchrisum0lem2a  26881  dchrisum0lem2  26882  dchrisum0lem3  26883  dchrisum0  26884  dchrmusumlem  26886  dchrvmasumlem  26887  rplogsum  26891  mudivsum  26894  mulogsumlem  26895  mulogsum  26896  mulog2sumlem1  26898  mulog2sumlem2  26899  mulog2sumlem3  26900  vmalogdivsum2  26902  vmalogdivsum  26903  2vmadivsumlem  26904  log2sumbnd  26908  selberglem1  26909  selberglem2  26910  selberglem3  26911  selberg  26912  selbergb  26913  selberg2lem  26914  selberg2  26915  selberg2b  26916  chpdifbndlem1  26917  logdivbnd  26920  selberg3lem1  26921  selberg3lem2  26922  selberg3  26923  selberg4lem1  26924  selberg4  26925  pntrsumo1  26929  pntrsumbnd  26930  pntrsumbnd2  26931  selbergr  26932  selberg3r  26933  selberg4r  26934  selberg34r  26935  pntsf  26937  pntsval2  26940  pntrlog2bndlem1  26941  pntrlog2bndlem2  26942  pntrlog2bndlem3  26943  pntrlog2bndlem4  26944  pntrlog2bndlem5  26945  pntrlog2bndlem6  26947  pntrlog2bnd  26948  pntpbnd2  26951  pntlemf  26969  pntlemk  26970  pntlemo  26971  eucrct2eupth  29231  dipcl  29696  dipcn  29704  prmdvdsbc  31761  freshmansdream  32116  esumpcvgval  32734  esumpmono  32735  esumcvg  32742  esumcvgsum  32744  eulerpartlemgc  33019  ballotlemfc0  33149  ballotlemfcc  33150  ballotlemic  33163  ballotlem1c  33164  ballotlemsel1i  33169  ballotlemsf1o  33170  erdszelem4  33845  erdszelem8  33849  erdsze2lem2  33855  cvmliftlem2  33937  cvmliftlem6  33941  cvmliftlem8  33943  cvmliftlem9  33944  cvmliftlem10  33945  bcprod  34367  faclim  34375  poimirlem6  36130  poimirlem7  36131  poimirlem8  36132  poimirlem9  36133  poimirlem11  36135  poimirlem13  36137  poimirlem14  36138  poimirlem15  36139  poimirlem16  36140  poimirlem17  36141  poimirlem18  36142  poimirlem22  36146  poimirlem32  36156  mblfinlem2  36162  aks4d1p1p2  40573  aks4d1p1p4  40574  aks4d1p1  40579  aks4d1p3  40581  aks4d1p4  40582  aks4d1p5  40583  aks4d1p6  40584  aks4d1p7d1  40585  aks4d1p7  40586  aks4d1p8  40590  aks4d1p9  40591  sticksstones1  40600  sticksstones2  40601  sticksstones3  40602  sticksstones6  40605  sticksstones7  40606  sticksstones10  40609  sticksstones12a  40611  sticksstones12  40612  metakunt1  40623  metakunt2  40624  metakunt6  40628  metakunt7  40629  metakunt8  40630  metakunt9  40631  metakunt11  40633  metakunt15  40637  metakunt16  40638  metakunt21  40643  metakunt22  40644  metakunt27  40649  metakunt29  40651  metakunt30  40652  eldioph3b  41131  diophin  41138  diophun  41139  eldiophss  41140  irrapxlem4  41191  sumnnodd  43957  stoweidlem34  44361  wallispilem4  44395  wallispi  44397  wallispi2lem1  44398  wallispi2  44400  stirlinglem5  44405  stirlinglem7  44407  stirlinglem10  44410  stirlinglem12  44412  fourierdlem83  44516  fourierdlem112  44545  caratheodorylem2  44854  hoidmvlelem2  44923  hoidmvlelem3  44924  altgsumbcALT  46515  nn0sumshdiglemA  46791  nn0sumshdiglemB  46792
  Copyright terms: Public domain W3C validator