Theorem elfznn 13467

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  (class class class)co 7356  1c1 11025   ≤ cle 11165  ℕcn 12143  ℤcz 12486  ...cfz 13421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-z 12487  df-uz 12750  df-fz 13422

This theorem is referenced by:  elfz1end  13468  fz1ssnn  13469  bcm1k  14236  bcpasc  14242  seqcoll  14385  pfxfv0  14613  pfxfvlsw  14616  isercolllem2  15587  isercolllem3  15588  isercoll  15589  sumeq2ii  15614  summolem3  15635  summolem2a  15636  fsum  15641  sumz  15643  fsumconst  15711  o1fsum  15734  binomlem  15750  incexc2  15759  climcndslem1  15770  climcndslem2  15771  climcnds  15772  harmonic  15780  arisum2  15782  trireciplem  15783  pwdif  15789  geo2sum  15794  geo2lim  15796  prodeq2ii  15832  prodmolem3  15854  prodmolem2a  15855  fprod  15862  prod1  15865  fprodfac  15894  fprodconst  15899  risefallfac  15945  risefacfac  15956  fallfacval4  15964  bpolydiflem  15975  rpnnen2lem10  16146  fzm1ndvds  16247  pwp1fsum  16316  lcmflefac  16573  prmdvdsbc  16651  phicl  16694  prmdivdiv  16712  pcfac  16825  pcbc  16826  prmreclem2  16843  prmreclem3  16844  prmreclem4  16845  prmreclem5  16846  prmreclem6  16847  prmrec  16848  4sqlem13  16883  vdwlem2  16908  vdwlem3  16909  vdwlem10  16916  vdwlem12  16918  prmocl  16960  prmop1  16964  fvprmselelfz  16970  fvprmselgcd1  16971  prmolefac  16972  prmodvdslcmf  16973  prmgapprmo  16988  mulgnngsum  19007  mulgnnsubcl  19014  mulgnn0z  19029  mulgnndir  19031  oddvdsnn0  19471  odnncl  19472  gexcl3  19514  efgsres  19665  mulgnn0di  19752  gsumconst  19861  srgbinomlem4  20162  freshmansdream  21527  chfacfscmulgsum  22802  chfacfpmmulgsum  22806  chfacfpmmulgsum2  22807  cayhamlem1  22808  cpmadugsumlemF  22818  lebnumii  24919  ovollb2lem  25443  ovolunlem1a  25451  ovoliunlem1  25457  ovoliunlem2  25458  ovoliun2  25461  ovolscalem1  25468  ovolicc2lem4  25475  voliunlem1  25505  volsup  25511  ioombl1lem4  25516  uniioovol  25534  uniioombllem3a  25539  uniioombllem3  25540  uniioombllem4  25541  uniioombllem5  25542  uniioombllem6  25543  dvply1  26245  aaliou3lem5  26309  aaliou3lem6  26310  dvtaylp  26332  taylthlem2  26336  taylthlem2OLD  26337  pserdvlem2  26392  logfac  26564  atantayl  26901  birthdaylem2  26916  emcllem1  26960  emcllem2  26961  emcllem3  26962  emcllem5  26964  emcllem7  26966  harmoniclbnd  26973  harmonicubnd  26974  harmonicbnd4  26975  fsumharmonic  26976  lgamcvg2  27019  gamcvg2lem  27023  wilthlem1  27032  wilthlem2  27033  ftalem5  27041  basellem1  27045  basellem8  27052  chpf  27087  efchpcl  27089  chpp1  27119  chpwordi  27121  prmorcht  27142  dvdsflf1o  27151  dvdsflsumcom  27152  chtlepsi  27171  fsumvma2  27179  pclogsum  27180  vmasum  27181  logfac2  27182  chpval2  27183  chpchtsum  27184  logfaclbnd  27187  logexprlim  27190  logfacrlim2  27191  pcbcctr  27241  bposlem1  27249  bposlem2  27250  lgscllem  27269  lgsval2lem  27272  lgsval4a  27284  lgsneg  27286  lgsdir  27297  lgsdilem2  27298  lgsdi  27299  lgsne0  27300  lgsqrlem2  27312  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgseisenlem4  27343  lgseisen  27344  lgsquadlem1  27345  lgsquadlem2  27346  lgsquadlem3  27347  2lgslem1a1  27354  chebbnd1lem1  27434  vmadivsum  27447  vmadivsumb  27448  rplogsumlem2  27450  dchrisum0lem1a  27451  rpvmasumlem  27452  dchrisumlem2  27455  dchrmusum2  27459  dchrvmasumlem1  27460  dchrvmasum2lem  27461  dchrvmasum2if  27462  dchrvmasumlem2  27463  dchrvmasumlem3  27464  dchrvmasumiflem1  27466  dchrvmasumiflem2  27467  dchrisum0fno1  27476  rpvmasum2  27477  dchrisum0re  27478  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2a  27482  dchrisum0lem2  27483  dchrisum0lem3  27484  dchrisum0  27485  dchrmusumlem  27487  dchrvmasumlem  27488  rplogsum  27492  mudivsum  27495  mulogsumlem  27496  mulogsum  27497  mulog2sumlem1  27499  mulog2sumlem2  27500  mulog2sumlem3  27501  vmalogdivsum2  27503  vmalogdivsum  27504  2vmadivsumlem  27505  log2sumbnd  27509  selberglem1  27510  selberglem2  27511  selberglem3  27512  selberg  27513  selbergb  27514  selberg2lem  27515  selberg2  27516  selberg2b  27517  chpdifbndlem1  27518  logdivbnd  27521  selberg3lem1  27522  selberg3lem2  27523  selberg3  27524  selberg4lem1  27525  selberg4  27526  pntrsumo1  27530  pntrsumbnd  27531  pntrsumbnd2  27532  selbergr  27533  selberg3r  27534  selberg4r  27535  selberg34r  27536  pntsf  27538  pntsval2  27541  pntrlog2bndlem1  27542  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntpbnd2  27552  pntlemf  27570  pntlemk  27571  pntlemo  27572  eucrct2eupth  30269  dipcl  30736  dipcn  30744  gsummptp1  33089  gsummulsubdishift1  33100  esplyind  33680  esumpcvgval  34184  esumpmono  34185  esumcvg  34192  esumcvgsum  34194  eulerpartlemgc  34468  ballotlemfc0  34599  ballotlemfcc  34600  ballotlemic  34613  ballotlem1c  34614  ballotlemsel1i  34619  ballotlemsf1o  34620  erdszelem4  35337  erdszelem8  35341  erdsze2lem2  35347  cvmliftlem2  35429  cvmliftlem6  35433  cvmliftlem8  35435  cvmliftlem9  35436  cvmliftlem10  35437  bcprod  35881  faclim  35889  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem9  37769  poimirlem11  37771  poimirlem13  37773  poimirlem14  37774  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem18  37778  poimirlem22  37782  poimirlem32  37792  mblfinlem2  37798  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1  42269  aks4d1p3  42271  aks4d1p4  42272  aks4d1p5  42273  aks4d1p6  42274  aks4d1p7d1  42275  aks4d1p7  42276  aks4d1p8  42280  aks4d1p9  42281  primrootlekpowne0  42298  hashscontpow1  42314  hashscontpow  42315  sticksstones1  42339  sticksstones2  42340  sticksstones3  42341  sticksstones6  42344  sticksstones7  42345  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  oddnumth  42508  nicomachus  42509  sumcubes  42510  eldioph3b  42949  diophin  42956  diophun  42957  eldiophss  42958  irrapxlem4  43009  sumnnodd  45818  stoweidlem34  46220  wallispilem4  46254  wallispi  46256  wallispi2lem1  46257  wallispi2  46259  stirlinglem5  46264  stirlinglem7  46266  stirlinglem10  46269  stirlinglem12  46271  fourierdlem83  46375  fourierdlem112  46404  caratheodorylem2  46713  hoidmvlelem2  46782  hoidmvlelem3  46783  stgrusgra  48147  isubgr3stgrlem7  48160  altgsumbcALT  48541  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808