MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfznn Structured version   Visualization version   GIF version

Theorem elfznn 12935
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
StepHypRef Expression
1 elfzelz 12906 . 2 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2 elfzle1 12909 . 2 (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3 elnnz1 12000 . 2 (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
41, 2, 3sylanbrc 586 1 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112   class class class wbr 5033  (class class class)co 7139  1c1 10531  cle 10669  cn 11629  cz 11973  ...cfz 12889
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-z 11974  df-uz 12236  df-fz 12890
This theorem is referenced by:  elfz1end  12936  fz1ssnn  12937  bcm1k  13675  bcpasc  13681  seqcoll  13822  pfxfv0  14049  pfxfvlsw  14052  isercolllem2  15017  isercolllem3  15018  isercoll  15019  sumeq2ii  15045  summolem3  15066  summolem2a  15067  fsum  15072  sumz  15074  fsumconst  15140  o1fsum  15163  binomlem  15179  incexc2  15188  climcndslem1  15199  climcndslem2  15200  climcnds  15201  harmonic  15209  arisum2  15211  trireciplem  15212  pwdif  15218  geo2sum  15224  geo2lim  15226  prodeq2ii  15262  prodmolem3  15282  prodmolem2a  15283  fprod  15290  prod1  15293  fprodfac  15322  fprodconst  15327  risefallfac  15373  risefacfac  15384  fallfacval4  15392  bpolydiflem  15403  rpnnen2lem10  15571  fzm1ndvds  15667  pwp1fsum  15735  lcmflefac  15985  phicl  16099  prmdivdiv  16117  pcfac  16228  pcbc  16229  prmreclem2  16246  prmreclem3  16247  prmreclem4  16248  prmreclem5  16249  prmreclem6  16250  prmrec  16251  4sqlem13  16286  vdwlem2  16311  vdwlem3  16312  vdwlem10  16319  vdwlem12  16321  prmocl  16363  prmop1  16367  fvprmselelfz  16373  fvprmselgcd1  16374  prmolefac  16375  prmodvdslcmf  16376  prmgapprmo  16391  mulgnngsum  18228  mulgnnsubcl  18235  mulgnn0z  18249  mulgnndir  18251  oddvdsnn0  18667  odnncl  18668  gexcl3  18707  efgsres  18859  mulgnn0di  18942  gsumconst  19050  srgbinomlem4  19289  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmadugsumlemF  21484  lebnumii  23574  ovollb2lem  24095  ovolunlem1a  24103  ovoliunlem1  24109  ovoliunlem2  24110  ovoliun2  24113  ovolscalem1  24120  ovolicc2lem4  24127  voliunlem1  24157  volsup  24163  ioombl1lem4  24168  uniioovol  24186  uniioombllem3a  24191  uniioombllem3  24192  uniioombllem4  24193  uniioombllem5  24194  uniioombllem6  24195  dvply1  24883  aaliou3lem5  24946  aaliou3lem6  24947  dvtaylp  24968  taylthlem2  24972  pserdvlem2  25026  logfac  25195  atantayl  25526  birthdaylem2  25541  emcllem1  25584  emcllem2  25585  emcllem3  25586  emcllem5  25588  emcllem7  25590  harmoniclbnd  25597  harmonicubnd  25598  harmonicbnd4  25599  fsumharmonic  25600  lgamcvg2  25643  gamcvg2lem  25647  wilthlem1  25656  wilthlem2  25657  ftalem5  25665  basellem1  25669  basellem8  25676  chpf  25711  efchpcl  25713  chpp1  25743  chpwordi  25745  prmorcht  25766  dvdsflf1o  25775  dvdsflsumcom  25776  chtlepsi  25793  fsumvma2  25801  pclogsum  25802  vmasum  25803  logfac2  25804  chpval2  25805  chpchtsum  25806  logfaclbnd  25809  logexprlim  25812  logfacrlim2  25813  pcbcctr  25863  bposlem1  25871  bposlem2  25872  lgscllem  25891  lgsval2lem  25894  lgsval4a  25906  lgsneg  25908  lgsdir  25919  lgsdilem2  25920  lgsdi  25921  lgsne0  25922  lgsqrlem2  25934  lgseisenlem1  25962  lgseisenlem2  25963  lgseisenlem3  25964  lgseisenlem4  25965  lgseisen  25966  lgsquadlem1  25967  lgsquadlem2  25968  lgsquadlem3  25969  2lgslem1a1  25976  chebbnd1lem1  26056  vmadivsum  26069  vmadivsumb  26070  rplogsumlem2  26072  dchrisum0lem1a  26073  rpvmasumlem  26074  dchrisumlem2  26077  dchrmusum2  26081  dchrvmasumlem1  26082  dchrvmasum2lem  26083  dchrvmasum2if  26084  dchrvmasumlem2  26085  dchrvmasumlem3  26086  dchrvmasumiflem1  26088  dchrvmasumiflem2  26089  dchrisum0fno1  26098  rpvmasum2  26099  dchrisum0re  26100  dchrisum0lem1b  26102  dchrisum0lem1  26103  dchrisum0lem2a  26104  dchrisum0lem2  26105  dchrisum0lem3  26106  dchrisum0  26107  dchrmusumlem  26109  dchrvmasumlem  26110  rplogsum  26114  mudivsum  26117  mulogsumlem  26118  mulogsum  26119  mulog2sumlem1  26121  mulog2sumlem2  26122  mulog2sumlem3  26123  vmalogdivsum2  26125  vmalogdivsum  26126  2vmadivsumlem  26127  log2sumbnd  26131  selberglem1  26132  selberglem2  26133  selberglem3  26134  selberg  26135  selbergb  26136  selberg2lem  26137  selberg2  26138  selberg2b  26139  chpdifbndlem1  26140  logdivbnd  26143  selberg3lem1  26144  selberg3lem2  26145  selberg3  26146  selberg4lem1  26147  selberg4  26148  pntrsumo1  26152  pntrsumbnd  26153  pntrsumbnd2  26154  selbergr  26155  selberg3r  26156  selberg4r  26157  selberg34r  26158  pntsf  26160  pntsval2  26163  pntrlog2bndlem1  26164  pntrlog2bndlem2  26165  pntrlog2bndlem3  26166  pntrlog2bndlem4  26167  pntrlog2bndlem5  26168  pntrlog2bndlem6  26170  pntrlog2bnd  26171  pntpbnd2  26174  pntlemf  26192  pntlemk  26193  pntlemo  26194  eucrct2eupth  28033  dipcl  28498  dipcn  28506  prmdvdsbc  30561  freshmansdream  30912  esumpcvgval  31445  esumpmono  31446  esumcvg  31453  esumcvgsum  31455  eulerpartlemgc  31728  ballotlemfc0  31858  ballotlemfcc  31859  ballotlemimin  31871  ballotlemic  31872  ballotlem1c  31873  ballotlemsel1i  31878  ballotlemsf1o  31879  erdszelem4  32549  erdszelem8  32553  erdsze2lem2  32559  cvmliftlem2  32641  cvmliftlem6  32645  cvmliftlem8  32647  cvmliftlem9  32648  cvmliftlem10  32649  bcprod  33078  faclim  33086  poimirlem6  35056  poimirlem7  35057  poimirlem8  35058  poimirlem9  35059  poimirlem11  35061  poimirlem13  35063  poimirlem14  35064  poimirlem15  35065  poimirlem16  35066  poimirlem17  35067  poimirlem18  35068  poimirlem22  35072  poimirlem32  35082  mblfinlem2  35088  metakunt1  39341  metakunt2  39342  metakunt6  39346  metakunt7  39347  metakunt8  39348  metakunt9  39349  metakunt11  39351  metakunt12  39352  metakunt15  39355  metakunt16  39356  metakunt21  39361  metakunt22  39362  metakunt27  39367  metakunt29  39369  metakunt30  39370  eldioph3b  39693  diophin  39700  diophun  39701  eldiophss  39702  irrapxlem4  39753  sumnnodd  42259  stoweidlem34  42663  wallispilem4  42697  wallispi  42699  wallispi2lem1  42700  wallispi2  42702  stirlinglem5  42707  stirlinglem7  42709  stirlinglem10  42712  stirlinglem12  42714  fourierdlem83  42818  fourierdlem112  42847  caratheodorylem2  43153  hoidmvlelem2  43222  hoidmvlelem3  43223  altgsumbcALT  44742  nn0sumshdiglemA  45020  nn0sumshdiglemB  45021
  Copyright terms: Public domain W3C validator