Theorem elfznn 13106

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 13077	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13080	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12168	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 586	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2112   class class class wbr 5039  (class class class)co 7191  1c1 10695   ≤ cle 10833  ℕcn 11795  ℤcz 12141  ...cfz 13060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-cnex 10750  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770  ax-pre-mulgt0 10771

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-1st 7739  df-2nd 7740  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838  df-sub 11029  df-neg 11030  df-nn 11796  df-z 12142  df-uz 12404  df-fz 13061

This theorem is referenced by:  elfz1end  13107  fz1ssnn  13108  bcm1k  13846  bcpasc  13852  seqcoll  13995  pfxfv0  14222  pfxfvlsw  14225  isercolllem2  15194  isercolllem3  15195  isercoll  15196  sumeq2ii  15222  summolem3  15243  summolem2a  15244  fsum  15249  sumz  15251  fsumconst  15317  o1fsum  15340  binomlem  15356  incexc2  15365  climcndslem1  15376  climcndslem2  15377  climcnds  15378  harmonic  15386  arisum2  15388  trireciplem  15389  pwdif  15395  geo2sum  15400  geo2lim  15402  prodeq2ii  15438  prodmolem3  15458  prodmolem2a  15459  fprod  15466  prod1  15469  fprodfac  15498  fprodconst  15503  risefallfac  15549  risefacfac  15560  fallfacval4  15568  bpolydiflem  15579  rpnnen2lem10  15747  fzm1ndvds  15846  pwp1fsum  15915  lcmflefac  16168  phicl  16285  prmdivdiv  16303  pcfac  16415  pcbc  16416  prmreclem2  16433  prmreclem3  16434  prmreclem4  16435  prmreclem5  16436  prmreclem6  16437  prmrec  16438  4sqlem13  16473  vdwlem2  16498  vdwlem3  16499  vdwlem10  16506  vdwlem12  16508  prmocl  16550  prmop1  16554  fvprmselelfz  16560  fvprmselgcd1  16561  prmolefac  16562  prmodvdslcmf  16563  prmgapprmo  16578  mulgnngsum  18451  mulgnnsubcl  18458  mulgnn0z  18472  mulgnndir  18474  oddvdsnn0  18890  odnncl  18891  gexcl3  18930  efgsres  19082  mulgnn0di  19165  gsumconst  19273  srgbinomlem4  19512  chfacfscmulgsum  21711  chfacfpmmulgsum  21715  chfacfpmmulgsum2  21716  cayhamlem1  21717  cpmadugsumlemF  21727  lebnumii  23817  ovollb2lem  24339  ovolunlem1a  24347  ovoliunlem1  24353  ovoliunlem2  24354  ovoliun2  24357  ovolscalem1  24364  ovolicc2lem4  24371  voliunlem1  24401  volsup  24407  ioombl1lem4  24412  uniioovol  24430  uniioombllem3a  24435  uniioombllem3  24436  uniioombllem4  24437  uniioombllem5  24438  uniioombllem6  24439  dvply1  25131  aaliou3lem5  25194  aaliou3lem6  25195  dvtaylp  25216  taylthlem2  25220  pserdvlem2  25274  logfac  25443  atantayl  25774  birthdaylem2  25789  emcllem1  25832  emcllem2  25833  emcllem3  25834  emcllem5  25836  emcllem7  25838  harmoniclbnd  25845  harmonicubnd  25846  harmonicbnd4  25847  fsumharmonic  25848  lgamcvg2  25891  gamcvg2lem  25895  wilthlem1  25904  wilthlem2  25905  ftalem5  25913  basellem1  25917  basellem8  25924  chpf  25959  efchpcl  25961  chpp1  25991  chpwordi  25993  prmorcht  26014  dvdsflf1o  26023  dvdsflsumcom  26024  chtlepsi  26041  fsumvma2  26049  pclogsum  26050  vmasum  26051  logfac2  26052  chpval2  26053  chpchtsum  26054  logfaclbnd  26057  logexprlim  26060  logfacrlim2  26061  pcbcctr  26111  bposlem1  26119  bposlem2  26120  lgscllem  26139  lgsval2lem  26142  lgsval4a  26154  lgsneg  26156  lgsdir  26167  lgsdilem2  26168  lgsdi  26169  lgsne0  26170  lgsqrlem2  26182  lgseisenlem1  26210  lgseisenlem2  26211  lgseisenlem3  26212  lgseisenlem4  26213  lgseisen  26214  lgsquadlem1  26215  lgsquadlem2  26216  lgsquadlem3  26217  2lgslem1a1  26224  chebbnd1lem1  26304  vmadivsum  26317  vmadivsumb  26318  rplogsumlem2  26320  dchrisum0lem1a  26321  rpvmasumlem  26322  dchrisumlem2  26325  dchrmusum2  26329  dchrvmasumlem1  26330  dchrvmasum2lem  26331  dchrvmasum2if  26332  dchrvmasumlem2  26333  dchrvmasumlem3  26334  dchrvmasumiflem1  26336  dchrvmasumiflem2  26337  dchrisum0fno1  26346  rpvmasum2  26347  dchrisum0re  26348  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2a  26352  dchrisum0lem2  26353  dchrisum0lem3  26354  dchrisum0  26355  dchrmusumlem  26357  dchrvmasumlem  26358  rplogsum  26362  mudivsum  26365  mulogsumlem  26366  mulogsum  26367  mulog2sumlem1  26369  mulog2sumlem2  26370  mulog2sumlem3  26371  vmalogdivsum2  26373  vmalogdivsum  26374  2vmadivsumlem  26375  log2sumbnd  26379  selberglem1  26380  selberglem2  26381  selberglem3  26382  selberg  26383  selbergb  26384  selberg2lem  26385  selberg2  26386  selberg2b  26387  chpdifbndlem1  26388  logdivbnd  26391  selberg3lem1  26392  selberg3lem2  26393  selberg3  26394  selberg4lem1  26395  selberg4  26396  pntrsumo1  26400  pntrsumbnd  26401  pntrsumbnd2  26402  selbergr  26403  selberg3r  26404  selberg4r  26405  selberg34r  26406  pntsf  26408  pntsval2  26411  pntrlog2bndlem1  26412  pntrlog2bndlem2  26413  pntrlog2bndlem3  26414  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  pntrlog2bndlem6  26418  pntrlog2bnd  26419  pntpbnd2  26422  pntlemf  26440  pntlemk  26441  pntlemo  26442  eucrct2eupth  28282  dipcl  28747  dipcn  28755  prmdvdsbc  30804  freshmansdream  31157  esumpcvgval  31712  esumpmono  31713  esumcvg  31720  esumcvgsum  31722  eulerpartlemgc  31995  ballotlemfc0  32125  ballotlemfcc  32126  ballotlemic  32139  ballotlem1c  32140  ballotlemsel1i  32145  ballotlemsf1o  32146  erdszelem4  32823  erdszelem8  32827  erdsze2lem2  32833  cvmliftlem2  32915  cvmliftlem6  32919  cvmliftlem8  32921  cvmliftlem9  32922  cvmliftlem10  32923  bcprod  33373  faclim  33381  poimirlem6  35469  poimirlem7  35470  poimirlem8  35471  poimirlem9  35472  poimirlem11  35474  poimirlem13  35476  poimirlem14  35477  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem18  35481  poimirlem22  35485  poimirlem32  35495  mblfinlem2  35501  aks4d1p1p2  39760  aks4d1p1p4  39761  aks4d1p1  39766  sticksstones1  39771  sticksstones2  39772  sticksstones3  39773  sticksstones6  39776  sticksstones7  39777  sticksstones10  39780  sticksstones12a  39782  sticksstones12  39783  metakunt1  39788  metakunt2  39789  metakunt6  39793  metakunt7  39794  metakunt8  39795  metakunt9  39796  metakunt11  39798  metakunt15  39802  metakunt16  39803  metakunt21  39808  metakunt22  39809  metakunt27  39814  metakunt29  39816  metakunt30  39817  eldioph3b  40231  diophin  40238  diophun  40239  eldiophss  40240  irrapxlem4  40291  sumnnodd  42789  stoweidlem34  43193  wallispilem4  43227  wallispi  43229  wallispi2lem1  43230  wallispi2  43232  stirlinglem5  43237  stirlinglem7  43239  stirlinglem10  43242  stirlinglem12  43244  fourierdlem83  43348  fourierdlem112  43377  caratheodorylem2  43683  hoidmvlelem2  43752  hoidmvlelem3  43753  altgsumbcALT  45305  nn0sumshdiglemA  45581  nn0sumshdiglemB  45582