Theorem elfznn 13214

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 13185	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13188	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12276	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 582	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  (class class class)co 7255  1c1 10803   ≤ cle 10941  ℕcn 11903  ℤcz 12249  ...cfz 13168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-z 12250  df-uz 12512  df-fz 13169

This theorem is referenced by:  elfz1end  13215  fz1ssnn  13216  bcm1k  13957  bcpasc  13963  seqcoll  14106  pfxfv0  14333  pfxfvlsw  14336  isercolllem2  15305  isercolllem3  15306  isercoll  15307  sumeq2ii  15333  summolem3  15354  summolem2a  15355  fsum  15360  sumz  15362  fsumconst  15430  o1fsum  15453  binomlem  15469  incexc2  15478  climcndslem1  15489  climcndslem2  15490  climcnds  15491  harmonic  15499  arisum2  15501  trireciplem  15502  pwdif  15508  geo2sum  15513  geo2lim  15515  prodeq2ii  15551  prodmolem3  15571  prodmolem2a  15572  fprod  15579  prod1  15582  fprodfac  15611  fprodconst  15616  risefallfac  15662  risefacfac  15673  fallfacval4  15681  bpolydiflem  15692  rpnnen2lem10  15860  fzm1ndvds  15959  pwp1fsum  16028  lcmflefac  16281  phicl  16398  prmdivdiv  16416  pcfac  16528  pcbc  16529  prmreclem2  16546  prmreclem3  16547  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  prmrec  16551  4sqlem13  16586  vdwlem2  16611  vdwlem3  16612  vdwlem10  16619  vdwlem12  16621  prmocl  16663  prmop1  16667  fvprmselelfz  16673  fvprmselgcd1  16674  prmolefac  16675  prmodvdslcmf  16676  prmgapprmo  16691  mulgnngsum  18624  mulgnnsubcl  18631  mulgnn0z  18645  mulgnndir  18647  oddvdsnn0  19067  odnncl  19068  gexcl3  19107  efgsres  19259  mulgnn0di  19342  gsumconst  19450  srgbinomlem4  19694  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadugsumlemF  21933  lebnumii  24035  ovollb2lem  24557  ovolunlem1a  24565  ovoliunlem1  24571  ovoliunlem2  24572  ovoliun2  24575  ovolscalem1  24582  ovolicc2lem4  24589  voliunlem1  24619  volsup  24625  ioombl1lem4  24630  uniioovol  24648  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  uniioombllem6  24657  dvply1  25349  aaliou3lem5  25412  aaliou3lem6  25413  dvtaylp  25434  taylthlem2  25438  pserdvlem2  25492  logfac  25661  atantayl  25992  birthdaylem2  26007  emcllem1  26050  emcllem2  26051  emcllem3  26052  emcllem5  26054  emcllem7  26056  harmoniclbnd  26063  harmonicubnd  26064  harmonicbnd4  26065  fsumharmonic  26066  lgamcvg2  26109  gamcvg2lem  26113  wilthlem1  26122  wilthlem2  26123  ftalem5  26131  basellem1  26135  basellem8  26142  chpf  26177  efchpcl  26179  chpp1  26209  chpwordi  26211  prmorcht  26232  dvdsflf1o  26241  dvdsflsumcom  26242  chtlepsi  26259  fsumvma2  26267  pclogsum  26268  vmasum  26269  logfac2  26270  chpval2  26271  chpchtsum  26272  logfaclbnd  26275  logexprlim  26278  logfacrlim2  26279  pcbcctr  26329  bposlem1  26337  bposlem2  26338  lgscllem  26357  lgsval2lem  26360  lgsval4a  26372  lgsneg  26374  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  lgsqrlem2  26400  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  2lgslem1a1  26442  chebbnd1lem1  26522  vmadivsum  26535  vmadivsumb  26536  rplogsumlem2  26538  dchrisum0lem1a  26539  rpvmasumlem  26540  dchrisumlem2  26543  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrvmasum2if  26550  dchrvmasumlem2  26551  dchrvmasumlem3  26552  dchrvmasumiflem1  26554  dchrvmasumiflem2  26555  dchrisum0fno1  26564  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrisum0  26573  dchrmusumlem  26575  dchrvmasumlem  26576  rplogsum  26580  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  mulog2sumlem1  26587  mulog2sumlem2  26588  mulog2sumlem3  26589  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  log2sumbnd  26597  selberglem1  26598  selberglem2  26599  selberglem3  26600  selberg  26601  selbergb  26602  selberg2lem  26603  selberg2  26604  selberg2b  26605  chpdifbndlem1  26606  logdivbnd  26609  selberg3lem1  26610  selberg3lem2  26611  selberg3  26612  selberg4lem1  26613  selberg4  26614  pntrsumo1  26618  pntrsumbnd  26619  pntrsumbnd2  26620  selbergr  26621  selberg3r  26622  selberg4r  26623  selberg34r  26624  pntsf  26626  pntsval2  26629  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd2  26640  pntlemf  26658  pntlemk  26659  pntlemo  26660  eucrct2eupth  28510  dipcl  28975  dipcn  28983  prmdvdsbc  31032  freshmansdream  31386  esumpcvgval  31946  esumpmono  31947  esumcvg  31954  esumcvgsum  31956  eulerpartlemgc  32229  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemic  32373  ballotlem1c  32374  ballotlemsel1i  32379  ballotlemsf1o  32380  erdszelem4  33056  erdszelem8  33060  erdsze2lem2  33066  cvmliftlem2  33148  cvmliftlem6  33152  cvmliftlem8  33154  cvmliftlem9  33155  cvmliftlem10  33156  bcprod  33610  faclim  33618  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem11  35715  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem22  35726  poimirlem32  35736  mblfinlem2  35742  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1  40012  aks4d1p3  40014  aks4d1p4  40015  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones6  40035  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  metakunt1  40053  metakunt2  40054  metakunt6  40058  metakunt7  40059  metakunt8  40060  metakunt9  40061  metakunt11  40063  metakunt15  40067  metakunt16  40068  metakunt21  40073  metakunt22  40074  metakunt27  40079  metakunt29  40081  metakunt30  40082  eldioph3b  40503  diophin  40510  diophun  40511  eldiophss  40512  irrapxlem4  40563  sumnnodd  43061  stoweidlem34  43465  wallispilem4  43499  wallispi  43501  wallispi2lem1  43502  wallispi2  43504  stirlinglem5  43509  stirlinglem7  43511  stirlinglem10  43514  stirlinglem12  43516  fourierdlem83  43620  fourierdlem112  43649  caratheodorylem2  43955  hoidmvlelem2  44024  hoidmvlelem3  44025  altgsumbcALT  45577  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854