Theorem elfznn 13526

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5147  (class class class)co 7405  1c1 11107   ≤ cle 11245  ℕcn 12208  ℤcz 12554  ...cfz 13480

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-z 12555  df-uz 12819  df-fz 13481

This theorem is referenced by:  elfz1end  13527  fz1ssnn  13528  bcm1k  14271  bcpasc  14277  seqcoll  14421  pfxfv0  14638  pfxfvlsw  14641  isercolllem2  15608  isercolllem3  15609  isercoll  15610  sumeq2ii  15635  summolem3  15656  summolem2a  15657  fsum  15662  sumz  15664  fsumconst  15732  o1fsum  15755  binomlem  15771  incexc2  15780  climcndslem1  15791  climcndslem2  15792  climcnds  15793  harmonic  15801  arisum2  15803  trireciplem  15804  pwdif  15810  geo2sum  15815  geo2lim  15817  prodeq2ii  15853  prodmolem3  15873  prodmolem2a  15874  fprod  15881  prod1  15884  fprodfac  15913  fprodconst  15918  risefallfac  15964  risefacfac  15975  fallfacval4  15983  bpolydiflem  15994  rpnnen2lem10  16162  fzm1ndvds  16261  pwp1fsum  16330  lcmflefac  16581  phicl  16698  prmdivdiv  16716  pcfac  16828  pcbc  16829  prmreclem2  16846  prmreclem3  16847  prmreclem4  16848  prmreclem5  16849  prmreclem6  16850  prmrec  16851  4sqlem13  16886  vdwlem2  16911  vdwlem3  16912  vdwlem10  16919  vdwlem12  16921  prmocl  16963  prmop1  16967  fvprmselelfz  16973  fvprmselgcd1  16974  prmolefac  16975  prmodvdslcmf  16976  prmgapprmo  16991  mulgnngsum  18953  mulgnnsubcl  18960  mulgnn0z  18975  mulgnndir  18977  oddvdsnn0  19406  odnncl  19407  gexcl3  19449  efgsres  19600  mulgnn0di  19687  gsumconst  19796  srgbinomlem4  20045  chfacfscmulgsum  22353  chfacfpmmulgsum  22357  chfacfpmmulgsum2  22358  cayhamlem1  22359  cpmadugsumlemF  22369  lebnumii  24473  ovollb2lem  24996  ovolunlem1a  25004  ovoliunlem1  25010  ovoliunlem2  25011  ovoliun2  25014  ovolscalem1  25021  ovolicc2lem4  25028  voliunlem1  25058  volsup  25064  ioombl1lem4  25069  uniioovol  25087  uniioombllem3a  25092  uniioombllem3  25093  uniioombllem4  25094  uniioombllem5  25095  uniioombllem6  25096  dvply1  25788  aaliou3lem5  25851  aaliou3lem6  25852  dvtaylp  25873  taylthlem2  25877  pserdvlem2  25931  logfac  26100  atantayl  26431  birthdaylem2  26446  emcllem1  26489  emcllem2  26490  emcllem3  26491  emcllem5  26493  emcllem7  26495  harmoniclbnd  26502  harmonicubnd  26503  harmonicbnd4  26504  fsumharmonic  26505  lgamcvg2  26548  gamcvg2lem  26552  wilthlem1  26561  wilthlem2  26562  ftalem5  26570  basellem1  26574  basellem8  26581  chpf  26616  efchpcl  26618  chpp1  26648  chpwordi  26650  prmorcht  26671  dvdsflf1o  26680  dvdsflsumcom  26681  chtlepsi  26698  fsumvma2  26706  pclogsum  26707  vmasum  26708  logfac2  26709  chpval2  26710  chpchtsum  26711  logfaclbnd  26714  logexprlim  26717  logfacrlim2  26718  pcbcctr  26768  bposlem1  26776  bposlem2  26777  lgscllem  26796  lgsval2lem  26799  lgsval4a  26811  lgsneg  26813  lgsdir  26824  lgsdilem2  26825  lgsdi  26826  lgsne0  26827  lgsqrlem2  26839  lgseisenlem1  26867  lgseisenlem2  26868  lgseisenlem3  26869  lgseisenlem4  26870  lgseisen  26871  lgsquadlem1  26872  lgsquadlem2  26873  lgsquadlem3  26874  2lgslem1a1  26881  chebbnd1lem1  26961  vmadivsum  26974  vmadivsumb  26975  rplogsumlem2  26977  dchrisum0lem1a  26978  rpvmasumlem  26979  dchrisumlem2  26982  dchrmusum2  26986  dchrvmasumlem1  26987  dchrvmasum2lem  26988  dchrvmasum2if  26989  dchrvmasumlem2  26990  dchrvmasumlem3  26991  dchrvmasumiflem1  26993  dchrvmasumiflem2  26994  dchrisum0fno1  27003  rpvmasum2  27004  dchrisum0re  27005  dchrisum0lem1b  27007  dchrisum0lem1  27008  dchrisum0lem2a  27009  dchrisum0lem2  27010  dchrisum0lem3  27011  dchrisum0  27012  dchrmusumlem  27014  dchrvmasumlem  27015  rplogsum  27019  mudivsum  27022  mulogsumlem  27023  mulogsum  27024  mulog2sumlem1  27026  mulog2sumlem2  27027  mulog2sumlem3  27028  vmalogdivsum2  27030  vmalogdivsum  27031  2vmadivsumlem  27032  log2sumbnd  27036  selberglem1  27037  selberglem2  27038  selberglem3  27039  selberg  27040  selbergb  27041  selberg2lem  27042  selberg2  27043  selberg2b  27044  chpdifbndlem1  27045  logdivbnd  27048  selberg3lem1  27049  selberg3lem2  27050  selberg3  27051  selberg4lem1  27052  selberg4  27053  pntrsumo1  27057  pntrsumbnd  27058  pntrsumbnd2  27059  selbergr  27060  selberg3r  27061  selberg4r  27062  selberg34r  27063  pntsf  27065  pntsval2  27068  pntrlog2bndlem1  27069  pntrlog2bndlem2  27070  pntrlog2bndlem3  27071  pntrlog2bndlem4  27072  pntrlog2bndlem5  27073  pntrlog2bndlem6  27075  pntrlog2bnd  27076  pntpbnd2  27079  pntlemf  27097  pntlemk  27098  pntlemo  27099  eucrct2eupth  29487  dipcl  29952  dipcn  29960  prmdvdsbc  32009  freshmansdream  32369  esumpcvgval  33064  esumpmono  33065  esumcvg  33072  esumcvgsum  33074  eulerpartlemgc  33349  ballotlemfc0  33479  ballotlemfcc  33480  ballotlemic  33493  ballotlem1c  33494  ballotlemsel1i  33499  ballotlemsf1o  33500  erdszelem4  34173  erdszelem8  34177  erdsze2lem2  34183  cvmliftlem2  34265  cvmliftlem6  34269  cvmliftlem8  34271  cvmliftlem9  34272  cvmliftlem10  34273  bcprod  34696  faclim  34704  poimirlem6  36482  poimirlem7  36483  poimirlem8  36484  poimirlem9  36485  poimirlem11  36487  poimirlem13  36489  poimirlem14  36490  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem18  36494  poimirlem22  36498  poimirlem32  36508  mblfinlem2  36514  aks4d1p1p2  40923  aks4d1p1p4  40924  aks4d1p1  40929  aks4d1p3  40931  aks4d1p4  40932  aks4d1p5  40933  aks4d1p6  40934  aks4d1p7d1  40935  aks4d1p7  40936  aks4d1p8  40940  aks4d1p9  40941  sticksstones1  40950  sticksstones2  40951  sticksstones3  40952  sticksstones6  40955  sticksstones7  40956  sticksstones10  40959  sticksstones12a  40961  sticksstones12  40962  metakunt1  40973  metakunt2  40974  metakunt6  40978  metakunt7  40979  metakunt8  40980  metakunt9  40981  metakunt11  40983  metakunt15  40987  metakunt16  40988  metakunt21  40993  metakunt22  40994  metakunt27  40999  metakunt29  41001  metakunt30  41002  oddnumth  41204  nicomachus  41205  sumcubes  41206  eldioph3b  41488  diophin  41495  diophun  41496  eldiophss  41497  irrapxlem4  41548  sumnnodd  44332  stoweidlem34  44736  wallispilem4  44770  wallispi  44772  wallispi2lem1  44773  wallispi2  44775  stirlinglem5  44780  stirlinglem7  44782  stirlinglem10  44785  stirlinglem12  44787  fourierdlem83  44891  fourierdlem112  44920  caratheodorylem2  45229  hoidmvlelem2  45298  hoidmvlelem3  45299  altgsumbcALT  46982  nn0sumshdiglemA  47258  nn0sumshdiglemB  47259