Theorem elfznn 13580

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  (class class class)co 7411  1c1 11100   ≤ cle 11243  ℕcn 12232  ℤcz 12590  ...cfz 13534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  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 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-z 12591  df-uz 12862  df-fz 13535

This theorem is referenced by:  elfz1end  13581  fz1ssnn  13582  bcm1k  14350  bcpasc  14356  seqcoll  14500  pfxfv0  14728  pfxfvlsw  14731  isercolllem2  15716  isercolllem3  15717  isercoll  15718  sumeq2ii  15743  summolem3  15764  summolem2a  15765  fsum  15770  sumz  15772  fsumconst  15840  o1fsum  15864  binomlem  15882  incexc2  15891  climcndslem1  15902  climcndslem2  15903  climcnds  15904  harmonic  15912  arisum2  15914  trireciplem  15915  pwdif  15921  geo2sum  15926  geo2lim  15928  prodeq2ii  15964  prodmolem3  15986  prodmolem2a  15987  fprod  15994  prod1  15997  fprodfac  16026  fprodconst  16031  risefallfac  16077  risefacfac  16088  fallfacval4  16096  bpolydiflem  16107  rpnnen2lem10  16278  fzm1ndvds  16379  pwp1fsum  16448  lcmflefac  16705  prmdvdsbc  16784  phicl  16827  prmdivdiv  16845  pcfac  16958  pcbc  16959  prmreclem2  16976  prmreclem3  16977  prmreclem4  16978  prmreclem5  16979  prmreclem6  16980  prmrec  16981  4sqlem13  17016  vdwlem2  17041  vdwlem3  17042  vdwlem10  17049  vdwlem12  17051  prmocl  17093  prmop1  17097  fvprmselelfz  17103  fvprmselgcd1  17104  prmolefac  17105  prmodvdslcmf  17106  prmgapprmo  17121  mulgnngsum  19144  mulgnnsubcl  19151  mulgnn0z  19166  mulgnndir  19168  oddvdsnn0  19613  odnncl  19614  gexcl3  19656  efgsres  19807  mulgnn0di  19894  gsumconst  20003  srgbinomlem4  20310  freshmansdream  21692  chfacfscmulgsum  22985  chfacfpmmulgsum  22989  chfacfpmmulgsum2  22990  cayhamlem1  22991  cpmadugsumlemF  23001  lebnumii  25093  ovollb2lem  25615  ovolunlem1a  25623  ovoliunlem1  25629  ovoliunlem2  25630  ovoliun2  25633  ovolscalem1  25640  ovolicc2lem4  25647  voliunlem1  25677  volsup  25683  ioombl1lem4  25688  uniioovol  25706  uniioombllem3a  25711  uniioombllem3  25712  uniioombllem4  25713  uniioombllem5  25714  uniioombllem6  25715  dvply1  26413  aaliou3lem5  26476  aaliou3lem6  26477  dvtaylp  26498  taylthlem2  26502  pserdvlem2  26556  logfac  26731  atantayl  27067  birthdaylem2  27082  emcllem1  27125  emcllem2  27126  emcllem3  27127  emcllem5  27129  emcllem7  27131  harmoniclbnd  27138  harmonicubnd  27139  harmonicbnd4  27140  fsumharmonic  27141  lgamcvg2  27184  gamcvg2lem  27188  wilthlem1  27197  wilthlem2  27198  ftalem5  27206  basellem1  27210  basellem8  27217  chpf  27252  efchpcl  27254  chpp1  27284  chpwordi  27286  prmorcht  27307  dvdsflf1o  27316  dvdsflsumcom  27317  chtlepsi  27335  fsumvma2  27343  pclogsum  27344  vmasum  27345  logfac2  27346  chpval2  27347  chpchtsum  27348  logfaclbnd  27351  logexprlim  27354  logfacrlim2  27355  pcbcctr  27405  bposlem1  27413  bposlem2  27414  lgscllem  27433  lgsval2lem  27436  lgsval4a  27448  lgsneg  27450  lgsdir  27461  lgsdilem2  27462  lgsdi  27463  lgsne0  27464  lgsqrlem2  27476  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem3  27506  lgseisenlem4  27507  lgseisen  27508  lgsquadlem1  27509  lgsquadlem2  27510  lgsquadlem3  27511  2lgslem1a1  27518  chebbnd1lem1  27598  vmadivsum  27611  vmadivsumb  27612  rplogsumlem2  27614  dchrisum0lem1a  27615  rpvmasumlem  27616  dchrisumlem2  27619  dchrmusum2  27623  dchrvmasumlem1  27624  dchrvmasum2lem  27625  dchrvmasum2if  27626  dchrvmasumlem2  27627  dchrvmasumlem3  27628  dchrvmasumiflem1  27630  dchrvmasumiflem2  27631  dchrisum0fno1  27640  rpvmasum2  27641  dchrisum0re  27642  dchrisum0lem1b  27644  dchrisum0lem1  27645  dchrisum0lem2a  27646  dchrisum0lem2  27647  dchrisum0lem3  27648  dchrisum0  27649  dchrmusumlem  27651  dchrvmasumlem  27652  rplogsum  27656  mudivsum  27659  mulogsumlem  27660  mulogsum  27661  mulog2sumlem1  27663  mulog2sumlem2  27664  mulog2sumlem3  27665  vmalogdivsum2  27667  vmalogdivsum  27668  2vmadivsumlem  27669  log2sumbnd  27673  selberglem1  27674  selberglem2  27675  selberglem3  27676  selberg  27677  selbergb  27678  selberg2lem  27679  selberg2  27680  selberg2b  27681  chpdifbndlem1  27682  logdivbnd  27685  selberg3lem1  27686  selberg3lem2  27687  selberg3  27688  selberg4lem1  27689  selberg4  27690  pntrsumo1  27694  pntrsumbnd  27695  pntrsumbnd2  27696  selbergr  27697  selberg3r  27698  selberg4r  27699  selberg34r  27700  pntsf  27702  pntsval2  27705  pntrlog2bndlem1  27706  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntrlog2bnd  27713  pntpbnd2  27716  pntlemf  27734  pntlemk  27735  pntlemo  27736  eucrct2eupth  30536  dipcl  31004  dipcn  31012  gsummptp1  33317  gsummulsubdishift1  33328  esplyind  33909  esumpcvgval  34412  esumpmono  34413  esumcvg  34420  esumcvgsum  34422  eulerpartlemgc  34696  ballotlemfc0  34827  ballotlemfcc  34828  ballotlemic  34841  ballotlem1c  34842  ballotlemsel1i  34847  ballotlemsf1o  34848  erdszelem4  35584  erdszelem8  35588  erdsze2lem2  35594  cvmliftlem2  35676  cvmliftlem6  35680  cvmliftlem8  35682  cvmliftlem9  35683  cvmliftlem10  35684  bcprod  36128  faclim  36136  poimirlem6  38164  poimirlem7  38165  poimirlem8  38166  poimirlem9  38167  poimirlem11  38169  poimirlem13  38171  poimirlem14  38172  poimirlem15  38173  poimirlem16  38174  poimirlem17  38175  poimirlem18  38176  poimirlem22  38180  poimirlem32  38190  mblfinlem2  38196  aks4d1p1p2  42726  aks4d1p1p4  42727  aks4d1p1  42732  aks4d1p3  42734  aks4d1p4  42735  aks4d1p5  42736  aks4d1p6  42737  aks4d1p7d1  42738  aks4d1p7  42739  aks4d1p8  42743  aks4d1p9  42744  primrootlekpowne0  42761  hashscontpow1  42777  hashscontpow  42778  sticksstones1  42802  sticksstones2  42803  sticksstones3  42804  sticksstones6  42807  sticksstones7  42808  sticksstones10  42811  sticksstones12a  42813  sticksstones12  42814  oddnumth  42961  nicomachus  42962  sumcubes  42963  eldioph3b  43387  diophin  43394  diophun  43395  eldiophss  43396  irrapxlem4  43443  sumnnodd  46237  stoweidlem34  46639  wallispilem4  46673  wallispi  46675  wallispi2lem1  46676  wallispi2  46678  stirlinglem5  46683  stirlinglem7  46685  stirlinglem10  46688  stirlinglem12  46690  fourierdlem83  46794  fourierdlem112  46823  caratheodorylem2  47132  hoidmvlelem2  47201  hoidmvlelem3  47202  elfz2nn  47947  stgrusgra  48612  isubgr3stgrlem7  48625  altgsumbcALT  49017  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284