Theorem elfznn 13577

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 13547	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13550	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12615	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 594	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  (class class class)co 7410  1c1 11096   ≤ cle 11239  ℕcn 12228  ℤcz 12586  ...cfz 13530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-z 12587  df-uz 12858  df-fz 13531

This theorem is referenced by:  elfz1end  13578  fz1ssnn  13579  bcm1k  14347  bcpasc  14353  seqcoll  14497  pfxfv0  14725  pfxfvlsw  14728  isercolllem2  15713  isercolllem3  15714  isercoll  15715  sumeq2ii  15740  summolem3  15761  summolem2a  15762  fsum  15767  sumz  15769  fsumconst  15837  o1fsum  15861  binomlem  15879  incexc2  15888  climcndslem1  15899  climcndslem2  15900  climcnds  15901  harmonic  15909  arisum2  15911  trireciplem  15912  pwdif  15918  geo2sum  15923  geo2lim  15925  prodeq2ii  15961  prodmolem3  15983  prodmolem2a  15984  fprod  15991  prod1  15994  fprodfac  16023  fprodconst  16028  risefallfac  16074  risefacfac  16084  fallfacval4  16092  bpolydiflem  16103  rpnnen2lem10  16274  fzm1ndvds  16375  pwp1fsum  16444  lcmflefac  16701  prmdvdsbc  16780  phicl  16823  prmdivdiv  16841  pcfac  16954  pcbc  16955  prmreclem2  16972  prmreclem3  16973  prmreclem4  16974  prmreclem5  16975  prmreclem6  16976  prmrec  16977  4sqlem13  17012  vdwlem2  17037  vdwlem3  17038  vdwlem10  17045  vdwlem12  17047  prmocl  17089  prmop1  17093  fvprmselelfz  17099  fvprmselgcd1  17100  prmolefac  17101  prmodvdslcmf  17102  prmgapprmo  17117  mulgnngsum  19140  mulgnnsubcl  19147  mulgnn0z  19162  mulgnndir  19164  oddvdsnn0  19609  odnncl  19610  gexcl3  19652  efgsres  19803  mulgnn0di  19890  gsumconst  19999  srgbinomlem4  20306  freshmansdream  21724  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  chfacfpmmulgsum2  23022  cayhamlem1  23023  cpmadugsumlemF  23033  lebnumii  25125  ovollb2lem  25647  ovolunlem1a  25655  ovoliunlem1  25661  ovoliunlem2  25662  ovoliun2  25665  ovolscalem1  25672  ovolicc2lem4  25679  voliunlem1  25709  volsup  25715  ioombl1lem4  25720  uniioovol  25738  uniioombllem3a  25743  uniioombllem3  25744  uniioombllem4  25745  uniioombllem5  25746  uniioombllem6  25747  dvply1  26445  aaliou3lem5  26510  aaliou3lem6  26511  dvtaylp  26533  taylthlem2  26537  pserdvlem2  26591  logfac  26766  atantayl  27102  birthdaylem2  27117  emcllem1  27160  emcllem2  27161  emcllem3  27162  emcllem5  27164  emcllem7  27166  harmoniclbnd  27173  harmonicubnd  27174  harmonicbnd4  27175  fsumharmonic  27176  lgamcvg2  27219  gamcvg2lem  27223  wilthlem1  27232  wilthlem2  27233  ftalem5  27241  basellem1  27245  basellem8  27252  chpf  27287  efchpcl  27289  chpp1  27319  chpwordi  27321  prmorcht  27342  dvdsflf1o  27351  dvdsflsumcom  27352  chtlepsi  27370  fsumvma2  27378  pclogsum  27379  vmasum  27380  logfac2  27381  chpval2  27382  chpchtsum  27383  logfaclbnd  27386  logexprlim  27389  logfacrlim2  27390  pcbcctr  27440  bposlem1  27448  bposlem2  27449  lgscllem  27468  lgsval2lem  27471  lgsval4a  27483  lgsneg  27485  lgsdir  27496  lgsdilem2  27497  lgsdi  27498  lgsne0  27499  lgsqrlem2  27511  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisenlem4  27542  lgseisen  27543  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  2lgslem1a1  27553  chebbnd1lem1  27633  vmadivsum  27646  vmadivsumb  27647  rplogsumlem2  27649  dchrisum0lem1a  27650  rpvmasumlem  27651  dchrisumlem2  27654  dchrmusum2  27658  dchrvmasumlem1  27659  dchrvmasum2lem  27660  dchrvmasum2if  27661  dchrvmasumlem2  27662  dchrvmasumlem3  27663  dchrvmasumiflem1  27665  dchrvmasumiflem2  27666  dchrisum0fno1  27675  rpvmasum2  27676  dchrisum0re  27677  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  dchrisum0lem3  27683  dchrisum0  27684  dchrmusumlem  27686  dchrvmasumlem  27687  rplogsum  27691  mudivsum  27694  mulogsumlem  27695  mulogsum  27696  mulog2sumlem1  27698  mulog2sumlem2  27699  mulog2sumlem3  27700  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  log2sumbnd  27708  selberglem1  27709  selberglem2  27710  selberglem3  27711  selberg  27712  selbergb  27713  selberg2lem  27714  selberg2  27715  selberg2b  27716  chpdifbndlem1  27717  logdivbnd  27720  selberg3lem1  27721  selberg3lem2  27722  selberg3  27723  selberg4lem1  27724  selberg4  27725  pntrsumo1  27729  pntrsumbnd  27730  pntrsumbnd2  27731  selbergr  27732  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntsf  27737  pntsval2  27740  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd2  27751  pntlemf  27769  pntlemk  27770  pntlemo  27771  eucrct2eupth  30596  dipcl  31064  dipcn  31072  gsummptp1  33377  gsummulsubdishift1  33388  esplyind  33965  esumpcvgval  34468  esumpmono  34469  esumcvg  34476  esumcvgsum  34478  eulerpartlemgc  34752  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemic  34897  ballotlem1c  34898  ballotlemsel1i  34903  ballotlemsf1o  34904  erdszelem4  35686  erdszelem8  35690  erdsze2lem2  35696  cvmliftlem2  35778  cvmliftlem6  35782  cvmliftlem8  35784  cvmliftlem9  35785  cvmliftlem10  35786  bcprod  36230  faclim  36238  poimirlem6  38277  poimirlem7  38278  poimirlem8  38279  poimirlem9  38280  poimirlem11  38282  poimirlem13  38284  poimirlem14  38285  poimirlem15  38286  poimirlem16  38287  poimirlem17  38288  poimirlem18  38289  poimirlem22  38293  poimirlem32  38303  mblfinlem2  38309  aks4d1p1p2  42837  aks4d1p1p4  42838  aks4d1p1  42843  aks4d1p3  42845  aks4d1p4  42846  aks4d1p5  42847  aks4d1p6  42848  aks4d1p7d1  42849  aks4d1p7  42850  aks4d1p8  42854  aks4d1p9  42855  primrootlekpowne0  42872  hashscontpow1  42888  hashscontpow  42889  sticksstones1  42913  sticksstones2  42914  sticksstones3  42915  sticksstones6  42918  sticksstones7  42919  sticksstones10  42922  sticksstones12a  42924  sticksstones12  42925  oddnumth  43072  nicomachus  43073  sumcubes  43074  eldioph3b  43496  diophin  43503  diophun  43504  eldiophss  43505  irrapxlem4  43552  sumnnodd  46346  stoweidlem34  46748  wallispilem4  46782  wallispi  46784  wallispi2lem1  46785  wallispi2  46787  stirlinglem5  46792  stirlinglem7  46794  stirlinglem10  46797  stirlinglem12  46799  fourierdlem83  46903  fourierdlem112  46932  caratheodorylem2  47241  hoidmvlelem2  47310  hoidmvlelem3  47311  elfz2nn  48059  stgrusgra  48724  isubgr3stgrlem7  48737  altgsumbcALT  49133  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400