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

Theorem elfznn 12926
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 12898 . 2 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2 elfzle1 12900 . 2 (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3 elnnz1 11997 . 2 (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
41, 2, 3sylanbrc 583 1 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105   class class class wbr 5058  (class class class)co 7145  1c1 10527  cle 10665  cn 11627  cz 11970  ...cfz 12882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-z 11971  df-uz 12233  df-fz 12883
This theorem is referenced by:  elfz1end  12927  fz1ssnn  12928  bcm1k  13665  bcpasc  13671  seqcoll  13812  pfxfv0  14044  pfxfvlsw  14047  isercolllem2  15012  isercolllem3  15013  isercoll  15014  sumeq2ii  15040  summolem3  15061  summolem2a  15062  fsum  15067  sumz  15069  fsumconst  15135  o1fsum  15158  binomlem  15174  incexc2  15183  climcndslem1  15194  climcndslem2  15195  climcnds  15196  harmonic  15204  arisum2  15206  trireciplem  15207  pwdif  15213  geo2sum  15219  geo2lim  15221  prodeq2ii  15257  prodmolem3  15277  prodmolem2a  15278  fprod  15285  prod1  15288  fprodfac  15317  fprodconst  15322  risefallfac  15368  risefacfac  15379  fallfacval4  15387  bpolydiflem  15398  rpnnen2lem10  15566  fzm1ndvds  15662  pwp1fsum  15732  lcmflefac  15982  phicl  16096  prmdivdiv  16114  pcfac  16225  pcbc  16226  prmreclem2  16243  prmreclem3  16244  prmreclem4  16245  prmreclem5  16246  prmreclem6  16247  prmrec  16248  4sqlem13  16283  vdwlem2  16308  vdwlem3  16309  vdwlem10  16316  vdwlem12  16318  prmocl  16360  prmop1  16364  fvprmselelfz  16370  fvprmselgcd1  16371  prmolefac  16372  prmodvdslcmf  16373  prmgapprmo  16388  mulgnngsum  18173  mulgnnsubcl  18180  mulgnn0z  18194  mulgnndir  18196  oddvdsnn0  18603  odnncl  18604  gexcl3  18643  efgsres  18795  mulgnn0di  18877  gsumconst  18985  srgbinomlem4  19224  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  chfacfpmmulgsum2  21403  cayhamlem1  21404  cpmadugsumlemF  21414  lebnumii  23499  ovollb2lem  24018  ovolunlem1a  24026  ovoliunlem1  24032  ovoliunlem2  24033  ovoliun2  24036  ovolscalem1  24043  ovolicc2lem4  24050  voliunlem1  24080  volsup  24086  ioombl1lem4  24091  uniioovol  24109  uniioombllem3a  24114  uniioombllem3  24115  uniioombllem4  24116  uniioombllem5  24117  uniioombllem6  24118  dvply1  24802  aaliou3lem5  24865  aaliou3lem6  24866  dvtaylp  24887  taylthlem2  24891  pserdvlem2  24945  logfac  25111  atantayl  25442  birthdaylem2  25458  emcllem1  25501  emcllem2  25502  emcllem3  25503  emcllem5  25505  emcllem7  25507  harmoniclbnd  25514  harmonicubnd  25515  harmonicbnd4  25516  fsumharmonic  25517  lgamcvg2  25560  gamcvg2lem  25564  wilthlem1  25573  wilthlem2  25574  ftalem5  25582  basellem1  25586  basellem8  25593  chpf  25628  efchpcl  25630  chpp1  25660  chpwordi  25662  prmorcht  25683  dvdsflf1o  25692  dvdsflsumcom  25693  chtlepsi  25710  fsumvma2  25718  pclogsum  25719  vmasum  25720  logfac2  25721  chpval2  25722  chpchtsum  25723  logfaclbnd  25726  logexprlim  25729  logfacrlim2  25730  pcbcctr  25780  bposlem1  25788  bposlem2  25789  lgscllem  25808  lgsval2lem  25811  lgsval4a  25823  lgsneg  25825  lgsdir  25836  lgsdilem2  25837  lgsdi  25838  lgsne0  25839  lgsqrlem2  25851  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgseisenlem4  25882  lgseisen  25883  lgsquadlem1  25884  lgsquadlem2  25885  lgsquadlem3  25886  2lgslem1a1  25893  chebbnd1lem1  25973  vmadivsum  25986  vmadivsumb  25987  rplogsumlem2  25989  dchrisum0lem1a  25990  rpvmasumlem  25991  dchrisumlem2  25994  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasum2lem  26000  dchrvmasum2if  26001  dchrvmasumlem2  26002  dchrvmasumlem3  26003  dchrvmasumiflem1  26005  dchrvmasumiflem2  26006  dchrisum0fno1  26015  rpvmasum2  26016  dchrisum0re  26017  dchrisum0lem1b  26019  dchrisum0lem1  26020  dchrisum0lem2a  26021  dchrisum0lem2  26022  dchrisum0lem3  26023  dchrisum0  26024  dchrmusumlem  26026  dchrvmasumlem  26027  rplogsum  26031  mudivsum  26034  mulogsumlem  26035  mulogsum  26036  mulog2sumlem1  26038  mulog2sumlem2  26039  mulog2sumlem3  26040  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  log2sumbnd  26048  selberglem1  26049  selberglem2  26050  selberglem3  26051  selberg  26052  selbergb  26053  selberg2lem  26054  selberg2  26055  selberg2b  26056  chpdifbndlem1  26057  logdivbnd  26060  selberg3lem1  26061  selberg3lem2  26062  selberg3  26063  selberg4lem1  26064  selberg4  26065  pntrsumo1  26069  pntrsumbnd  26070  pntrsumbnd2  26071  selbergr  26072  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntsf  26077  pntsval2  26080  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntrlog2bnd  26088  pntpbnd2  26091  pntlemf  26109  pntlemk  26110  pntlemo  26111  eucrct2eupth  27952  dipcl  28417  dipcn  28425  prmdvdsbc  30459  freshmansdream  30787  esumpcvgval  31237  esumpmono  31238  esumcvg  31245  esumcvgsum  31247  eulerpartlemgc  31520  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemimin  31663  ballotlemic  31664  ballotlem1c  31665  ballotlemsel1i  31670  ballotlemsf1o  31671  erdszelem4  32339  erdszelem8  32343  erdsze2lem2  32349  cvmliftlem2  32431  cvmliftlem6  32435  cvmliftlem8  32437  cvmliftlem9  32438  cvmliftlem10  32439  bcprod  32868  faclim  32876  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem9  34783  poimirlem11  34785  poimirlem13  34787  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem18  34792  poimirlem22  34796  poimirlem32  34806  mblfinlem2  34812  eldioph3b  39242  diophin  39249  diophun  39250  eldiophss  39251  irrapxlem4  39302  sumnnodd  41791  stoweidlem34  42200  wallispilem4  42234  wallispi  42236  wallispi2lem1  42237  wallispi2  42239  stirlinglem5  42244  stirlinglem7  42246  stirlinglem10  42249  stirlinglem12  42251  fourierdlem83  42355  fourierdlem112  42384  caratheodorylem2  42690  hoidmvlelem2  42759  hoidmvlelem3  42760  altgsumbcALT  44299  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator