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

Theorem elfznn 12196
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 12168 . 2 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2 elfzle1 12170 . 2 (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3 elnnz1 11236 . 2 (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
41, 2, 3sylanbrc 694 1 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976   class class class wbr 4577  (class class class)co 6527  1c1 9793  cle 9931  cn 10867  cz 11210  ...cfz 12152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-z 11211  df-uz 11520  df-fz 12153
This theorem is referenced by:  elfz1end  12197  fz1ssnn  12198  fzossnn  12339  bcm1k  12919  bcpasc  12925  seqcoll  13057  swrd0fv0  13238  swrd0fvlsw  13241  isercolllem2  14190  isercolllem3  14191  isercoll  14192  sumeq2ii  14217  summolem3  14238  summolem2a  14239  fsum  14244  sumz  14246  fsumconst  14310  o1fsum  14332  binomlem  14346  incexc2  14355  climcndslem1  14366  climcndslem2  14367  climcnds  14368  harmonic  14376  arisum2  14378  trireciplem  14379  geo2sum  14389  geo2lim  14391  prodeq2ii  14428  prodmolem3  14448  prodmolem2a  14449  fprod  14456  prod1  14459  fprodfac  14488  fprodconst  14493  risefallfac  14540  risefacfac  14551  fallfacval4  14559  bpolydiflem  14570  rpnnen2lem10  14737  fzm1ndvds  14828  pwp1fsum  14898  lcmflefac  15145  phicl  15258  prmdivdiv  15276  pcfac  15387  pcbc  15388  prmreclem2  15405  prmreclem3  15406  prmreclem4  15407  prmreclem5  15408  prmreclem6  15409  prmrec  15410  4sqlem13  15445  vdwlem2  15470  vdwlem3  15471  vdwlem10  15478  vdwlem12  15480  prmocl  15522  prmop1  15526  fvprmselelfz  15532  fvprmselgcd1  15533  prmolefac  15534  prmodvdslcmf  15535  prmgapprmo  15550  mulgnnsubcl  17322  mulgnn0z  17336  mulgnndir  17338  mulgnndirOLD  17339  oddvdsnn0  17732  odnncl  17733  gexcl3  17771  efgsres  17920  mulgnn0di  18000  gsumconst  18103  srgbinomlem4  18312  chfacfscmulgsum  20426  chfacfpmmulgsum  20430  chfacfpmmulgsum2  20431  cayhamlem1  20432  cpmadugsumlemF  20442  1stcfb  21000  1stckgenlem  21108  lebnumii  22504  ovollb2lem  22980  ovolunlem1a  22988  ovoliunlem1  22994  ovoliunlem2  22995  ovoliun2  22998  ovolscalem1  23005  ovolicc2lem4  23012  voliunlem1  23042  volsup  23048  ioombl1lem4  23053  uniioovol  23070  uniioombllem3a  23075  uniioombllem3  23076  uniioombllem4  23077  uniioombllem5  23078  uniioombllem6  23079  dvply1  23760  aaliou3lem5  23823  aaliou3lem6  23824  dvtaylp  23845  taylthlem2  23849  pserdvlem2  23903  logfac  24068  atantayl  24381  birthdaylem2  24396  emcllem1  24439  emcllem2  24440  emcllem3  24441  emcllem5  24443  emcllem7  24445  harmoniclbnd  24452  harmonicubnd  24453  harmonicbnd4  24454  fsumharmonic  24455  lgamcvg2  24498  gamcvg2lem  24502  wilthlem1  24511  wilthlem2  24512  ftalem5  24520  basellem1  24524  basellem8  24531  chpf  24566  efchpcl  24568  chpp1  24598  chpwordi  24600  prmorcht  24621  dvdsflf1o  24630  dvdsflsumcom  24631  chtlepsi  24648  fsumvma2  24656  pclogsum  24657  vmasum  24658  logfac2  24659  chpval2  24660  chpchtsum  24661  logfaclbnd  24664  logexprlim  24667  logfacrlim2  24668  pcbcctr  24718  bposlem1  24726  bposlem2  24727  lgscllem  24746  lgsval2lem  24749  lgsval4a  24761  lgsneg  24763  lgsdir  24774  lgsdilem2  24775  lgsdi  24776  lgsne0  24777  lgsqrlem2  24789  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgseisenlem4  24820  lgseisen  24821  lgsquadlem1  24822  lgsquadlem2  24823  lgsquadlem3  24824  2lgslem1a1  24831  chebbnd1lem1  24875  vmadivsum  24888  vmadivsumb  24889  rplogsumlem2  24891  dchrisum0lem1a  24892  rpvmasumlem  24893  dchrisumlem2  24896  dchrmusum2  24900  dchrvmasumlem1  24901  dchrvmasum2lem  24902  dchrvmasum2if  24903  dchrvmasumlem2  24904  dchrvmasumlem3  24905  dchrvmasumiflem1  24907  dchrvmasumiflem2  24908  dchrisum0fno1  24917  rpvmasum2  24918  dchrisum0re  24919  dchrisum0lem1b  24921  dchrisum0lem1  24922  dchrisum0lem2a  24923  dchrisum0lem2  24924  dchrisum0lem3  24925  dchrisum0  24926  dchrmusumlem  24928  dchrvmasumlem  24929  rplogsum  24933  mudivsum  24936  mulogsumlem  24937  mulogsum  24938  mulog2sumlem1  24940  mulog2sumlem2  24941  mulog2sumlem3  24942  vmalogdivsum2  24944  vmalogdivsum  24945  2vmadivsumlem  24946  log2sumbnd  24950  selberglem1  24951  selberglem2  24952  selberglem3  24953  selberg  24954  selbergb  24955  selberg2lem  24956  selberg2  24957  selberg2b  24958  chpdifbndlem1  24959  logdivbnd  24962  selberg3lem1  24963  selberg3lem2  24964  selberg3  24965  selberg4lem1  24966  selberg4  24967  pntrsumo1  24971  pntrsumbnd  24972  pntrsumbnd2  24973  selbergr  24974  selberg3r  24975  selberg4r  24976  selberg34r  24977  pntsf  24979  pntsval2  24982  pntrlog2bndlem1  24983  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntrlog2bndlem6  24989  pntrlog2bnd  24990  pntpbnd2  24993  pntlemf  25011  pntlemk  25012  pntlemo  25013  eupares  26268  eupap1  26269  dipcl  26755  dipcn  26763  sspival  26781  esumpcvgval  29273  esumpmono  29274  esumcvg  29281  esumcvgsum  29283  eulerpartlemgc  29557  ballotlemfc0  29687  ballotlemfcc  29688  ballotlemimin  29700  ballotlemic  29701  ballotlem1c  29702  ballotlemsel1i  29707  ballotlemsf1o  29708  erdszelem4  30236  erdszelem8  30240  erdsze2lem2  30246  cvmliftlem2  30328  cvmliftlem6  30332  cvmliftlem8  30334  cvmliftlem9  30335  cvmliftlem10  30336  bcprod  30683  faclim  30691  poimirlem6  32388  poimirlem7  32389  poimirlem8  32390  poimirlem9  32391  poimirlem11  32393  poimirlem13  32395  poimirlem14  32396  poimirlem15  32397  poimirlem16  32398  poimirlem17  32399  poimirlem18  32400  poimirlem22  32404  poimirlem32  32414  mblfinlem2  32420  eldioph3b  36149  diophin  36157  diophun  36158  eldiophss  36159  irrapxlem4  36210  sumnnodd  38501  stoweidlem34  38731  wallispilem4  38765  wallispi  38767  wallispi2lem1  38768  wallispi2  38770  stirlinglem5  38775  stirlinglem7  38777  stirlinglem10  38780  stirlinglem12  38782  fourierdlem83  38886  fourierdlem112  38915  caratheodorylem2  39221  hoidmvlelem2  39290  hoidmvlelem3  39291  pwdif  39844  pfxfv0  40068  pfxfvlsw  40071  eucrct2eupth  41415  altgsumbcALT  41926  nn0sumshdiglemA  42213  nn0sumshdiglemB  42214
  Copyright terms: Public domain W3C validator