Theorem elfznn 13514

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  (class class class)co 7387  1c1 11069   ≤ cle 11209  ℕcn 12186  ℤcz 12529  ...cfz 13468

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-z 12530  df-uz 12794  df-fz 13469

This theorem is referenced by:  elfz1end  13515  fz1ssnn  13516  bcm1k  14280  bcpasc  14286  seqcoll  14429  pfxfv0  14657  pfxfvlsw  14660  isercolllem2  15632  isercolllem3  15633  isercoll  15634  sumeq2ii  15659  summolem3  15680  summolem2a  15681  fsum  15686  sumz  15688  fsumconst  15756  o1fsum  15779  binomlem  15795  incexc2  15804  climcndslem1  15815  climcndslem2  15816  climcnds  15817  harmonic  15825  arisum2  15827  trireciplem  15828  pwdif  15834  geo2sum  15839  geo2lim  15841  prodeq2ii  15877  prodmolem3  15899  prodmolem2a  15900  fprod  15907  prod1  15910  fprodfac  15939  fprodconst  15944  risefallfac  15990  risefacfac  16001  fallfacval4  16009  bpolydiflem  16020  rpnnen2lem10  16191  fzm1ndvds  16292  pwp1fsum  16361  lcmflefac  16618  prmdvdsbc  16696  phicl  16739  prmdivdiv  16757  pcfac  16870  pcbc  16871  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  prmrec  16893  4sqlem13  16928  vdwlem2  16953  vdwlem3  16954  vdwlem10  16961  vdwlem12  16963  prmocl  17005  prmop1  17009  fvprmselelfz  17015  fvprmselgcd1  17016  prmolefac  17017  prmodvdslcmf  17018  prmgapprmo  17033  mulgnngsum  19011  mulgnnsubcl  19018  mulgnn0z  19033  mulgnndir  19035  oddvdsnn0  19474  odnncl  19475  gexcl3  19517  efgsres  19668  mulgnn0di  19755  gsumconst  19864  srgbinomlem4  20138  freshmansdream  21484  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmadugsumlemF  22763  lebnumii  24865  ovollb2lem  25389  ovolunlem1a  25397  ovoliunlem1  25403  ovoliunlem2  25404  ovoliun2  25407  ovolscalem1  25414  ovolicc2lem4  25421  voliunlem1  25451  volsup  25457  ioombl1lem4  25462  uniioovol  25480  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombllem6  25489  dvply1  26191  aaliou3lem5  26255  aaliou3lem6  26256  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  logfac  26510  atantayl  26847  birthdaylem2  26862  emcllem1  26906  emcllem2  26907  emcllem3  26908  emcllem5  26910  emcllem7  26912  harmoniclbnd  26919  harmonicubnd  26920  harmonicbnd4  26921  fsumharmonic  26922  lgamcvg2  26965  gamcvg2lem  26969  wilthlem1  26978  wilthlem2  26979  ftalem5  26987  basellem1  26991  basellem8  26998  chpf  27033  efchpcl  27035  chpp1  27065  chpwordi  27067  prmorcht  27088  dvdsflf1o  27097  dvdsflsumcom  27098  chtlepsi  27117  fsumvma2  27125  pclogsum  27126  vmasum  27127  logfac2  27128  chpval2  27129  chpchtsum  27130  logfaclbnd  27133  logexprlim  27136  logfacrlim2  27137  pcbcctr  27187  bposlem1  27195  bposlem2  27196  lgscllem  27215  lgsval2lem  27218  lgsval4a  27230  lgsneg  27232  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  lgsqrlem2  27258  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  2lgslem1a1  27300  chebbnd1lem1  27380  vmadivsum  27393  vmadivsumb  27394  rplogsumlem2  27396  dchrisum0lem1a  27397  rpvmasumlem  27398  dchrisumlem2  27401  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasum2if  27408  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  dchrvmasumiflem2  27413  dchrisum0fno1  27422  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  dchrisum0  27431  dchrmusumlem  27433  dchrvmasumlem  27434  rplogsum  27438  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  mulog2sumlem1  27445  mulog2sumlem2  27446  mulog2sumlem3  27447  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  log2sumbnd  27455  selberglem1  27456  selberglem2  27457  selberglem3  27458  selberg  27459  selbergb  27460  selberg2lem  27461  selberg2  27462  selberg2b  27463  chpdifbndlem1  27464  logdivbnd  27467  selberg3lem1  27468  selberg3lem2  27469  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrsumo1  27476  pntrsumbnd  27477  pntrsumbnd2  27478  selbergr  27479  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntsf  27484  pntsval2  27487  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd2  27498  pntlemf  27516  pntlemk  27517  pntlemo  27518  eucrct2eupth  30174  dipcl  30641  dipcn  30649  esumpcvgval  34068  esumpmono  34069  esumcvg  34076  esumcvgsum  34078  eulerpartlemgc  34353  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemic  34498  ballotlem1c  34499  ballotlemsel1i  34504  ballotlemsf1o  34505  erdszelem4  35181  erdszelem8  35185  erdsze2lem2  35191  cvmliftlem2  35273  cvmliftlem6  35277  cvmliftlem8  35279  cvmliftlem9  35280  cvmliftlem10  35281  bcprod  35725  faclim  35733  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem11  37625  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem22  37636  poimirlem32  37646  mblfinlem2  37652  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1  42064  aks4d1p3  42066  aks4d1p4  42067  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  primrootlekpowne0  42093  hashscontpow1  42109  hashscontpow  42110  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  oddnumth  42299  nicomachus  42300  sumcubes  42301  eldioph3b  42753  diophin  42760  diophun  42761  eldiophss  42762  irrapxlem4  42813  sumnnodd  45628  stoweidlem34  46032  wallispilem4  46066  wallispi  46068  wallispi2lem1  46069  wallispi2  46071  stirlinglem5  46076  stirlinglem7  46078  stirlinglem10  46081  stirlinglem12  46083  fourierdlem83  46187  fourierdlem112  46216  caratheodorylem2  46525  hoidmvlelem2  46594  hoidmvlelem3  46595  stgrusgra  47958  isubgr3stgrlem7  47971  altgsumbcALT  48341  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609