Theorem elfznn 13680

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 13649	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13653	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12715	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7418  1c1 11194   ≤ cle 11337  ℕcn 12328  ℤcz 12686  ...cfz 13632

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-z 12687  df-uz 12959  df-fz 13633

This theorem is used by:  elfz1end  13681  fz1ssnn  13682  bcm1k  14452  bcpasc  14458  seqcoll  14602  pfxfv0  14834  pfxfvlsw  14837  isercolllem2  15826  isercolllem3  15827  isercoll  15828  sumeq2ii  15853  summolem3  15873  summolem2a  15874  fsum  15879  sumz  15881  fsumconst  15949  o1fsum  15973  binomlem  15991  incexc2  16000  climcndslem1  16011  climcndslem2  16012  climcnds  16013  harmonic  16021  arisum2  16023  trireciplem  16024  pwdif  16030  geo2sum  16035  geo2lim  16037  prodeq2ii  16073  prodmolem3  16093  prodmolem2a  16094  fprod  16101  prod1  16104  fprodfac  16133  fprodconst  16138  risefallfac  16184  risefacfac  16194  fallfacval4  16202  bpolydiflem  16213  rpnnen2lem10  16384  fzm1ndvds  16485  pwp1fsum  16554  lcmflefac  16816  prmdvdsbc  16895  phicl  16939  prmdivdiv  16957  pcfac  17070  pcbc  17071  prmreclem2  17088  prmreclem3  17089  prmreclem4  17090  prmreclem5  17091  prmreclem6  17092  prmrec  17093  4sqlem13  17128  vdwlem2  17153  vdwlem3  17154  vdwlem10  17161  vdwlem12  17163  prmocl  17205  prmop1  17209  fvprmselelfz  17215  fvprmselgcd1  17216  prmolefac  17217  prmodvdslcmf  17218  prmgapprmo  17233  mulgnngsum  19282  mulgnnsubcl  19289  mulgnn0z  19304  mulgnndir  19306  oddvdsnn0  19751  odnncl  19752  gexcl3  19794  efgsres  19945  mulgnn0di  20032  gsumconst  20141  srgbinomlem4  20448  freshmansdream  21873  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  chfacfpmmulgsum2  23176  cayhamlem1  23177  cpmadugsumlemF  23187  lebnumii  25280  ovollb2lem  25802  ovolunlem1a  25810  ovoliunlem1  25816  ovoliunlem2  25817  ovoliun2  25820  ovolscalem1  25827  ovolicc2lem4  25834  voliunlem1  25864  volsup  25870  ioombl1lem4  25875  uniioovol  25893  uniioombllem3a  25898  uniioombllem3  25899  uniioombllem4  25900  uniioombllem5  25901  uniioombllem6  25902  dvply1  26598  aaliou3lem5  26667  aaliou3lem6  26668  dvtaylp  26690  taylthlem2  26694  pserdvlem2  26748  logfac  26922  atantayl  27258  birthdaylem2  27273  emcllem1  27316  emcllem2  27317  emcllem3  27318  emcllem5  27320  emcllem7  27322  harmoniclbnd  27329  harmonicubnd  27330  harmonicbnd4  27331  fsumharmonic  27332  lgamcvg2  27375  gamcvg2lem  27379  wilthlem1  27388  wilthlem2  27389  ftalem5  27397  basellem1  27401  basellem8  27408  chpf  27443  efchpcl  27445  chpp1  27475  chpwordi  27477  prmorcht  27498  dvdsflf1o  27507  dvdsflsumcom  27508  chtlepsi  27526  fsumvma2  27534  pclogsum  27535  vmasum  27536  logfac2  27537  chpval2  27538  chpchtsum  27539  logfaclbnd  27542  logexprlim  27545  logfacrlim2  27546  pcbcctr  27596  bposlem1  27604  bposlem2  27605  lgscllem  27624  lgsval2lem  27627  lgsval4a  27639  lgsneg  27641  lgsdir  27652  lgsdilem2  27653  lgsdi  27654  lgsne0  27655  lgsqrlem2  27667  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgseisenlem4  27698  lgseisen  27699  lgsquadlem1  27700  lgsquadlem2  27701  lgsquadlem3  27702  2lgslem1a1  27709  chebbnd1lem1  27789  vmadivsum  27802  vmadivsumb  27803  rplogsumlem2  27805  dchrisum0lem1a  27806  rpvmasumlem  27807  dchrisumlem2  27810  dchrmusum2  27814  dchrvmasumlem1  27815  dchrvmasum2lem  27816  dchrvmasum2if  27817  dchrvmasumlem2  27818  dchrvmasumlem3  27819  dchrvmasumiflem1  27821  dchrvmasumiflem2  27822  dchrisum0fno1  27831  rpvmasum2  27832  dchrisum0re  27833  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2a  27837  dchrisum0lem2  27838  dchrisum0lem3  27839  dchrisum0  27840  dchrmusumlem  27842  dchrvmasumlem  27843  rplogsum  27847  mudivsum  27850  mulogsumlem  27851  mulogsum  27852  mulog2sumlem1  27854  mulog2sumlem2  27855  mulog2sumlem3  27856  vmalogdivsum2  27858  vmalogdivsum  27859  2vmadivsumlem  27860  log2sumbnd  27864  selberglem1  27865  selberglem2  27866  selberglem3  27867  selberg  27868  selbergb  27869  selberg2lem  27870  selberg2  27871  selberg2b  27872  chpdifbndlem1  27873  logdivbnd  27876  selberg3lem1  27877  selberg3lem2  27878  selberg3  27879  selberg4lem1  27880  selberg4  27881  pntrsumo1  27885  pntrsumbnd  27886  pntrsumbnd2  27887  selbergr  27888  selberg3r  27889  selberg4r  27890  selberg34r  27891  pntsf  27893  pntsval2  27896  pntrlog2bndlem1  27897  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntrlog2bnd  27904  pntpbnd2  27907  pntlemf  27925  pntlemk  27926  pntlemo  27927  eucrct2eupth  30839  dipcl  31307  dipcn  31315  gsummptp1  33611  gsummulsubdishift1  33622  esplyind  34200  esumpcvgval  34703  esumpmono  34704  esumcvg  34711  esumcvgsum  34713  eulerpartlemgc  34987  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemic  35132  ballotlem1c  35133  ballotlemsel1i  35138  ballotlemsf1o  35139  erdszelem4  35938  erdszelem8  35942  erdsze2lem2  35948  cvmliftlem2  36030  cvmliftlem6  36034  cvmliftlem8  36036  cvmliftlem9  36037  cvmliftlem10  36038  bcprod  36482  faclim  36490  poimirlem6  38524  poimirlem7  38525  poimirlem8  38526  poimirlem9  38527  poimirlem11  38529  poimirlem13  38531  poimirlem14  38532  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem22  38540  poimirlem32  38550  mblfinlem2  38556  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p1  43106  aks4d1p3  43108  aks4d1p4  43109  aks4d1p5  43110  aks4d1p6  43111  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8  43117  aks4d1p9  43118  primrootlekpowne0  43135  hashscontpow1  43151  hashscontpow  43152  sticksstones1  43176  sticksstones2  43177  sticksstones3  43178  sticksstones6  43181  sticksstones7  43182  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  oddnumth  43348  nicomachus  43349  sumcubes  43350  eldioph3b  43755  diophin  43762  diophun  43763  eldiophss  43764  irrapxlem4  43811  sumnnodd  46611  stoweidlem34  47013  wallispilem4  47047  wallispi  47049  wallispi2lem1  47050  wallispi2  47052  stirlinglem5  47057  stirlinglem7  47059  stirlinglem10  47062  stirlinglem12  47064  fourierdlem83  47168  fourierdlem112  47197  caratheodorylem2  47506  hoidmvlelem2  47575  hoidmvlelem3  47576  elfz2nn  48361  stgrusgra  49026  isubgr3stgrlem7  49039  altgsumbcALT  49434  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701