Theorem elfznn 13568

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  (class class class)co 7403  1c1 11128   ≤ cle 11268  ℕcn 12238  ℤcz 12586  ...cfz 13522

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-z 12587  df-uz 12851  df-fz 13523

This theorem is referenced by:  elfz1end  13569  fz1ssnn  13570  bcm1k  14331  bcpasc  14337  seqcoll  14480  pfxfv0  14708  pfxfvlsw  14711  isercolllem2  15680  isercolllem3  15681  isercoll  15682  sumeq2ii  15707  summolem3  15728  summolem2a  15729  fsum  15734  sumz  15736  fsumconst  15804  o1fsum  15827  binomlem  15843  incexc2  15852  climcndslem1  15863  climcndslem2  15864  climcnds  15865  harmonic  15873  arisum2  15875  trireciplem  15876  pwdif  15882  geo2sum  15887  geo2lim  15889  prodeq2ii  15925  prodmolem3  15947  prodmolem2a  15948  fprod  15955  prod1  15958  fprodfac  15987  fprodconst  15992  risefallfac  16038  risefacfac  16049  fallfacval4  16057  bpolydiflem  16068  rpnnen2lem10  16239  fzm1ndvds  16339  pwp1fsum  16408  lcmflefac  16665  prmdvdsbc  16743  phicl  16786  prmdivdiv  16804  pcfac  16917  pcbc  16918  prmreclem2  16935  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  prmreclem6  16939  prmrec  16940  4sqlem13  16975  vdwlem2  17000  vdwlem3  17001  vdwlem10  17008  vdwlem12  17010  prmocl  17052  prmop1  17056  fvprmselelfz  17062  fvprmselgcd1  17063  prmolefac  17064  prmodvdslcmf  17065  prmgapprmo  17080  mulgnngsum  19060  mulgnnsubcl  19067  mulgnn0z  19082  mulgnndir  19084  oddvdsnn0  19523  odnncl  19524  gexcl3  19566  efgsres  19717  mulgnn0di  19804  gsumconst  19913  srgbinomlem4  20187  freshmansdream  21533  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmadugsumlemF  22812  lebnumii  24914  ovollb2lem  25439  ovolunlem1a  25447  ovoliunlem1  25453  ovoliunlem2  25454  ovoliun2  25457  ovolscalem1  25464  ovolicc2lem4  25471  voliunlem1  25501  volsup  25507  ioombl1lem4  25512  uniioovol  25530  uniioombllem3a  25535  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  uniioombllem6  25539  dvply1  26241  aaliou3lem5  26305  aaliou3lem6  26306  dvtaylp  26328  taylthlem2  26332  taylthlem2OLD  26333  pserdvlem2  26388  logfac  26560  atantayl  26897  birthdaylem2  26912  emcllem1  26956  emcllem2  26957  emcllem3  26958  emcllem5  26960  emcllem7  26962  harmoniclbnd  26969  harmonicubnd  26970  harmonicbnd4  26971  fsumharmonic  26972  lgamcvg2  27015  gamcvg2lem  27019  wilthlem1  27028  wilthlem2  27029  ftalem5  27037  basellem1  27041  basellem8  27048  chpf  27083  efchpcl  27085  chpp1  27115  chpwordi  27117  prmorcht  27138  dvdsflf1o  27147  dvdsflsumcom  27148  chtlepsi  27167  fsumvma2  27175  pclogsum  27176  vmasum  27177  logfac2  27178  chpval2  27179  chpchtsum  27180  logfaclbnd  27183  logexprlim  27186  logfacrlim2  27187  pcbcctr  27237  bposlem1  27245  bposlem2  27246  lgscllem  27265  lgsval2lem  27268  lgsval4a  27280  lgsneg  27282  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  lgsqrlem2  27308  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  2lgslem1a1  27350  chebbnd1lem1  27430  vmadivsum  27443  vmadivsumb  27444  rplogsumlem2  27446  dchrisum0lem1a  27447  rpvmasumlem  27448  dchrisumlem2  27451  dchrmusum2  27455  dchrvmasumlem1  27456  dchrvmasum2lem  27457  dchrvmasum2if  27458  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  dchrisum0fno1  27472  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  dchrisum0  27481  dchrmusumlem  27483  dchrvmasumlem  27484  rplogsum  27488  mudivsum  27491  mulogsumlem  27492  mulogsum  27493  mulog2sumlem1  27495  mulog2sumlem2  27496  mulog2sumlem3  27497  vmalogdivsum2  27499  vmalogdivsum  27500  2vmadivsumlem  27501  log2sumbnd  27505  selberglem1  27506  selberglem2  27507  selberglem3  27508  selberg  27509  selbergb  27510  selberg2lem  27511  selberg2  27512  selberg2b  27513  chpdifbndlem1  27514  logdivbnd  27517  selberg3lem1  27518  selberg3lem2  27519  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrsumo1  27526  pntrsumbnd  27527  pntrsumbnd2  27528  selbergr  27529  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntsf  27534  pntsval2  27537  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd2  27548  pntlemf  27566  pntlemk  27567  pntlemo  27568  eucrct2eupth  30172  dipcl  30639  dipcn  30647  esumpcvgval  34055  esumpmono  34056  esumcvg  34063  esumcvgsum  34065  eulerpartlemgc  34340  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemic  34485  ballotlem1c  34486  ballotlemsel1i  34491  ballotlemsf1o  34492  erdszelem4  35162  erdszelem8  35166  erdsze2lem2  35172  cvmliftlem2  35254  cvmliftlem6  35258  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem10  35262  bcprod  35701  faclim  35709  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem9  37599  poimirlem11  37601  poimirlem13  37603  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem22  37612  poimirlem32  37622  mblfinlem2  37628  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1  42035  aks4d1p3  42037  aks4d1p4  42038  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  aks4d1p9  42047  primrootlekpowne0  42064  hashscontpow1  42080  hashscontpow  42081  sticksstones1  42105  sticksstones2  42106  sticksstones3  42107  sticksstones6  42110  sticksstones7  42111  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  metakunt1  42164  metakunt2  42165  metakunt6  42169  metakunt7  42170  metakunt8  42171  metakunt9  42172  metakunt11  42174  metakunt15  42178  metakunt16  42179  metakunt21  42184  metakunt22  42185  metakunt27  42190  metakunt29  42192  metakunt30  42193  oddnumth  42307  nicomachus  42308  sumcubes  42309  eldioph3b  42735  diophin  42742  diophun  42743  eldiophss  42744  irrapxlem4  42795  sumnnodd  45607  stoweidlem34  46011  wallispilem4  46045  wallispi  46047  wallispi2lem1  46048  wallispi2  46050  stirlinglem5  46055  stirlinglem7  46057  stirlinglem10  46060  stirlinglem12  46062  fourierdlem83  46166  fourierdlem112  46195  caratheodorylem2  46504  hoidmvlelem2  46573  hoidmvlelem3  46574  stgrusgra  47919  isubgr3stgrlem7  47932  altgsumbcALT  48276  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548