Theorem elfznn 13481

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 13452	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13455	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12529	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  (class class class)co 7368  1c1 11039   ≤ cle 11179  ℕcn 12157  ℤcz 12500  ...cfz 13435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-z 12501  df-uz 12764  df-fz 13436

This theorem is referenced by:  elfz1end  13482  fz1ssnn  13483  bcm1k  14250  bcpasc  14256  seqcoll  14399  pfxfv0  14627  pfxfvlsw  14630  isercolllem2  15601  isercolllem3  15602  isercoll  15603  sumeq2ii  15628  summolem3  15649  summolem2a  15650  fsum  15655  sumz  15657  fsumconst  15725  o1fsum  15748  binomlem  15764  incexc2  15773  climcndslem1  15784  climcndslem2  15785  climcnds  15786  harmonic  15794  arisum2  15796  trireciplem  15797  pwdif  15803  geo2sum  15808  geo2lim  15810  prodeq2ii  15846  prodmolem3  15868  prodmolem2a  15869  fprod  15876  prod1  15879  fprodfac  15908  fprodconst  15913  risefallfac  15959  risefacfac  15970  fallfacval4  15978  bpolydiflem  15989  rpnnen2lem10  16160  fzm1ndvds  16261  pwp1fsum  16330  lcmflefac  16587  prmdvdsbc  16665  phicl  16708  prmdivdiv  16726  pcfac  16839  pcbc  16840  prmreclem2  16857  prmreclem3  16858  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  prmrec  16862  4sqlem13  16897  vdwlem2  16922  vdwlem3  16923  vdwlem10  16930  vdwlem12  16932  prmocl  16974  prmop1  16978  fvprmselelfz  16984  fvprmselgcd1  16985  prmolefac  16986  prmodvdslcmf  16987  prmgapprmo  17002  mulgnngsum  19021  mulgnnsubcl  19028  mulgnn0z  19043  mulgnndir  19045  oddvdsnn0  19485  odnncl  19486  gexcl3  19528  efgsres  19679  mulgnn0di  19766  gsumconst  19875  srgbinomlem4  20176  freshmansdream  21541  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmadugsumlemF  22832  lebnumii  24933  ovollb2lem  25457  ovolunlem1a  25465  ovoliunlem1  25471  ovoliunlem2  25472  ovoliun2  25475  ovolscalem1  25482  ovolicc2lem4  25489  voliunlem1  25519  volsup  25525  ioombl1lem4  25530  uniioovol  25548  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombllem6  25557  dvply1  26259  aaliou3lem5  26323  aaliou3lem6  26324  dvtaylp  26346  taylthlem2  26350  taylthlem2OLD  26351  pserdvlem2  26406  logfac  26578  atantayl  26915  birthdaylem2  26930  emcllem1  26974  emcllem2  26975  emcllem3  26976  emcllem5  26978  emcllem7  26980  harmoniclbnd  26987  harmonicubnd  26988  harmonicbnd4  26989  fsumharmonic  26990  lgamcvg2  27033  gamcvg2lem  27037  wilthlem1  27046  wilthlem2  27047  ftalem5  27055  basellem1  27059  basellem8  27066  chpf  27101  efchpcl  27103  chpp1  27133  chpwordi  27135  prmorcht  27156  dvdsflf1o  27165  dvdsflsumcom  27166  chtlepsi  27185  fsumvma2  27193  pclogsum  27194  vmasum  27195  logfac2  27196  chpval2  27197  chpchtsum  27198  logfaclbnd  27201  logexprlim  27204  logfacrlim2  27205  pcbcctr  27255  bposlem1  27263  bposlem2  27264  lgscllem  27283  lgsval2lem  27286  lgsval4a  27298  lgsneg  27300  lgsdir  27311  lgsdilem2  27312  lgsdi  27313  lgsne0  27314  lgsqrlem2  27326  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgseisen  27358  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  2lgslem1a1  27368  chebbnd1lem1  27448  vmadivsum  27461  vmadivsumb  27462  rplogsumlem2  27464  dchrisum0lem1a  27465  rpvmasumlem  27466  dchrisumlem2  27469  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasum2if  27476  dchrvmasumlem2  27477  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  dchrvmasumiflem2  27481  dchrisum0fno1  27490  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  dchrisum0  27499  dchrmusumlem  27501  dchrvmasumlem  27502  rplogsum  27506  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  mulog2sumlem1  27513  mulog2sumlem2  27514  mulog2sumlem3  27515  vmalogdivsum2  27517  vmalogdivsum  27518  2vmadivsumlem  27519  log2sumbnd  27523  selberglem1  27524  selberglem2  27525  selberglem3  27526  selberg  27527  selbergb  27528  selberg2lem  27529  selberg2  27530  selberg2b  27531  chpdifbndlem1  27532  logdivbnd  27535  selberg3lem1  27536  selberg3lem2  27537  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrsumo1  27544  pntrsumbnd  27545  pntrsumbnd2  27546  selbergr  27547  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntsf  27552  pntsval2  27555  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd2  27566  pntlemf  27584  pntlemk  27585  pntlemo  27586  eucrct2eupth  30332  dipcl  30800  dipcn  30808  gsummptp1  33151  gsummulsubdishift1  33162  esplyind  33752  esumpcvgval  34256  esumpmono  34257  esumcvg  34264  esumcvgsum  34266  eulerpartlemgc  34540  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemic  34685  ballotlem1c  34686  ballotlemsel1i  34691  ballotlemsf1o  34692  erdszelem4  35410  erdszelem8  35414  erdsze2lem2  35420  cvmliftlem2  35502  cvmliftlem6  35506  cvmliftlem8  35508  cvmliftlem9  35509  cvmliftlem10  35510  bcprod  35954  faclim  35962  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem9  37880  poimirlem11  37882  poimirlem13  37884  poimirlem14  37885  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem18  37889  poimirlem22  37893  poimirlem32  37903  mblfinlem2  37909  aks4d1p1p2  42440  aks4d1p1p4  42441  aks4d1p1  42446  aks4d1p3  42448  aks4d1p4  42449  aks4d1p5  42450  aks4d1p6  42451  aks4d1p7d1  42452  aks4d1p7  42453  aks4d1p8  42457  aks4d1p9  42458  primrootlekpowne0  42475  hashscontpow1  42491  hashscontpow  42492  sticksstones1  42516  sticksstones2  42517  sticksstones3  42518  sticksstones6  42521  sticksstones7  42522  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  oddnumth  42681  nicomachus  42682  sumcubes  42683  eldioph3b  43122  diophin  43129  diophun  43130  eldiophss  43131  irrapxlem4  43182  sumnnodd  45990  stoweidlem34  46392  wallispilem4  46426  wallispi  46428  wallispi2lem1  46429  wallispi2  46431  stirlinglem5  46436  stirlinglem7  46438  stirlinglem10  46441  stirlinglem12  46443  fourierdlem83  46547  fourierdlem112  46576  caratheodorylem2  46885  hoidmvlelem2  46954  hoidmvlelem3  46955  stgrusgra  48319  isubgr3stgrlem7  48332  altgsumbcALT  48713  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980