Theorem elfznn 13456

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 13427	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13430	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12501	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  (class class class)co 7349  1c1 11010   ≤ cle 11150  ℕcn 12128  ℤcz 12471  ...cfz 13410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-z 12472  df-uz 12736  df-fz 13411

This theorem is referenced by:  elfz1end  13457  fz1ssnn  13458  bcm1k  14222  bcpasc  14228  seqcoll  14371  pfxfv0  14598  pfxfvlsw  14601  isercolllem2  15573  isercolllem3  15574  isercoll  15575  sumeq2ii  15600  summolem3  15621  summolem2a  15622  fsum  15627  sumz  15629  fsumconst  15697  o1fsum  15720  binomlem  15736  incexc2  15745  climcndslem1  15756  climcndslem2  15757  climcnds  15758  harmonic  15766  arisum2  15768  trireciplem  15769  pwdif  15775  geo2sum  15780  geo2lim  15782  prodeq2ii  15818  prodmolem3  15840  prodmolem2a  15841  fprod  15848  prod1  15851  fprodfac  15880  fprodconst  15885  risefallfac  15931  risefacfac  15942  fallfacval4  15950  bpolydiflem  15961  rpnnen2lem10  16132  fzm1ndvds  16233  pwp1fsum  16302  lcmflefac  16559  prmdvdsbc  16637  phicl  16680  prmdivdiv  16698  pcfac  16811  pcbc  16812  prmreclem2  16829  prmreclem3  16830  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  prmrec  16834  4sqlem13  16869  vdwlem2  16894  vdwlem3  16895  vdwlem10  16902  vdwlem12  16904  prmocl  16946  prmop1  16950  fvprmselelfz  16956  fvprmselgcd1  16957  prmolefac  16958  prmodvdslcmf  16959  prmgapprmo  16974  mulgnngsum  18958  mulgnnsubcl  18965  mulgnn0z  18980  mulgnndir  18982  oddvdsnn0  19423  odnncl  19424  gexcl3  19466  efgsres  19617  mulgnn0di  19704  gsumconst  19813  srgbinomlem4  20114  freshmansdream  21481  chfacfscmulgsum  22745  chfacfpmmulgsum  22749  chfacfpmmulgsum2  22750  cayhamlem1  22751  cpmadugsumlemF  22761  lebnumii  24863  ovollb2lem  25387  ovolunlem1a  25395  ovoliunlem1  25401  ovoliunlem2  25402  ovoliun2  25405  ovolscalem1  25412  ovolicc2lem4  25419  voliunlem1  25449  volsup  25455  ioombl1lem4  25460  uniioovol  25478  uniioombllem3a  25483  uniioombllem3  25484  uniioombllem4  25485  uniioombllem5  25486  uniioombllem6  25487  dvply1  26189  aaliou3lem5  26253  aaliou3lem6  26254  dvtaylp  26276  taylthlem2  26280  taylthlem2OLD  26281  pserdvlem2  26336  logfac  26508  atantayl  26845  birthdaylem2  26860  emcllem1  26904  emcllem2  26905  emcllem3  26906  emcllem5  26908  emcllem7  26910  harmoniclbnd  26917  harmonicubnd  26918  harmonicbnd4  26919  fsumharmonic  26920  lgamcvg2  26963  gamcvg2lem  26967  wilthlem1  26976  wilthlem2  26977  ftalem5  26985  basellem1  26989  basellem8  26996  chpf  27031  efchpcl  27033  chpp1  27063  chpwordi  27065  prmorcht  27086  dvdsflf1o  27095  dvdsflsumcom  27096  chtlepsi  27115  fsumvma2  27123  pclogsum  27124  vmasum  27125  logfac2  27126  chpval2  27127  chpchtsum  27128  logfaclbnd  27131  logexprlim  27134  logfacrlim2  27135  pcbcctr  27185  bposlem1  27193  bposlem2  27194  lgscllem  27213  lgsval2lem  27216  lgsval4a  27228  lgsneg  27230  lgsdir  27241  lgsdilem2  27242  lgsdi  27243  lgsne0  27244  lgsqrlem2  27256  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgseisen  27288  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  2lgslem1a1  27298  chebbnd1lem1  27378  vmadivsum  27391  vmadivsumb  27392  rplogsumlem2  27394  dchrisum0lem1a  27395  rpvmasumlem  27396  dchrisumlem2  27399  dchrmusum2  27403  dchrvmasumlem1  27404  dchrvmasum2lem  27405  dchrvmasum2if  27406  dchrvmasumlem2  27407  dchrvmasumlem3  27408  dchrvmasumiflem1  27410  dchrvmasumiflem2  27411  dchrisum0fno1  27420  rpvmasum2  27421  dchrisum0re  27422  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  dchrisum0lem3  27428  dchrisum0  27429  dchrmusumlem  27431  dchrvmasumlem  27432  rplogsum  27436  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  mulog2sumlem1  27443  mulog2sumlem2  27444  mulog2sumlem3  27445  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  log2sumbnd  27453  selberglem1  27454  selberglem2  27455  selberglem3  27456  selberg  27457  selbergb  27458  selberg2lem  27459  selberg2  27460  selberg2b  27461  chpdifbndlem1  27462  logdivbnd  27465  selberg3lem1  27466  selberg3lem2  27467  selberg3  27468  selberg4lem1  27469  selberg4  27470  pntrsumo1  27474  pntrsumbnd  27475  pntrsumbnd2  27476  selbergr  27477  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntsf  27482  pntsval2  27485  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd2  27496  pntlemf  27514  pntlemk  27515  pntlemo  27516  eucrct2eupth  30189  dipcl  30656  dipcn  30664  esumpcvgval  34045  esumpmono  34046  esumcvg  34053  esumcvgsum  34055  eulerpartlemgc  34330  ballotlemfc0  34461  ballotlemfcc  34462  ballotlemic  34475  ballotlem1c  34476  ballotlemsel1i  34481  ballotlemsf1o  34482  erdszelem4  35167  erdszelem8  35171  erdsze2lem2  35177  cvmliftlem2  35259  cvmliftlem6  35263  cvmliftlem8  35265  cvmliftlem9  35266  cvmliftlem10  35267  bcprod  35711  faclim  35719  poimirlem6  37606  poimirlem7  37607  poimirlem8  37608  poimirlem9  37609  poimirlem11  37611  poimirlem13  37613  poimirlem14  37614  poimirlem15  37615  poimirlem16  37616  poimirlem17  37617  poimirlem18  37618  poimirlem22  37622  poimirlem32  37632  mblfinlem2  37638  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1  42049  aks4d1p3  42051  aks4d1p4  42052  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7d1  42055  aks4d1p7  42056  aks4d1p8  42060  aks4d1p9  42061  primrootlekpowne0  42078  hashscontpow1  42094  hashscontpow  42095  sticksstones1  42119  sticksstones2  42120  sticksstones3  42121  sticksstones6  42124  sticksstones7  42125  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  oddnumth  42284  nicomachus  42285  sumcubes  42286  eldioph3b  42738  diophin  42745  diophun  42746  eldiophss  42747  irrapxlem4  42798  sumnnodd  45611  stoweidlem34  46015  wallispilem4  46049  wallispi  46051  wallispi2lem1  46052  wallispi2  46054  stirlinglem5  46059  stirlinglem7  46061  stirlinglem10  46064  stirlinglem12  46066  fourierdlem83  46170  fourierdlem112  46199  caratheodorylem2  46508  hoidmvlelem2  46577  hoidmvlelem3  46578  stgrusgra  47943  isubgr3stgrlem7  47956  altgsumbcALT  48337  nn0sumshdiglemA  48604  nn0sumshdiglemB  48605