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

Theorem elfznn 12484
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 12456 . 2 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2 elfzle1 12458 . 2 (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3 elnnz1 11516 . 2 (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
41, 2, 3sylanbrc 701 1 (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2103   class class class wbr 4760  (class class class)co 6765  1c1 10050  cle 10188  cn 11133  cz 11490  ...cfz 12440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-z 11491  df-uz 11801  df-fz 12441
This theorem is referenced by:  elfz1end  12485  fz1ssnn  12486  fzossnn  12632  bcm1k  13217  bcpasc  13223  seqcoll  13361  swrd0fv0  13561  swrd0fvlsw  13564  isercolllem2  14516  isercolllem3  14517  isercoll  14518  sumeq2ii  14543  summolem3  14565  summolem2a  14566  fsum  14571  sumz  14573  fsumconst  14642  o1fsum  14665  binomlem  14681  incexc2  14690  climcndslem1  14701  climcndslem2  14702  climcnds  14703  harmonic  14711  arisum2  14713  trireciplem  14714  geo2sum  14724  geo2lim  14726  prodeq2ii  14763  prodmolem3  14783  prodmolem2a  14784  fprod  14791  prod1  14794  fprodfac  14823  fprodconst  14828  risefallfac  14875  risefacfac  14886  fallfacval4  14894  bpolydiflem  14905  rpnnen2lem10  15072  fzm1ndvds  15167  pwp1fsum  15237  lcmflefac  15484  phicl  15597  prmdivdiv  15615  pcfac  15726  pcbc  15727  prmreclem2  15744  prmreclem3  15745  prmreclem4  15746  prmreclem5  15747  prmreclem6  15748  prmrec  15749  4sqlem13  15784  vdwlem2  15809  vdwlem3  15810  vdwlem10  15817  vdwlem12  15819  prmocl  15861  prmop1  15865  fvprmselelfz  15871  fvprmselgcd1  15872  prmolefac  15873  prmodvdslcmf  15874  prmgapprmo  15889  mulgnnsubcl  17675  mulgnn0z  17689  mulgnndir  17691  mulgnndirOLD  17692  oddvdsnn0  18084  odnncl  18085  gexcl3  18123  efgsres  18272  mulgnn0di  18352  gsumconst  18455  srgbinomlem4  18664  chfacfscmulgsum  20788  chfacfpmmulgsum  20792  chfacfpmmulgsum2  20793  cayhamlem1  20794  cpmadugsumlemF  20804  1stcfb  21371  1stckgenlem  21479  lebnumii  22887  ovollb2lem  23377  ovolunlem1a  23385  ovoliunlem1  23391  ovoliunlem2  23392  ovoliun2  23395  ovolscalem1  23402  ovolicc2lem4  23409  voliunlem1  23439  volsup  23445  ioombl1lem4  23450  uniioovol  23468  uniioombllem3a  23473  uniioombllem3  23474  uniioombllem4  23475  uniioombllem5  23476  uniioombllem6  23477  dvply1  24159  aaliou3lem5  24222  aaliou3lem6  24223  dvtaylp  24244  taylthlem2  24248  pserdvlem2  24302  logfac  24467  atantayl  24784  birthdaylem2  24799  emcllem1  24842  emcllem2  24843  emcllem3  24844  emcllem5  24846  emcllem7  24848  harmoniclbnd  24855  harmonicubnd  24856  harmonicbnd4  24857  fsumharmonic  24858  lgamcvg2  24901  gamcvg2lem  24905  wilthlem1  24914  wilthlem2  24915  ftalem5  24923  basellem1  24927  basellem8  24934  chpf  24969  efchpcl  24971  chpp1  25001  chpwordi  25003  prmorcht  25024  dvdsflf1o  25033  dvdsflsumcom  25034  chtlepsi  25051  fsumvma2  25059  pclogsum  25060  vmasum  25061  logfac2  25062  chpval2  25063  chpchtsum  25064  logfaclbnd  25067  logexprlim  25070  logfacrlim2  25071  pcbcctr  25121  bposlem1  25129  bposlem2  25130  lgscllem  25149  lgsval2lem  25152  lgsval4a  25164  lgsneg  25166  lgsdir  25177  lgsdilem2  25178  lgsdi  25179  lgsne0  25180  lgsqrlem2  25192  lgseisenlem1  25220  lgseisenlem2  25221  lgseisenlem3  25222  lgseisenlem4  25223  lgseisen  25224  lgsquadlem1  25225  lgsquadlem2  25226  lgsquadlem3  25227  2lgslem1a1  25234  chebbnd1lem1  25278  vmadivsum  25291  vmadivsumb  25292  rplogsumlem2  25294  dchrisum0lem1a  25295  rpvmasumlem  25296  dchrisumlem2  25299  dchrmusum2  25303  dchrvmasumlem1  25304  dchrvmasum2lem  25305  dchrvmasum2if  25306  dchrvmasumlem2  25307  dchrvmasumlem3  25308  dchrvmasumiflem1  25310  dchrvmasumiflem2  25311  dchrisum0fno1  25320  rpvmasum2  25321  dchrisum0re  25322  dchrisum0lem1b  25324  dchrisum0lem1  25325  dchrisum0lem2a  25326  dchrisum0lem2  25327  dchrisum0lem3  25328  dchrisum0  25329  dchrmusumlem  25331  dchrvmasumlem  25332  rplogsum  25336  mudivsum  25339  mulogsumlem  25340  mulogsum  25341  mulog2sumlem1  25343  mulog2sumlem2  25344  mulog2sumlem3  25345  vmalogdivsum2  25347  vmalogdivsum  25348  2vmadivsumlem  25349  log2sumbnd  25353  selberglem1  25354  selberglem2  25355  selberglem3  25356  selberg  25357  selbergb  25358  selberg2lem  25359  selberg2  25360  selberg2b  25361  chpdifbndlem1  25362  logdivbnd  25365  selberg3lem1  25366  selberg3lem2  25367  selberg3  25368  selberg4lem1  25369  selberg4  25370  pntrsumo1  25374  pntrsumbnd  25375  pntrsumbnd2  25376  selbergr  25377  selberg3r  25378  selberg4r  25379  selberg34r  25380  pntsf  25382  pntsval2  25385  pntrlog2bndlem1  25386  pntrlog2bndlem2  25387  pntrlog2bndlem3  25388  pntrlog2bndlem4  25389  pntrlog2bndlem5  25390  pntrlog2bndlem6  25392  pntrlog2bnd  25393  pntpbnd2  25396  pntlemf  25414  pntlemk  25415  pntlemo  25416  eucrct2eupth  27318  dipcl  27797  dipcn  27805  esumpcvgval  30370  esumpmono  30371  esumcvg  30378  esumcvgsum  30380  eulerpartlemgc  30654  ballotlemfc0  30784  ballotlemfcc  30785  ballotlemimin  30797  ballotlemic  30798  ballotlem1c  30799  ballotlemsel1i  30804  ballotlemsf1o  30805  erdszelem4  31404  erdszelem8  31408  erdsze2lem2  31414  cvmliftlem2  31496  cvmliftlem6  31500  cvmliftlem8  31502  cvmliftlem9  31503  cvmliftlem10  31504  bcprod  31852  faclim  31860  poimirlem6  33647  poimirlem7  33648  poimirlem8  33649  poimirlem9  33650  poimirlem11  33652  poimirlem13  33654  poimirlem14  33655  poimirlem15  33656  poimirlem16  33657  poimirlem17  33658  poimirlem18  33659  poimirlem22  33663  poimirlem32  33673  mblfinlem2  33679  eldioph3b  37747  diophin  37755  diophun  37756  eldiophss  37757  irrapxlem4  37808  sumnnodd  40282  stoweidlem34  40671  wallispilem4  40705  wallispi  40707  wallispi2lem1  40708  wallispi2  40710  stirlinglem5  40715  stirlinglem7  40717  stirlinglem10  40720  stirlinglem12  40722  fourierdlem83  40826  fourierdlem112  40855  caratheodorylem2  41164  hoidmvlelem2  41233  hoidmvlelem3  41234  pfxfv0  41827  pfxfvlsw  41830  pwdif  41928  altgsumbcALT  42558  nn0sumshdiglemA  42840  nn0sumshdiglemB  42841
  Copyright terms: Public domain W3C validator