Theorem elfznn 13530

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

Step	Hyp	Ref	Expression
1		elfzelz 13501	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13504	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12588	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5149  (class class class)co 7409  1c1 11111   ≤ cle 11249  ℕcn 12212  ℤcz 12558  ...cfz 13484

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 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-z 12559  df-uz 12823  df-fz 13485

This theorem is referenced by:  elfz1end  13531  fz1ssnn  13532  bcm1k  14275  bcpasc  14281  seqcoll  14425  pfxfv0  14642  pfxfvlsw  14645  isercolllem2  15612  isercolllem3  15613  isercoll  15614  sumeq2ii  15639  summolem3  15660  summolem2a  15661  fsum  15666  sumz  15668  fsumconst  15736  o1fsum  15759  binomlem  15775  incexc2  15784  climcndslem1  15795  climcndslem2  15796  climcnds  15797  harmonic  15805  arisum2  15807  trireciplem  15808  pwdif  15814  geo2sum  15819  geo2lim  15821  prodeq2ii  15857  prodmolem3  15877  prodmolem2a  15878  fprod  15885  prod1  15888  fprodfac  15917  fprodconst  15922  risefallfac  15968  risefacfac  15979  fallfacval4  15987  bpolydiflem  15998  rpnnen2lem10  16166  fzm1ndvds  16265  pwp1fsum  16334  lcmflefac  16585  phicl  16702  prmdivdiv  16720  pcfac  16832  pcbc  16833  prmreclem2  16850  prmreclem3  16851  prmreclem4  16852  prmreclem5  16853  prmreclem6  16854  prmrec  16855  4sqlem13  16890  vdwlem2  16915  vdwlem3  16916  vdwlem10  16923  vdwlem12  16925  prmocl  16967  prmop1  16971  fvprmselelfz  16977  fvprmselgcd1  16978  prmolefac  16979  prmodvdslcmf  16980  prmgapprmo  16995  mulgnngsum  18959  mulgnnsubcl  18966  mulgnn0z  18981  mulgnndir  18983  oddvdsnn0  19412  odnncl  19413  gexcl3  19455  efgsres  19606  mulgnn0di  19693  gsumconst  19802  srgbinomlem4  20052  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  chfacfpmmulgsum2  22367  cayhamlem1  22368  cpmadugsumlemF  22378  lebnumii  24482  ovollb2lem  25005  ovolunlem1a  25013  ovoliunlem1  25019  ovoliunlem2  25020  ovoliun2  25023  ovolscalem1  25030  ovolicc2lem4  25037  voliunlem1  25067  volsup  25073  ioombl1lem4  25078  uniioovol  25096  uniioombllem3a  25101  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  uniioombllem6  25105  dvply1  25797  aaliou3lem5  25860  aaliou3lem6  25861  dvtaylp  25882  taylthlem2  25886  pserdvlem2  25940  logfac  26109  atantayl  26442  birthdaylem2  26457  emcllem1  26500  emcllem2  26501  emcllem3  26502  emcllem5  26504  emcllem7  26506  harmoniclbnd  26513  harmonicubnd  26514  harmonicbnd4  26515  fsumharmonic  26516  lgamcvg2  26559  gamcvg2lem  26563  wilthlem1  26572  wilthlem2  26573  ftalem5  26581  basellem1  26585  basellem8  26592  chpf  26627  efchpcl  26629  chpp1  26659  chpwordi  26661  prmorcht  26682  dvdsflf1o  26691  dvdsflsumcom  26692  chtlepsi  26709  fsumvma2  26717  pclogsum  26718  vmasum  26719  logfac2  26720  chpval2  26721  chpchtsum  26722  logfaclbnd  26725  logexprlim  26728  logfacrlim2  26729  pcbcctr  26779  bposlem1  26787  bposlem2  26788  lgscllem  26807  lgsval2lem  26810  lgsval4a  26822  lgsneg  26824  lgsdir  26835  lgsdilem2  26836  lgsdi  26837  lgsne0  26838  lgsqrlem2  26850  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgseisen  26882  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  2lgslem1a1  26892  chebbnd1lem1  26972  vmadivsum  26985  vmadivsumb  26986  rplogsumlem2  26988  dchrisum0lem1a  26989  rpvmasumlem  26990  dchrisumlem2  26993  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrvmasum2if  27000  dchrvmasumlem2  27001  dchrvmasumlem3  27002  dchrvmasumiflem1  27004  dchrvmasumiflem2  27005  dchrisum0fno1  27014  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0lem3  27022  dchrisum0  27023  dchrmusumlem  27025  dchrvmasumlem  27026  rplogsum  27030  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  mulog2sumlem1  27037  mulog2sumlem2  27038  mulog2sumlem3  27039  vmalogdivsum2  27041  vmalogdivsum  27042  2vmadivsumlem  27043  log2sumbnd  27047  selberglem1  27048  selberglem2  27049  selberglem3  27050  selberg  27051  selbergb  27052  selberg2lem  27053  selberg2  27054  selberg2b  27055  chpdifbndlem1  27056  logdivbnd  27059  selberg3lem1  27060  selberg3lem2  27061  selberg3  27062  selberg4lem1  27063  selberg4  27064  pntrsumo1  27068  pntrsumbnd  27069  pntrsumbnd2  27070  selbergr  27071  selberg3r  27072  selberg4r  27073  selberg34r  27074  pntsf  27076  pntsval2  27079  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntpbnd2  27090  pntlemf  27108  pntlemk  27109  pntlemo  27110  eucrct2eupth  29498  dipcl  29965  dipcn  29973  prmdvdsbc  32022  freshmansdream  32381  esumpcvgval  33076  esumpmono  33077  esumcvg  33084  esumcvgsum  33086  eulerpartlemgc  33361  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemic  33505  ballotlem1c  33506  ballotlemsel1i  33511  ballotlemsf1o  33512  erdszelem4  34185  erdszelem8  34189  erdsze2lem2  34195  cvmliftlem2  34277  cvmliftlem6  34281  cvmliftlem8  34283  cvmliftlem9  34284  cvmliftlem10  34285  bcprod  34708  faclim  34716  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem11  36499  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem22  36510  poimirlem32  36520  mblfinlem2  36526  aks4d1p1p2  40935  aks4d1p1p4  40936  aks4d1p1  40941  aks4d1p3  40943  aks4d1p4  40944  aks4d1p5  40945  aks4d1p6  40946  aks4d1p7d1  40947  aks4d1p7  40948  aks4d1p8  40952  aks4d1p9  40953  sticksstones1  40962  sticksstones2  40963  sticksstones3  40964  sticksstones6  40967  sticksstones7  40968  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  metakunt1  40985  metakunt2  40986  metakunt6  40990  metakunt7  40991  metakunt8  40992  metakunt9  40993  metakunt11  40995  metakunt15  40999  metakunt16  41000  metakunt21  41005  metakunt22  41006  metakunt27  41011  metakunt29  41013  metakunt30  41014  oddnumth  41209  nicomachus  41210  sumcubes  41211  eldioph3b  41503  diophin  41510  diophun  41511  eldiophss  41512  irrapxlem4  41563  sumnnodd  44346  stoweidlem34  44750  wallispilem4  44784  wallispi  44786  wallispi2lem1  44787  wallispi2  44789  stirlinglem5  44794  stirlinglem7  44796  stirlinglem10  44799  stirlinglem12  44801  fourierdlem83  44905  fourierdlem112  44934  caratheodorylem2  45243  hoidmvlelem2  45312  hoidmvlelem3  45313  altgsumbcALT  47029  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306