Theorem elfznn 13498

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  (class class class)co 7360  1c1 11030   ≤ cle 11171  ℕcn 12165  ℤcz 12515  ...cfz 13452

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-z 12516  df-uz 12780  df-fz 13453

This theorem is referenced by:  elfz1end  13499  fz1ssnn  13500  bcm1k  14268  bcpasc  14274  seqcoll  14417  pfxfv0  14645  pfxfvlsw  14648  isercolllem2  15619  isercolllem3  15620  isercoll  15621  sumeq2ii  15646  summolem3  15667  summolem2a  15668  fsum  15673  sumz  15675  fsumconst  15743  o1fsum  15767  binomlem  15785  incexc2  15794  climcndslem1  15805  climcndslem2  15806  climcnds  15807  harmonic  15815  arisum2  15817  trireciplem  15818  pwdif  15824  geo2sum  15829  geo2lim  15831  prodeq2ii  15867  prodmolem3  15889  prodmolem2a  15890  fprod  15897  prod1  15900  fprodfac  15929  fprodconst  15934  risefallfac  15980  risefacfac  15991  fallfacval4  15999  bpolydiflem  16010  rpnnen2lem10  16181  fzm1ndvds  16282  pwp1fsum  16351  lcmflefac  16608  prmdvdsbc  16687  phicl  16730  prmdivdiv  16748  pcfac  16861  pcbc  16862  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  prmrec  16884  4sqlem13  16919  vdwlem2  16944  vdwlem3  16945  vdwlem10  16952  vdwlem12  16954  prmocl  16996  prmop1  17000  fvprmselelfz  17006  fvprmselgcd1  17007  prmolefac  17008  prmodvdslcmf  17009  prmgapprmo  17024  mulgnngsum  19046  mulgnnsubcl  19053  mulgnn0z  19068  mulgnndir  19070  oddvdsnn0  19510  odnncl  19511  gexcl3  19553  efgsres  19704  mulgnn0di  19791  gsumconst  19900  srgbinomlem4  20201  freshmansdream  21564  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmadugsumlemF  22851  lebnumii  24943  ovollb2lem  25465  ovolunlem1a  25473  ovoliunlem1  25479  ovoliunlem2  25480  ovoliun2  25483  ovolscalem1  25490  ovolicc2lem4  25497  voliunlem1  25527  volsup  25533  ioombl1lem4  25538  uniioovol  25556  uniioombllem3a  25561  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  uniioombllem6  25565  dvply1  26260  aaliou3lem5  26324  aaliou3lem6  26325  dvtaylp  26347  taylthlem2  26351  taylthlem2OLD  26352  pserdvlem2  26406  logfac  26578  atantayl  26914  birthdaylem2  26929  emcllem1  26973  emcllem2  26974  emcllem3  26975  emcllem5  26977  emcllem7  26979  harmoniclbnd  26986  harmonicubnd  26987  harmonicbnd4  26988  fsumharmonic  26989  lgamcvg2  27032  gamcvg2lem  27036  wilthlem1  27045  wilthlem2  27046  ftalem5  27054  basellem1  27058  basellem8  27065  chpf  27100  efchpcl  27102  chpp1  27132  chpwordi  27134  prmorcht  27155  dvdsflf1o  27164  dvdsflsumcom  27165  chtlepsi  27183  fsumvma2  27191  pclogsum  27192  vmasum  27193  logfac2  27194  chpval2  27195  chpchtsum  27196  logfaclbnd  27199  logexprlim  27202  logfacrlim2  27203  pcbcctr  27253  bposlem1  27261  bposlem2  27262  lgscllem  27281  lgsval2lem  27284  lgsval4a  27296  lgsneg  27298  lgsdir  27309  lgsdilem2  27310  lgsdi  27311  lgsne0  27312  lgsqrlem2  27324  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgseisen  27356  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  2lgslem1a1  27366  chebbnd1lem1  27446  vmadivsum  27459  vmadivsumb  27460  rplogsumlem2  27462  dchrisum0lem1a  27463  rpvmasumlem  27464  dchrisumlem2  27467  dchrmusum2  27471  dchrvmasumlem1  27472  dchrvmasum2lem  27473  dchrvmasum2if  27474  dchrvmasumlem2  27475  dchrvmasumlem3  27476  dchrvmasumiflem1  27478  dchrvmasumiflem2  27479  dchrisum0fno1  27488  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem1b  27492  dchrisum0lem1  27493  dchrisum0lem2a  27494  dchrisum0lem2  27495  dchrisum0lem3  27496  dchrisum0  27497  dchrmusumlem  27499  dchrvmasumlem  27500  rplogsum  27504  mudivsum  27507  mulogsumlem  27508  mulogsum  27509  mulog2sumlem1  27511  mulog2sumlem2  27512  mulog2sumlem3  27513  vmalogdivsum2  27515  vmalogdivsum  27516  2vmadivsumlem  27517  log2sumbnd  27521  selberglem1  27522  selberglem2  27523  selberglem3  27524  selberg  27525  selbergb  27526  selberg2lem  27527  selberg2  27528  selberg2b  27529  chpdifbndlem1  27530  logdivbnd  27533  selberg3lem1  27534  selberg3lem2  27535  selberg3  27536  selberg4lem1  27537  selberg4  27538  pntrsumo1  27542  pntrsumbnd  27543  pntrsumbnd2  27544  selbergr  27545  selberg3r  27546  selberg4r  27547  selberg34r  27548  pntsf  27550  pntsval2  27553  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntrlog2bnd  27561  pntpbnd2  27564  pntlemf  27582  pntlemk  27583  pntlemo  27584  eucrct2eupth  30330  dipcl  30798  dipcn  30806  gsummptp1  33133  gsummulsubdishift1  33144  esplyind  33734  esumpcvgval  34238  esumpmono  34239  esumcvg  34246  esumcvgsum  34248  eulerpartlemgc  34522  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemic  34667  ballotlem1c  34668  ballotlemsel1i  34673  ballotlemsf1o  34674  erdszelem4  35392  erdszelem8  35396  erdsze2lem2  35402  cvmliftlem2  35484  cvmliftlem6  35488  cvmliftlem8  35490  cvmliftlem9  35491  cvmliftlem10  35492  bcprod  35936  faclim  35944  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem9  37964  poimirlem11  37966  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem22  37977  poimirlem32  37987  mblfinlem2  37993  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1  42529  aks4d1p3  42531  aks4d1p4  42532  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  aks4d1p9  42541  primrootlekpowne0  42558  hashscontpow1  42574  hashscontpow  42575  sticksstones1  42599  sticksstones2  42600  sticksstones3  42601  sticksstones6  42604  sticksstones7  42605  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  oddnumth  42757  nicomachus  42758  sumcubes  42759  eldioph3b  43211  diophin  43218  diophun  43219  eldiophss  43220  irrapxlem4  43271  sumnnodd  46078  stoweidlem34  46480  wallispilem4  46514  wallispi  46516  wallispi2lem1  46517  wallispi2  46519  stirlinglem5  46524  stirlinglem7  46526  stirlinglem10  46529  stirlinglem12  46531  fourierdlem83  46635  fourierdlem112  46664  caratheodorylem2  46973  hoidmvlelem2  47042  hoidmvlelem3  47043  elfz2nn  47782  stgrusgra  48447  isubgr3stgrlem7  48460  altgsumbcALT  48841  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108