Theorem elfznn 13584

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 13555	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13558	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12640	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 581	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2099   class class class wbr 5153  (class class class)co 7424  1c1 11159   ≤ cle 11299  ℕcn 12264  ℤcz 12610  ...cfz 13538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-nn 12265  df-z 12611  df-uz 12875  df-fz 13539

This theorem is referenced by:  elfz1end  13585  fz1ssnn  13586  bcm1k  14332  bcpasc  14338  seqcoll  14483  pfxfv0  14700  pfxfvlsw  14703  isercolllem2  15670  isercolllem3  15671  isercoll  15672  sumeq2ii  15697  summolem3  15718  summolem2a  15719  fsum  15724  sumz  15726  fsumconst  15794  o1fsum  15817  binomlem  15833  incexc2  15842  climcndslem1  15853  climcndslem2  15854  climcnds  15855  harmonic  15863  arisum2  15865  trireciplem  15866  pwdif  15872  geo2sum  15877  geo2lim  15879  prodeq2ii  15915  prodmolem3  15935  prodmolem2a  15936  fprod  15943  prod1  15946  fprodfac  15975  fprodconst  15980  risefallfac  16026  risefacfac  16037  fallfacval4  16045  bpolydiflem  16056  rpnnen2lem10  16225  fzm1ndvds  16324  pwp1fsum  16393  lcmflefac  16649  prmdvdsbc  16728  phicl  16771  prmdivdiv  16789  pcfac  16901  pcbc  16902  prmreclem2  16919  prmreclem3  16920  prmreclem4  16921  prmreclem5  16922  prmreclem6  16923  prmrec  16924  4sqlem13  16959  vdwlem2  16984  vdwlem3  16985  vdwlem10  16992  vdwlem12  16994  prmocl  17036  prmop1  17040  fvprmselelfz  17046  fvprmselgcd1  17047  prmolefac  17048  prmodvdslcmf  17049  prmgapprmo  17064  mulgnngsum  19073  mulgnnsubcl  19080  mulgnn0z  19095  mulgnndir  19097  oddvdsnn0  19542  odnncl  19543  gexcl3  19585  efgsres  19736  mulgnn0di  19823  gsumconst  19932  srgbinomlem4  20212  freshmansdream  21572  chfacfscmulgsum  22853  chfacfpmmulgsum  22857  chfacfpmmulgsum2  22858  cayhamlem1  22859  cpmadugsumlemF  22869  lebnumii  24983  ovollb2lem  25508  ovolunlem1a  25516  ovoliunlem1  25522  ovoliunlem2  25523  ovoliun2  25526  ovolscalem1  25533  ovolicc2lem4  25540  voliunlem1  25570  volsup  25576  ioombl1lem4  25581  uniioovol  25599  uniioombllem3a  25604  uniioombllem3  25605  uniioombllem4  25606  uniioombllem5  25607  uniioombllem6  25608  dvply1  26311  aaliou3lem5  26375  aaliou3lem6  26376  dvtaylp  26398  taylthlem2  26402  taylthlem2OLD  26403  pserdvlem2  26458  logfac  26628  atantayl  26965  birthdaylem2  26980  emcllem1  27024  emcllem2  27025  emcllem3  27026  emcllem5  27028  emcllem7  27030  harmoniclbnd  27037  harmonicubnd  27038  harmonicbnd4  27039  fsumharmonic  27040  lgamcvg2  27083  gamcvg2lem  27087  wilthlem1  27096  wilthlem2  27097  ftalem5  27105  basellem1  27109  basellem8  27116  chpf  27151  efchpcl  27153  chpp1  27183  chpwordi  27185  prmorcht  27206  dvdsflf1o  27215  dvdsflsumcom  27216  chtlepsi  27235  fsumvma2  27243  pclogsum  27244  vmasum  27245  logfac2  27246  chpval2  27247  chpchtsum  27248  logfaclbnd  27251  logexprlim  27254  logfacrlim2  27255  pcbcctr  27305  bposlem1  27313  bposlem2  27314  lgscllem  27333  lgsval2lem  27336  lgsval4a  27348  lgsneg  27350  lgsdir  27361  lgsdilem2  27362  lgsdi  27363  lgsne0  27364  lgsqrlem2  27376  lgseisenlem1  27404  lgseisenlem2  27405  lgseisenlem3  27406  lgseisenlem4  27407  lgseisen  27408  lgsquadlem1  27409  lgsquadlem2  27410  lgsquadlem3  27411  2lgslem1a1  27418  chebbnd1lem1  27498  vmadivsum  27511  vmadivsumb  27512  rplogsumlem2  27514  dchrisum0lem1a  27515  rpvmasumlem  27516  dchrisumlem2  27519  dchrmusum2  27523  dchrvmasumlem1  27524  dchrvmasum2lem  27525  dchrvmasum2if  27526  dchrvmasumlem2  27527  dchrvmasumlem3  27528  dchrvmasumiflem1  27530  dchrvmasumiflem2  27531  dchrisum0fno1  27540  rpvmasum2  27541  dchrisum0re  27542  dchrisum0lem1b  27544  dchrisum0lem1  27545  dchrisum0lem2a  27546  dchrisum0lem2  27547  dchrisum0lem3  27548  dchrisum0  27549  dchrmusumlem  27551  dchrvmasumlem  27552  rplogsum  27556  mudivsum  27559  mulogsumlem  27560  mulogsum  27561  mulog2sumlem1  27563  mulog2sumlem2  27564  mulog2sumlem3  27565  vmalogdivsum2  27567  vmalogdivsum  27568  2vmadivsumlem  27569  log2sumbnd  27573  selberglem1  27574  selberglem2  27575  selberglem3  27576  selberg  27577  selbergb  27578  selberg2lem  27579  selberg2  27580  selberg2b  27581  chpdifbndlem1  27582  logdivbnd  27585  selberg3lem1  27586  selberg3lem2  27587  selberg3  27588  selberg4lem1  27589  selberg4  27590  pntrsumo1  27594  pntrsumbnd  27595  pntrsumbnd2  27596  selbergr  27597  selberg3r  27598  selberg4r  27599  selberg34r  27600  pntsf  27602  pntsval2  27605  pntrlog2bndlem1  27606  pntrlog2bndlem2  27607  pntrlog2bndlem3  27608  pntrlog2bndlem4  27609  pntrlog2bndlem5  27610  pntrlog2bndlem6  27612  pntrlog2bnd  27613  pntpbnd2  27616  pntlemf  27634  pntlemk  27635  pntlemo  27636  eucrct2eupth  30178  dipcl  30645  dipcn  30653  esumpcvgval  33911  esumpmono  33912  esumcvg  33919  esumcvgsum  33921  eulerpartlemgc  34196  ballotlemfc0  34326  ballotlemfcc  34327  ballotlemic  34340  ballotlem1c  34341  ballotlemsel1i  34346  ballotlemsf1o  34347  erdszelem4  35022  erdszelem8  35026  erdsze2lem2  35032  cvmliftlem2  35114  cvmliftlem6  35118  cvmliftlem8  35120  cvmliftlem9  35121  cvmliftlem10  35122  bcprod  35560  faclim  35568  poimirlem6  37327  poimirlem7  37328  poimirlem8  37329  poimirlem9  37330  poimirlem11  37332  poimirlem13  37334  poimirlem14  37335  poimirlem15  37336  poimirlem16  37337  poimirlem17  37338  poimirlem18  37339  poimirlem22  37343  poimirlem32  37353  mblfinlem2  37359  aks4d1p1p2  41769  aks4d1p1p4  41770  aks4d1p1  41775  aks4d1p3  41777  aks4d1p4  41778  aks4d1p5  41779  aks4d1p6  41780  aks4d1p7d1  41781  aks4d1p7  41782  aks4d1p8  41786  aks4d1p9  41787  primrootlekpowne0  41803  hashscontpow1  41819  hashscontpow  41820  sticksstones1  41844  sticksstones2  41845  sticksstones3  41846  sticksstones6  41849  sticksstones7  41850  sticksstones10  41853  sticksstones12a  41855  sticksstones12  41856  metakunt1  41891  metakunt2  41892  metakunt6  41896  metakunt7  41897  metakunt8  41898  metakunt9  41899  metakunt11  41901  metakunt15  41905  metakunt16  41906  metakunt21  41911  metakunt22  41912  metakunt27  41917  metakunt29  41919  metakunt30  41920  oddnumth  42110  nicomachus  42111  sumcubes  42112  eldioph3b  42422  diophin  42429  diophun  42430  eldiophss  42431  irrapxlem4  42482  sumnnodd  45251  stoweidlem34  45655  wallispilem4  45689  wallispi  45691  wallispi2lem1  45692  wallispi2  45694  stirlinglem5  45699  stirlinglem7  45701  stirlinglem10  45704  stirlinglem12  45706  fourierdlem83  45810  fourierdlem112  45839  caratheodorylem2  46148  hoidmvlelem2  46217  hoidmvlelem3  46218  altgsumbcALT  47732  nn0sumshdiglemA  48007  nn0sumshdiglemB  48008