Theorem elfznn 13391

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 13362	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 13365	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12452	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5097  (class class class)co 7342  1c1 10978   ≤ cle 11116  ℕcn 12079  ℤcz 12425  ...cfz 13345

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-cnex 11033  ax-resscn 11034  ax-1cn 11035  ax-icn 11036  ax-addcl 11037  ax-addrcl 11038  ax-mulcl 11039  ax-mulrcl 11040  ax-mulcom 11041  ax-addass 11042  ax-mulass 11043  ax-distr 11044  ax-i2m1 11045  ax-1ne0 11046  ax-1rid 11047  ax-rnegex 11048  ax-rrecex 11049  ax-cnre 11050  ax-pre-lttri 11051  ax-pre-lttrn 11052  ax-pre-ltadd 11053  ax-pre-mulgt0 11054

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-om 7786  df-1st 7904  df-2nd 7905  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-er 8574  df-en 8810  df-dom 8811  df-sdom 8812  df-pnf 11117  df-mnf 11118  df-xr 11119  df-ltxr 11120  df-le 11121  df-sub 11313  df-neg 11314  df-nn 12080  df-z 12426  df-uz 12689  df-fz 13346

This theorem is referenced by:  elfz1end  13392  fz1ssnn  13393  bcm1k  14135  bcpasc  14141  seqcoll  14283  pfxfv0  14504  pfxfvlsw  14507  isercolllem2  15477  isercolllem3  15478  isercoll  15479  sumeq2ii  15505  summolem3  15526  summolem2a  15527  fsum  15532  sumz  15534  fsumconst  15602  o1fsum  15625  binomlem  15641  incexc2  15650  climcndslem1  15661  climcndslem2  15662  climcnds  15663  harmonic  15671  arisum2  15673  trireciplem  15674  pwdif  15680  geo2sum  15685  geo2lim  15687  prodeq2ii  15723  prodmolem3  15743  prodmolem2a  15744  fprod  15751  prod1  15754  fprodfac  15783  fprodconst  15788  risefallfac  15834  risefacfac  15845  fallfacval4  15853  bpolydiflem  15864  rpnnen2lem10  16032  fzm1ndvds  16131  pwp1fsum  16200  lcmflefac  16451  phicl  16568  prmdivdiv  16586  pcfac  16698  pcbc  16699  prmreclem2  16716  prmreclem3  16717  prmreclem4  16718  prmreclem5  16719  prmreclem6  16720  prmrec  16721  4sqlem13  16756  vdwlem2  16781  vdwlem3  16782  vdwlem10  16789  vdwlem12  16791  prmocl  16833  prmop1  16837  fvprmselelfz  16843  fvprmselgcd1  16844  prmolefac  16845  prmodvdslcmf  16846  prmgapprmo  16861  mulgnngsum  18806  mulgnnsubcl  18813  mulgnn0z  18827  mulgnndir  18829  oddvdsnn0  19249  odnncl  19250  gexcl3  19289  efgsres  19440  mulgnn0di  19523  gsumconst  19630  srgbinomlem4  19874  chfacfscmulgsum  22115  chfacfpmmulgsum  22119  chfacfpmmulgsum2  22120  cayhamlem1  22121  cpmadugsumlemF  22131  lebnumii  24235  ovollb2lem  24758  ovolunlem1a  24766  ovoliunlem1  24772  ovoliunlem2  24773  ovoliun2  24776  ovolscalem1  24783  ovolicc2lem4  24790  voliunlem1  24820  volsup  24826  ioombl1lem4  24831  uniioovol  24849  uniioombllem3a  24854  uniioombllem3  24855  uniioombllem4  24856  uniioombllem5  24857  uniioombllem6  24858  dvply1  25550  aaliou3lem5  25613  aaliou3lem6  25614  dvtaylp  25635  taylthlem2  25639  pserdvlem2  25693  logfac  25862  atantayl  26193  birthdaylem2  26208  emcllem1  26251  emcllem2  26252  emcllem3  26253  emcllem5  26255  emcllem7  26257  harmoniclbnd  26264  harmonicubnd  26265  harmonicbnd4  26266  fsumharmonic  26267  lgamcvg2  26310  gamcvg2lem  26314  wilthlem1  26323  wilthlem2  26324  ftalem5  26332  basellem1  26336  basellem8  26343  chpf  26378  efchpcl  26380  chpp1  26410  chpwordi  26412  prmorcht  26433  dvdsflf1o  26442  dvdsflsumcom  26443  chtlepsi  26460  fsumvma2  26468  pclogsum  26469  vmasum  26470  logfac2  26471  chpval2  26472  chpchtsum  26473  logfaclbnd  26476  logexprlim  26479  logfacrlim2  26480  pcbcctr  26530  bposlem1  26538  bposlem2  26539  lgscllem  26558  lgsval2lem  26561  lgsval4a  26573  lgsneg  26575  lgsdir  26586  lgsdilem2  26587  lgsdi  26588  lgsne0  26589  lgsqrlem2  26601  lgseisenlem1  26629  lgseisenlem2  26630  lgseisenlem3  26631  lgseisenlem4  26632  lgseisen  26633  lgsquadlem1  26634  lgsquadlem2  26635  lgsquadlem3  26636  2lgslem1a1  26643  chebbnd1lem1  26723  vmadivsum  26736  vmadivsumb  26737  rplogsumlem2  26739  dchrisum0lem1a  26740  rpvmasumlem  26741  dchrisumlem2  26744  dchrmusum2  26748  dchrvmasumlem1  26749  dchrvmasum2lem  26750  dchrvmasum2if  26751  dchrvmasumlem2  26752  dchrvmasumlem3  26753  dchrvmasumiflem1  26755  dchrvmasumiflem2  26756  dchrisum0fno1  26765  rpvmasum2  26766  dchrisum0re  26767  dchrisum0lem1b  26769  dchrisum0lem1  26770  dchrisum0lem2a  26771  dchrisum0lem2  26772  dchrisum0lem3  26773  dchrisum0  26774  dchrmusumlem  26776  dchrvmasumlem  26777  rplogsum  26781  mudivsum  26784  mulogsumlem  26785  mulogsum  26786  mulog2sumlem1  26788  mulog2sumlem2  26789  mulog2sumlem3  26790  vmalogdivsum2  26792  vmalogdivsum  26793  2vmadivsumlem  26794  log2sumbnd  26798  selberglem1  26799  selberglem2  26800  selberglem3  26801  selberg  26802  selbergb  26803  selberg2lem  26804  selberg2  26805  selberg2b  26806  chpdifbndlem1  26807  logdivbnd  26810  selberg3lem1  26811  selberg3lem2  26812  selberg3  26813  selberg4lem1  26814  selberg4  26815  pntrsumo1  26819  pntrsumbnd  26820  pntrsumbnd2  26821  selbergr  26822  selberg3r  26823  selberg4r  26824  selberg34r  26825  pntsf  26827  pntsval2  26830  pntrlog2bndlem1  26831  pntrlog2bndlem2  26832  pntrlog2bndlem3  26833  pntrlog2bndlem4  26834  pntrlog2bndlem5  26835  pntrlog2bndlem6  26837  pntrlog2bnd  26838  pntpbnd2  26841  pntlemf  26859  pntlemk  26860  pntlemo  26861  eucrct2eupth  28897  dipcl  29362  dipcn  29370  prmdvdsbc  31415  freshmansdream  31769  esumpcvgval  32342  esumpmono  32343  esumcvg  32350  esumcvgsum  32352  eulerpartlemgc  32627  ballotlemfc0  32757  ballotlemfcc  32758  ballotlemic  32771  ballotlem1c  32772  ballotlemsel1i  32777  ballotlemsf1o  32778  erdszelem4  33453  erdszelem8  33457  erdsze2lem2  33463  cvmliftlem2  33545  cvmliftlem6  33549  cvmliftlem8  33551  cvmliftlem9  33552  cvmliftlem10  33553  bcprod  33994  faclim  34002  poimirlem6  35937  poimirlem7  35938  poimirlem8  35939  poimirlem9  35940  poimirlem11  35942  poimirlem13  35944  poimirlem14  35945  poimirlem15  35946  poimirlem16  35947  poimirlem17  35948  poimirlem18  35949  poimirlem22  35953  poimirlem32  35963  mblfinlem2  35969  aks4d1p1p2  40381  aks4d1p1p4  40382  aks4d1p1  40387  aks4d1p3  40389  aks4d1p4  40390  aks4d1p5  40391  aks4d1p6  40392  aks4d1p7d1  40393  aks4d1p7  40394  aks4d1p8  40398  aks4d1p9  40399  sticksstones1  40408  sticksstones2  40409  sticksstones3  40410  sticksstones6  40413  sticksstones7  40414  sticksstones10  40417  sticksstones12a  40419  sticksstones12  40420  metakunt1  40431  metakunt2  40432  metakunt6  40436  metakunt7  40437  metakunt8  40438  metakunt9  40439  metakunt11  40441  metakunt15  40445  metakunt16  40446  metakunt21  40451  metakunt22  40452  metakunt27  40457  metakunt29  40459  metakunt30  40460  eldioph3b  40898  diophin  40905  diophun  40906  eldiophss  40907  irrapxlem4  40958  sumnnodd  43557  stoweidlem34  43961  wallispilem4  43995  wallispi  43997  wallispi2lem1  43998  wallispi2  44000  stirlinglem5  44005  stirlinglem7  44007  stirlinglem10  44010  stirlinglem12  44012  fourierdlem83  44116  fourierdlem112  44145  caratheodorylem2  44452  hoidmvlelem2  44521  hoidmvlelem3  44522  altgsumbcALT  46105  nn0sumshdiglemA  46381  nn0sumshdiglemB  46382