Theorem elfznn 12589

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 12561	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 12563	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 11665	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 574	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2158   class class class wbr 4840  (class class class)co 6871  1c1 10219   ≤ cle 10357  ℕcn 11302  ℤcz 11639  ...cfz 12545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-cnex 10274  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-1st 7395  df-2nd 7396  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-er 7976  df-en 8190  df-dom 8191  df-sdom 8192  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-nn 11303  df-z 11640  df-uz 11901  df-fz 12546

This theorem is referenced by:  elfz1end  12590  fz1ssnn  12591  fzossnn  12737  bcm1k  13318  bcpasc  13324  seqcoll  13461  swrd0fv0  13660  swrd0fvlsw  13663  isercolllem2  14615  isercolllem3  14616  isercoll  14617  sumeq2ii  14642  summolem3  14664  summolem2a  14665  fsum  14670  sumz  14672  fsumconst  14740  o1fsum  14763  binomlem  14779  incexc2  14788  climcndslem1  14799  climcndslem2  14800  climcnds  14801  harmonic  14809  arisum2  14811  trireciplem  14812  geo2sum  14822  geo2lim  14824  prodeq2ii  14860  prodmolem3  14880  prodmolem2a  14881  fprod  14888  prod1  14891  fprodfac  14920  fprodconst  14925  risefallfac  14971  risefacfac  14982  fallfacval4  14990  bpolydiflem  15001  rpnnen2lem10  15168  fzm1ndvds  15263  pwp1fsum  15330  lcmflefac  15576  phicl  15687  prmdivdiv  15705  pcfac  15816  pcbc  15817  prmreclem2  15834  prmreclem3  15835  prmreclem4  15836  prmreclem5  15837  prmreclem6  15838  prmrec  15839  4sqlem13  15874  vdwlem2  15899  vdwlem3  15900  vdwlem10  15907  vdwlem12  15909  prmocl  15951  prmop1  15955  fvprmselelfz  15961  fvprmselgcd1  15962  prmolefac  15963  prmodvdslcmf  15964  prmgapprmo  15979  mulgnnsubcl  17754  mulgnn0z  17767  mulgnndir  17769  oddvdsnn0  18160  odnncl  18161  gexcl3  18199  efgsres  18348  mulgnn0di  18428  gsumconst  18531  srgbinomlem4  18741  chfacfscmulgsum  20874  chfacfpmmulgsum  20878  chfacfpmmulgsum2  20879  cayhamlem1  20880  cpmadugsumlemF  20890  1stcfb  21458  1stckgenlem  21566  lebnumii  22974  ovollb2lem  23465  ovolunlem1a  23473  ovoliunlem1  23479  ovoliunlem2  23480  ovoliun2  23483  ovolscalem1  23490  ovolicc2lem4  23497  voliunlem1  23527  volsup  23533  ioombl1lem4  23538  uniioovol  23556  uniioombllem3a  23561  uniioombllem3  23562  uniioombllem4  23563  uniioombllem5  23564  uniioombllem6  23565  dvply1  24249  aaliou3lem5  24312  aaliou3lem6  24313  dvtaylp  24334  taylthlem2  24338  pserdvlem2  24392  logfac  24557  atantayl  24874  birthdaylem2  24889  emcllem1  24932  emcllem2  24933  emcllem3  24934  emcllem5  24936  emcllem7  24938  harmoniclbnd  24945  harmonicubnd  24946  harmonicbnd4  24947  fsumharmonic  24948  lgamcvg2  24991  gamcvg2lem  24995  wilthlem1  25004  wilthlem2  25005  ftalem5  25013  basellem1  25017  basellem8  25024  chpf  25059  efchpcl  25061  chpp1  25091  chpwordi  25093  prmorcht  25114  dvdsflf1o  25123  dvdsflsumcom  25124  chtlepsi  25141  fsumvma2  25149  pclogsum  25150  vmasum  25151  logfac2  25152  chpval2  25153  chpchtsum  25154  logfaclbnd  25157  logexprlim  25160  logfacrlim2  25161  pcbcctr  25211  bposlem1  25219  bposlem2  25220  lgscllem  25239  lgsval2lem  25242  lgsval4a  25254  lgsneg  25256  lgsdir  25267  lgsdilem2  25268  lgsdi  25269  lgsne0  25270  lgsqrlem2  25282  lgseisenlem1  25310  lgseisenlem2  25311  lgseisenlem3  25312  lgseisenlem4  25313  lgseisen  25314  lgsquadlem1  25315  lgsquadlem2  25316  lgsquadlem3  25317  2lgslem1a1  25324  chebbnd1lem1  25368  vmadivsum  25381  vmadivsumb  25382  rplogsumlem2  25384  dchrisum0lem1a  25385  rpvmasumlem  25386  dchrisumlem2  25389  dchrmusum2  25393  dchrvmasumlem1  25394  dchrvmasum2lem  25395  dchrvmasum2if  25396  dchrvmasumlem2  25397  dchrvmasumlem3  25398  dchrvmasumiflem1  25400  dchrvmasumiflem2  25401  dchrisum0fno1  25410  rpvmasum2  25411  dchrisum0re  25412  dchrisum0lem1b  25414  dchrisum0lem1  25415  dchrisum0lem2a  25416  dchrisum0lem2  25417  dchrisum0lem3  25418  dchrisum0  25419  dchrmusumlem  25421  dchrvmasumlem  25422  rplogsum  25426  mudivsum  25429  mulogsumlem  25430  mulogsum  25431  mulog2sumlem1  25433  mulog2sumlem2  25434  mulog2sumlem3  25435  vmalogdivsum2  25437  vmalogdivsum  25438  2vmadivsumlem  25439  log2sumbnd  25443  selberglem1  25444  selberglem2  25445  selberglem3  25446  selberg  25447  selbergb  25448  selberg2lem  25449  selberg2  25450  selberg2b  25451  chpdifbndlem1  25452  logdivbnd  25455  selberg3lem1  25456  selberg3lem2  25457  selberg3  25458  selberg4lem1  25459  selberg4  25460  pntrsumo1  25464  pntrsumbnd  25465  pntrsumbnd2  25466  selbergr  25467  selberg3r  25468  selberg4r  25469  selberg34r  25470  pntsf  25472  pntsval2  25475  pntrlog2bndlem1  25476  pntrlog2bndlem2  25477  pntrlog2bndlem3  25478  pntrlog2bndlem4  25479  pntrlog2bndlem5  25480  pntrlog2bndlem6  25482  pntrlog2bnd  25483  pntpbnd2  25486  pntlemf  25504  pntlemk  25505  pntlemo  25506  eucrct2eupth  27414  dipcl  27892  dipcn  27900  esumpcvgval  30462  esumpmono  30463  esumcvg  30470  esumcvgsum  30472  eulerpartlemgc  30746  ballotlemfc0  30876  ballotlemfcc  30877  ballotlemimin  30889  ballotlemic  30890  ballotlem1c  30891  ballotlemsel1i  30896  ballotlemsf1o  30897  erdszelem4  31496  erdszelem8  31500  erdsze2lem2  31506  cvmliftlem2  31588  cvmliftlem6  31592  cvmliftlem8  31594  cvmliftlem9  31595  cvmliftlem10  31596  bcprod  31943  faclim  31951  poimirlem6  33725  poimirlem7  33726  poimirlem8  33727  poimirlem9  33728  poimirlem11  33730  poimirlem13  33732  poimirlem14  33733  poimirlem15  33734  poimirlem16  33735  poimirlem17  33736  poimirlem18  33737  poimirlem22  33741  poimirlem32  33751  mblfinlem2  33757  eldioph3b  37827  diophin  37835  diophun  37836  eldiophss  37837  irrapxlem4  37888  sumnnodd  40339  stoweidlem34  40727  wallispilem4  40761  wallispi  40763  wallispi2lem1  40764  wallispi2  40766  stirlinglem5  40771  stirlinglem7  40773  stirlinglem10  40776  stirlinglem12  40778  fourierdlem83  40882  fourierdlem112  40911  caratheodorylem2  41220  hoidmvlelem2  41289  hoidmvlelem3  41290  pfxfv0  41972  pfxfvlsw  41975  pwdif  42073  altgsumbcALT  42696  nn0sumshdiglemA  42978  nn0sumshdiglemB  42979