Theorem elfznn 13294

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 13265	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13268	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12355	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5075  (class class class)co 7284  1c1 10881   ≤ cle 11019  ℕcn 11982  ℤcz 12328  ...cfz 13248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-z 12329  df-uz 12592  df-fz 13249

This theorem is referenced by:  elfz1end  13295  fz1ssnn  13296  bcm1k  14038  bcpasc  14044  seqcoll  14187  pfxfv0  14414  pfxfvlsw  14417  isercolllem2  15386  isercolllem3  15387  isercoll  15388  sumeq2ii  15414  summolem3  15435  summolem2a  15436  fsum  15441  sumz  15443  fsumconst  15511  o1fsum  15534  binomlem  15550  incexc2  15559  climcndslem1  15570  climcndslem2  15571  climcnds  15572  harmonic  15580  arisum2  15582  trireciplem  15583  pwdif  15589  geo2sum  15594  geo2lim  15596  prodeq2ii  15632  prodmolem3  15652  prodmolem2a  15653  fprod  15660  prod1  15663  fprodfac  15692  fprodconst  15697  risefallfac  15743  risefacfac  15754  fallfacval4  15762  bpolydiflem  15773  rpnnen2lem10  15941  fzm1ndvds  16040  pwp1fsum  16109  lcmflefac  16362  phicl  16479  prmdivdiv  16497  pcfac  16609  pcbc  16610  prmreclem2  16627  prmreclem3  16628  prmreclem4  16629  prmreclem5  16630  prmreclem6  16631  prmrec  16632  4sqlem13  16667  vdwlem2  16692  vdwlem3  16693  vdwlem10  16700  vdwlem12  16702  prmocl  16744  prmop1  16748  fvprmselelfz  16754  fvprmselgcd1  16755  prmolefac  16756  prmodvdslcmf  16757  prmgapprmo  16772  mulgnngsum  18718  mulgnnsubcl  18725  mulgnn0z  18739  mulgnndir  18741  oddvdsnn0  19161  odnncl  19162  gexcl3  19201  efgsres  19353  mulgnn0di  19436  gsumconst  19544  srgbinomlem4  19788  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  chfacfpmmulgsum2  22023  cayhamlem1  22024  cpmadugsumlemF  22034  lebnumii  24138  ovollb2lem  24661  ovolunlem1a  24669  ovoliunlem1  24675  ovoliunlem2  24676  ovoliun2  24679  ovolscalem1  24686  ovolicc2lem4  24693  voliunlem1  24723  volsup  24729  ioombl1lem4  24734  uniioovol  24752  uniioombllem3a  24757  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  uniioombllem6  24761  dvply1  25453  aaliou3lem5  25516  aaliou3lem6  25517  dvtaylp  25538  taylthlem2  25542  pserdvlem2  25596  logfac  25765  atantayl  26096  birthdaylem2  26111  emcllem1  26154  emcllem2  26155  emcllem3  26156  emcllem5  26158  emcllem7  26160  harmoniclbnd  26167  harmonicubnd  26168  harmonicbnd4  26169  fsumharmonic  26170  lgamcvg2  26213  gamcvg2lem  26217  wilthlem1  26226  wilthlem2  26227  ftalem5  26235  basellem1  26239  basellem8  26246  chpf  26281  efchpcl  26283  chpp1  26313  chpwordi  26315  prmorcht  26336  dvdsflf1o  26345  dvdsflsumcom  26346  chtlepsi  26363  fsumvma2  26371  pclogsum  26372  vmasum  26373  logfac2  26374  chpval2  26375  chpchtsum  26376  logfaclbnd  26379  logexprlim  26382  logfacrlim2  26383  pcbcctr  26433  bposlem1  26441  bposlem2  26442  lgscllem  26461  lgsval2lem  26464  lgsval4a  26476  lgsneg  26478  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  lgsqrlem2  26504  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgseisen  26536  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  2lgslem1a1  26546  chebbnd1lem1  26626  vmadivsum  26639  vmadivsumb  26640  rplogsumlem2  26642  dchrisum0lem1a  26643  rpvmasumlem  26644  dchrisumlem2  26647  dchrmusum2  26651  dchrvmasumlem1  26652  dchrvmasum2lem  26653  dchrvmasum2if  26654  dchrvmasumlem2  26655  dchrvmasumlem3  26656  dchrvmasumiflem1  26658  dchrvmasumiflem2  26659  dchrisum0fno1  26668  rpvmasum2  26669  dchrisum0re  26670  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrisum0lem3  26676  dchrisum0  26677  dchrmusumlem  26679  dchrvmasumlem  26680  rplogsum  26684  mudivsum  26687  mulogsumlem  26688  mulogsum  26689  mulog2sumlem1  26691  mulog2sumlem2  26692  mulog2sumlem3  26693  vmalogdivsum2  26695  vmalogdivsum  26696  2vmadivsumlem  26697  log2sumbnd  26701  selberglem1  26702  selberglem2  26703  selberglem3  26704  selberg  26705  selbergb  26706  selberg2lem  26707  selberg2  26708  selberg2b  26709  chpdifbndlem1  26710  logdivbnd  26713  selberg3lem1  26714  selberg3lem2  26715  selberg3  26716  selberg4lem1  26717  selberg4  26718  pntrsumo1  26722  pntrsumbnd  26723  pntrsumbnd2  26724  selbergr  26725  selberg3r  26726  selberg4r  26727  selberg34r  26728  pntsf  26730  pntsval2  26733  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntpbnd2  26744  pntlemf  26762  pntlemk  26763  pntlemo  26764  eucrct2eupth  28618  dipcl  29083  dipcn  29091  prmdvdsbc  31139  freshmansdream  31493  esumpcvgval  32055  esumpmono  32056  esumcvg  32063  esumcvgsum  32065  eulerpartlemgc  32338  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemic  32482  ballotlem1c  32483  ballotlemsel1i  32488  ballotlemsf1o  32489  erdszelem4  33165  erdszelem8  33169  erdsze2lem2  33175  cvmliftlem2  33257  cvmliftlem6  33261  cvmliftlem8  33263  cvmliftlem9  33264  cvmliftlem10  33265  bcprod  33713  faclim  33721  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem9  35795  poimirlem11  35797  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem22  35808  poimirlem32  35818  mblfinlem2  35824  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1  40091  aks4d1p3  40093  aks4d1p4  40094  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8  40102  aks4d1p9  40103  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones6  40114  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  metakunt1  40132  metakunt2  40133  metakunt6  40137  metakunt7  40138  metakunt8  40139  metakunt9  40140  metakunt11  40142  metakunt15  40146  metakunt16  40147  metakunt21  40152  metakunt22  40153  metakunt27  40158  metakunt29  40160  metakunt30  40161  eldioph3b  40594  diophin  40601  diophun  40602  eldiophss  40603  irrapxlem4  40654  sumnnodd  43178  stoweidlem34  43582  wallispilem4  43616  wallispi  43618  wallispi2lem1  43619  wallispi2  43621  stirlinglem5  43626  stirlinglem7  43628  stirlinglem10  43631  stirlinglem12  43633  fourierdlem83  43737  fourierdlem112  43766  caratheodorylem2  44072  hoidmvlelem2  44141  hoidmvlelem3  44142  altgsumbcALT  45700  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977