Theorem elfznn 13608

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 13578	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13581	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12644	. 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 7413  1c1 11125   ≤ cle 11268  ℕcn 12257  ℤcz 12615  ...cfz 13561

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-z 12616  df-uz 12888  df-fz 13562

This theorem is used by:  elfz1end  13609  fz1ssnn  13610  bcm1k  14379  bcpasc  14385  seqcoll  14529  pfxfv0  14761  pfxfvlsw  14764  isercolllem2  15753  isercolllem3  15754  isercoll  15755  sumeq2ii  15780  summolem3  15800  summolem2a  15801  fsum  15806  sumz  15808  fsumconst  15876  o1fsum  15900  binomlem  15918  incexc2  15927  climcndslem1  15938  climcndslem2  15939  climcnds  15940  harmonic  15948  arisum2  15950  trireciplem  15951  pwdif  15957  geo2sum  15962  geo2lim  15964  prodeq2ii  16000  prodmolem3  16020  prodmolem2a  16021  fprod  16028  prod1  16031  fprodfac  16060  fprodconst  16065  risefallfac  16111  risefacfac  16121  fallfacval4  16129  bpolydiflem  16140  rpnnen2lem10  16311  fzm1ndvds  16412  pwp1fsum  16481  lcmflefac  16738  prmdvdsbc  16817  phicl  16860  prmdivdiv  16878  pcfac  16991  pcbc  16992  prmreclem2  17009  prmreclem3  17010  prmreclem4  17011  prmreclem5  17012  prmreclem6  17013  prmrec  17014  4sqlem13  17049  vdwlem2  17074  vdwlem3  17075  vdwlem10  17082  vdwlem12  17084  prmocl  17126  prmop1  17130  fvprmselelfz  17136  fvprmselgcd1  17137  prmolefac  17138  prmodvdslcmf  17139  prmgapprmo  17154  mulgnngsum  19202  mulgnnsubcl  19209  mulgnn0z  19224  mulgnndir  19226  oddvdsnn0  19671  odnncl  19672  gexcl3  19714  efgsres  19865  mulgnn0di  19952  gsumconst  20061  srgbinomlem4  20368  freshmansdream  21787  chfacfscmulgsum  23085  chfacfpmmulgsum  23089  chfacfpmmulgsum2  23090  cayhamlem1  23091  cpmadugsumlemF  23101  lebnumii  25194  ovollb2lem  25716  ovolunlem1a  25724  ovoliunlem1  25730  ovoliunlem2  25731  ovoliun2  25734  ovolscalem1  25741  ovolicc2lem4  25748  voliunlem1  25778  volsup  25784  ioombl1lem4  25789  uniioovol  25807  uniioombllem3a  25812  uniioombllem3  25813  uniioombllem4  25814  uniioombllem5  25815  uniioombllem6  25816  dvply1  26514  aaliou3lem5  26583  aaliou3lem6  26584  dvtaylp  26606  taylthlem2  26610  pserdvlem2  26664  logfac  26838  atantayl  27174  birthdaylem2  27189  emcllem1  27232  emcllem2  27233  emcllem3  27234  emcllem5  27236  emcllem7  27238  harmoniclbnd  27245  harmonicubnd  27246  harmonicbnd4  27247  fsumharmonic  27248  lgamcvg2  27291  gamcvg2lem  27295  wilthlem1  27304  wilthlem2  27305  ftalem5  27313  basellem1  27317  basellem8  27324  chpf  27359  efchpcl  27361  chpp1  27391  chpwordi  27393  prmorcht  27414  dvdsflf1o  27423  dvdsflsumcom  27424  chtlepsi  27442  fsumvma2  27450  pclogsum  27451  vmasum  27452  logfac2  27453  chpval2  27454  chpchtsum  27455  logfaclbnd  27458  logexprlim  27461  logfacrlim2  27462  pcbcctr  27512  bposlem1  27520  bposlem2  27521  lgscllem  27540  lgsval2lem  27543  lgsval4a  27555  lgsneg  27557  lgsdir  27568  lgsdilem2  27569  lgsdi  27570  lgsne0  27571  lgsqrlem2  27583  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisenlem4  27614  lgseisen  27615  lgsquadlem1  27616  lgsquadlem2  27617  lgsquadlem3  27618  2lgslem1a1  27625  chebbnd1lem1  27705  vmadivsum  27718  vmadivsumb  27719  rplogsumlem2  27721  dchrisum0lem1a  27722  rpvmasumlem  27723  dchrisumlem2  27726  dchrmusum2  27730  dchrvmasumlem1  27731  dchrvmasum2lem  27732  dchrvmasum2if  27733  dchrvmasumlem2  27734  dchrvmasumlem3  27735  dchrvmasumiflem1  27737  dchrvmasumiflem2  27738  dchrisum0fno1  27747  rpvmasum2  27748  dchrisum0re  27749  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2a  27753  dchrisum0lem2  27754  dchrisum0lem3  27755  dchrisum0  27756  dchrmusumlem  27758  dchrvmasumlem  27759  rplogsum  27763  mudivsum  27766  mulogsumlem  27767  mulogsum  27768  mulog2sumlem1  27770  mulog2sumlem2  27771  mulog2sumlem3  27772  vmalogdivsum2  27774  vmalogdivsum  27775  2vmadivsumlem  27776  log2sumbnd  27780  selberglem1  27781  selberglem2  27782  selberglem3  27783  selberg  27784  selbergb  27785  selberg2lem  27786  selberg2  27787  selberg2b  27788  chpdifbndlem1  27789  logdivbnd  27792  selberg3lem1  27793  selberg3lem2  27794  selberg3  27795  selberg4lem1  27796  selberg4  27797  pntrsumo1  27801  pntrsumbnd  27802  pntrsumbnd2  27803  selbergr  27804  selberg3r  27805  selberg4r  27806  selberg34r  27807  pntsf  27809  pntsval2  27812  pntrlog2bndlem1  27813  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  pntrlog2bnd  27820  pntpbnd2  27823  pntlemf  27841  pntlemk  27842  pntlemo  27843  eucrct2eupth  30725  dipcl  31193  dipcn  31201  gsummptp1  33497  gsummulsubdishift1  33508  esplyind  34085  esumpcvgval  34588  esumpmono  34589  esumcvg  34596  esumcvgsum  34598  eulerpartlemgc  34873  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemic  35018  ballotlem1c  35019  ballotlemsel1i  35024  ballotlemsf1o  35025  erdszelem4  35773  erdszelem8  35777  erdsze2lem2  35783  cvmliftlem2  35865  cvmliftlem6  35869  cvmliftlem8  35871  cvmliftlem9  35872  cvmliftlem10  35873  bcprod  36317  faclim  36325  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem9  38378  poimirlem11  38380  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem22  38391  poimirlem32  38401  mblfinlem2  38407  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1  42942  aks4d1p3  42944  aks4d1p4  42945  aks4d1p5  42946  aks4d1p6  42947  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8  42953  aks4d1p9  42954  primrootlekpowne0  42971  hashscontpow1  42987  hashscontpow  42988  sticksstones1  43012  sticksstones2  43013  sticksstones3  43014  sticksstones6  43017  sticksstones7  43018  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  oddnumth  43186  nicomachus  43187  sumcubes  43188  eldioph3b  43610  diophin  43617  diophun  43618  eldiophss  43619  irrapxlem4  43666  sumnnodd  46460  stoweidlem34  46862  wallispilem4  46896  wallispi  46898  wallispi2lem1  46899  wallispi2  46901  stirlinglem5  46906  stirlinglem7  46908  stirlinglem10  46911  stirlinglem12  46913  fourierdlem83  47017  fourierdlem112  47046  caratheodorylem2  47355  hoidmvlelem2  47424  hoidmvlelem3  47425  elfz2nn  48210  stgrusgra  48875  isubgr3stgrlem7  48888  altgsumbcALT  49283  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550