Theorem elfznn 13569

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

Syntax hints:   → wi 4   ∈ wcel 2145   class class class wbr 5104  (class class class)co 7400  1c1 11089   ≤ cle 11232  ℕcn 12221  ℤcz 12579  ...cfz 13523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-nn 12222  df-z 12580  df-uz 12851  df-fz 13524

This theorem is referenced by:  elfz1end  13570  fz1ssnn  13571  bcm1k  14339  bcpasc  14345  seqcoll  14489  pfxfv0  14717  pfxfvlsw  14720  isercolllem2  15705  isercolllem3  15706  isercoll  15707  sumeq2ii  15732  summolem3  15753  summolem2a  15754  fsum  15759  sumz  15761  fsumconst  15829  o1fsum  15853  binomlem  15871  incexc2  15880  climcndslem1  15891  climcndslem2  15892  climcnds  15893  harmonic  15901  arisum2  15903  trireciplem  15904  pwdif  15910  geo2sum  15915  geo2lim  15917  prodeq2ii  15953  prodmolem3  15975  prodmolem2a  15976  fprod  15983  prod1  15986  fprodfac  16015  fprodconst  16020  risefallfac  16066  risefacfac  16077  fallfacval4  16085  bpolydiflem  16096  rpnnen2lem10  16267  fzm1ndvds  16368  pwp1fsum  16437  lcmflefac  16694  prmdvdsbc  16773  phicl  16816  prmdivdiv  16834  pcfac  16947  pcbc  16948  prmreclem2  16965  prmreclem3  16966  prmreclem4  16967  prmreclem5  16968  prmreclem6  16969  prmrec  16970  4sqlem13  17005  vdwlem2  17030  vdwlem3  17031  vdwlem10  17038  vdwlem12  17040  prmocl  17082  prmop1  17086  fvprmselelfz  17092  fvprmselgcd1  17093  prmolefac  17094  prmodvdslcmf  17095  prmgapprmo  17110  mulgnngsum  19133  mulgnnsubcl  19140  mulgnn0z  19155  mulgnndir  19157  oddvdsnn0  19602  odnncl  19603  gexcl3  19645  efgsres  19796  mulgnn0di  19883  gsumconst  19992  srgbinomlem4  20299  freshmansdream  21681  chfacfscmulgsum  22974  chfacfpmmulgsum  22978  chfacfpmmulgsum2  22979  cayhamlem1  22980  cpmadugsumlemF  22990  lebnumii  25082  ovollb2lem  25604  ovolunlem1a  25612  ovoliunlem1  25618  ovoliunlem2  25619  ovoliun2  25622  ovolscalem1  25629  ovolicc2lem4  25636  voliunlem1  25666  volsup  25672  ioombl1lem4  25677  uniioovol  25695  uniioombllem3a  25700  uniioombllem3  25701  uniioombllem4  25702  uniioombllem5  25703  uniioombllem6  25704  dvply1  26402  aaliou3lem5  26465  aaliou3lem6  26466  dvtaylp  26487  taylthlem2  26491  pserdvlem2  26545  logfac  26720  atantayl  27056  birthdaylem2  27071  emcllem1  27114  emcllem2  27115  emcllem3  27116  emcllem5  27118  emcllem7  27120  harmoniclbnd  27127  harmonicubnd  27128  harmonicbnd4  27129  fsumharmonic  27130  lgamcvg2  27173  gamcvg2lem  27177  wilthlem1  27186  wilthlem2  27187  ftalem5  27195  basellem1  27199  basellem8  27206  chpf  27241  efchpcl  27243  chpp1  27273  chpwordi  27275  prmorcht  27296  dvdsflf1o  27305  dvdsflsumcom  27306  chtlepsi  27324  fsumvma2  27332  pclogsum  27333  vmasum  27334  logfac2  27335  chpval2  27336  chpchtsum  27337  logfaclbnd  27340  logexprlim  27343  logfacrlim2  27344  pcbcctr  27394  bposlem1  27402  bposlem2  27403  lgscllem  27422  lgsval2lem  27425  lgsval4a  27437  lgsneg  27439  lgsdir  27450  lgsdilem2  27451  lgsdi  27452  lgsne0  27453  lgsqrlem2  27465  lgseisenlem1  27493  lgseisenlem2  27494  lgseisenlem3  27495  lgseisenlem4  27496  lgseisen  27497  lgsquadlem1  27498  lgsquadlem2  27499  lgsquadlem3  27500  2lgslem1a1  27507  chebbnd1lem1  27587  vmadivsum  27600  vmadivsumb  27601  rplogsumlem2  27603  dchrisum0lem1a  27604  rpvmasumlem  27605  dchrisumlem2  27608  dchrmusum2  27612  dchrvmasumlem1  27613  dchrvmasum2lem  27614  dchrvmasum2if  27615  dchrvmasumlem2  27616  dchrvmasumlem3  27617  dchrvmasumiflem1  27619  dchrvmasumiflem2  27620  dchrisum0fno1  27629  rpvmasum2  27630  dchrisum0re  27631  dchrisum0lem1b  27633  dchrisum0lem1  27634  dchrisum0lem2a  27635  dchrisum0lem2  27636  dchrisum0lem3  27637  dchrisum0  27638  dchrmusumlem  27640  dchrvmasumlem  27641  rplogsum  27645  mudivsum  27648  mulogsumlem  27649  mulogsum  27650  mulog2sumlem1  27652  mulog2sumlem2  27653  mulog2sumlem3  27654  vmalogdivsum2  27656  vmalogdivsum  27657  2vmadivsumlem  27658  log2sumbnd  27662  selberglem1  27663  selberglem2  27664  selberglem3  27665  selberg  27666  selbergb  27667  selberg2lem  27668  selberg2  27669  selberg2b  27670  chpdifbndlem1  27671  logdivbnd  27674  selberg3lem1  27675  selberg3lem2  27676  selberg3  27677  selberg4lem1  27678  selberg4  27679  pntrsumo1  27683  pntrsumbnd  27684  pntrsumbnd2  27685  selbergr  27686  selberg3r  27687  selberg4r  27688  selberg34r  27689  pntsf  27691  pntsval2  27694  pntrlog2bndlem1  27695  pntrlog2bndlem2  27696  pntrlog2bndlem3  27697  pntrlog2bndlem4  27698  pntrlog2bndlem5  27699  pntrlog2bndlem6  27701  pntrlog2bnd  27702  pntpbnd2  27705  pntlemf  27723  pntlemk  27724  pntlemo  27725  eucrct2eupth  30501  dipcl  30969  dipcn  30977  gsummptp1  33285  gsummulsubdishift1  33296  esplyind  33877  esumpcvgval  34380  esumpmono  34381  esumcvg  34388  esumcvgsum  34390  eulerpartlemgc  34664  ballotlemfc0  34795  ballotlemfcc  34796  ballotlemic  34809  ballotlem1c  34810  ballotlemsel1i  34815  ballotlemsf1o  34816  erdszelem4  35552  erdszelem8  35556  erdsze2lem2  35562  cvmliftlem2  35644  cvmliftlem6  35648  cvmliftlem8  35650  cvmliftlem9  35651  cvmliftlem10  35652  bcprod  36096  faclim  36104  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem9  38135  poimirlem11  38137  poimirlem13  38139  poimirlem14  38140  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem18  38144  poimirlem22  38148  poimirlem32  38158  mblfinlem2  38164  aks4d1p1p2  42694  aks4d1p1p4  42695  aks4d1p1  42700  aks4d1p3  42702  aks4d1p4  42703  aks4d1p5  42704  aks4d1p6  42705  aks4d1p7d1  42706  aks4d1p7  42707  aks4d1p8  42711  aks4d1p9  42712  primrootlekpowne0  42729  hashscontpow1  42745  hashscontpow  42746  sticksstones1  42770  sticksstones2  42771  sticksstones3  42772  sticksstones6  42775  sticksstones7  42776  sticksstones10  42779  sticksstones12a  42781  sticksstones12  42782  oddnumth  42927  nicomachus  42928  sumcubes  42929  eldioph3b  43353  diophin  43360  diophun  43361  eldiophss  43362  irrapxlem4  43409  sumnnodd  46205  stoweidlem34  46607  wallispilem4  46641  wallispi  46643  wallispi2lem1  46644  wallispi2  46646  stirlinglem5  46651  stirlinglem7  46653  stirlinglem10  46656  stirlinglem12  46658  fourierdlem83  46762  fourierdlem112  46791  caratheodorylem2  47100  hoidmvlelem2  47169  hoidmvlelem3  47170  elfz2nn  47915  stgrusgra  48580  isubgr3stgrlem7  48593  altgsumbcALT  48985  nn0sumshdiglemA  49251  nn0sumshdiglemB  49252