Theorem elfznn 13558

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 13529	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13532	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12597	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 592	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  (class class class)co 7396  1c1 11074   ≤ cle 11217  ℕcn 12210  ℤcz 12568  ...cfz 13512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-z 12569  df-uz 12840  df-fz 13513

This theorem is referenced by:  elfz1end  13559  fz1ssnn  13560  bcm1k  14328  bcpasc  14334  seqcoll  14477  pfxfv0  14705  pfxfvlsw  14708  isercolllem2  15693  isercolllem3  15694  isercoll  15695  sumeq2ii  15720  summolem3  15741  summolem2a  15742  fsum  15747  sumz  15749  fsumconst  15817  o1fsum  15841  binomlem  15859  incexc2  15868  climcndslem1  15879  climcndslem2  15880  climcnds  15881  harmonic  15889  arisum2  15891  trireciplem  15892  pwdif  15898  geo2sum  15903  geo2lim  15905  prodeq2ii  15941  prodmolem3  15963  prodmolem2a  15964  fprod  15971  prod1  15974  fprodfac  16003  fprodconst  16008  risefallfac  16054  risefacfac  16065  fallfacval4  16073  bpolydiflem  16084  rpnnen2lem10  16255  fzm1ndvds  16356  pwp1fsum  16425  lcmflefac  16682  prmdvdsbc  16761  phicl  16804  prmdivdiv  16822  pcfac  16935  pcbc  16936  prmreclem2  16953  prmreclem3  16954  prmreclem4  16955  prmreclem5  16956  prmreclem6  16957  prmrec  16958  4sqlem13  16993  vdwlem2  17018  vdwlem3  17019  vdwlem10  17026  vdwlem12  17028  prmocl  17070  prmop1  17074  fvprmselelfz  17080  fvprmselgcd1  17081  prmolefac  17082  prmodvdslcmf  17083  prmgapprmo  17098  mulgnngsum  19121  mulgnnsubcl  19128  mulgnn0z  19143  mulgnndir  19145  oddvdsnn0  19584  odnncl  19585  gexcl3  19627  efgsres  19778  mulgnn0di  19865  gsumconst  19974  srgbinomlem4  20275  freshmansdream  21623  chfacfscmulgsum  22917  chfacfpmmulgsum  22921  chfacfpmmulgsum2  22922  cayhamlem1  22923  cpmadugsumlemF  22933  lebnumii  25025  ovollb2lem  25547  ovolunlem1a  25555  ovoliunlem1  25561  ovoliunlem2  25562  ovoliun2  25565  ovolscalem1  25572  ovolicc2lem4  25579  voliunlem1  25609  volsup  25615  ioombl1lem4  25620  uniioovol  25638  uniioombllem3a  25643  uniioombllem3  25644  uniioombllem4  25645  uniioombllem5  25646  uniioombllem6  25647  dvply1  26345  aaliou3lem5  26408  aaliou3lem6  26409  dvtaylp  26430  taylthlem2  26434  pserdvlem2  26488  logfac  26663  atantayl  26999  birthdaylem2  27014  emcllem1  27057  emcllem2  27058  emcllem3  27059  emcllem5  27061  emcllem7  27063  harmoniclbnd  27070  harmonicubnd  27071  harmonicbnd4  27072  fsumharmonic  27073  lgamcvg2  27116  gamcvg2lem  27120  wilthlem1  27129  wilthlem2  27130  ftalem5  27138  basellem1  27142  basellem8  27149  chpf  27184  efchpcl  27186  chpp1  27216  chpwordi  27218  prmorcht  27239  dvdsflf1o  27248  dvdsflsumcom  27249  chtlepsi  27267  fsumvma2  27275  pclogsum  27276  vmasum  27277  logfac2  27278  chpval2  27279  chpchtsum  27280  logfaclbnd  27283  logexprlim  27286  logfacrlim2  27287  pcbcctr  27337  bposlem1  27345  bposlem2  27346  lgscllem  27365  lgsval2lem  27368  lgsval4a  27380  lgsneg  27382  lgsdir  27393  lgsdilem2  27394  lgsdi  27395  lgsne0  27396  lgsqrlem2  27408  lgseisenlem1  27436  lgseisenlem2  27437  lgseisenlem3  27438  lgseisenlem4  27439  lgseisen  27440  lgsquadlem1  27441  lgsquadlem2  27442  lgsquadlem3  27443  2lgslem1a1  27450  chebbnd1lem1  27530  vmadivsum  27543  vmadivsumb  27544  rplogsumlem2  27546  dchrisum0lem1a  27547  rpvmasumlem  27548  dchrisumlem2  27551  dchrmusum2  27555  dchrvmasumlem1  27556  dchrvmasum2lem  27557  dchrvmasum2if  27558  dchrvmasumlem2  27559  dchrvmasumlem3  27560  dchrvmasumiflem1  27562  dchrvmasumiflem2  27563  dchrisum0fno1  27572  rpvmasum2  27573  dchrisum0re  27574  dchrisum0lem1b  27576  dchrisum0lem1  27577  dchrisum0lem2a  27578  dchrisum0lem2  27579  dchrisum0lem3  27580  dchrisum0  27581  dchrmusumlem  27583  dchrvmasumlem  27584  rplogsum  27588  mudivsum  27591  mulogsumlem  27592  mulogsum  27593  mulog2sumlem1  27595  mulog2sumlem2  27596  mulog2sumlem3  27597  vmalogdivsum2  27599  vmalogdivsum  27600  2vmadivsumlem  27601  log2sumbnd  27605  selberglem1  27606  selberglem2  27607  selberglem3  27608  selberg  27609  selbergb  27610  selberg2lem  27611  selberg2  27612  selberg2b  27613  chpdifbndlem1  27614  logdivbnd  27617  selberg3lem1  27618  selberg3lem2  27619  selberg3  27620  selberg4lem1  27621  selberg4  27622  pntrsumo1  27626  pntrsumbnd  27627  pntrsumbnd2  27628  selbergr  27629  selberg3r  27630  selberg4r  27631  selberg34r  27632  pntsf  27634  pntsval2  27637  pntrlog2bndlem1  27638  pntrlog2bndlem2  27639  pntrlog2bndlem3  27640  pntrlog2bndlem4  27641  pntrlog2bndlem5  27642  pntrlog2bndlem6  27644  pntrlog2bnd  27645  pntpbnd2  27648  pntlemf  27666  pntlemk  27667  pntlemo  27668  eucrct2eupth  30444  dipcl  30912  dipcn  30920  gsummptp1  33234  gsummulsubdishift1  33245  esplyind  33869  esumpcvgval  34372  esumpmono  34373  esumcvg  34380  esumcvgsum  34382  eulerpartlemgc  34656  ballotlemfc0  34787  ballotlemfcc  34788  ballotlemic  34801  ballotlem1c  34802  ballotlemsel1i  34807  ballotlemsf1o  34808  erdszelem4  35541  erdszelem8  35545  erdsze2lem2  35551  cvmliftlem2  35633  cvmliftlem6  35637  cvmliftlem8  35639  cvmliftlem9  35640  cvmliftlem10  35641  bcprod  36085  faclim  36093  poimirlem6  38122  poimirlem7  38123  poimirlem8  38124  poimirlem9  38125  poimirlem11  38127  poimirlem13  38129  poimirlem14  38130  poimirlem15  38131  poimirlem16  38132  poimirlem17  38133  poimirlem18  38134  poimirlem22  38138  poimirlem32  38148  mblfinlem2  38154  aks4d1p1p2  42684  aks4d1p1p4  42685  aks4d1p1  42690  aks4d1p3  42692  aks4d1p4  42693  aks4d1p5  42694  aks4d1p6  42695  aks4d1p7d1  42696  aks4d1p7  42697  aks4d1p8  42701  aks4d1p9  42702  primrootlekpowne0  42719  hashscontpow1  42735  hashscontpow  42736  sticksstones1  42760  sticksstones2  42761  sticksstones3  42762  sticksstones6  42765  sticksstones7  42766  sticksstones10  42769  sticksstones12a  42771  sticksstones12  42772  oddnumth  42917  nicomachus  42918  sumcubes  42919  eldioph3b  43343  diophin  43350  diophun  43351  eldiophss  43352  irrapxlem4  43399  sumnnodd  46203  stoweidlem34  46605  wallispilem4  46639  wallispi  46641  wallispi2lem1  46642  wallispi2  46644  stirlinglem5  46649  stirlinglem7  46651  stirlinglem10  46654  stirlinglem12  46656  fourierdlem83  46760  fourierdlem112  46789  caratheodorylem2  47098  hoidmvlelem2  47167  hoidmvlelem3  47168  elfz2nn  47913  stgrusgra  48578  isubgr3stgrlem7  48591  altgsumbcALT  48972  nn0sumshdiglemA  49238  nn0sumshdiglemB  49239