Theorem elfznn 12755

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 12727	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 12729	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 11824	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 575	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2050   class class class wbr 4930  (class class class)co 6978  1c1 10338   ≤ cle 10477  ℕcn 11441  ℤcz 11796  ...cfz 12711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-cnex 10393  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413  ax-pre-mulgt0 10414

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-iun 4795  df-br 4931  df-opab 4993  df-mpt 5010  df-tr 5032  df-id 5313  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-we 5369  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-pred 5988  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-om 7399  df-1st 7503  df-2nd 7504  df-wrecs 7752  df-recs 7814  df-rdg 7852  df-er 8091  df-en 8309  df-dom 8310  df-sdom 8311  df-pnf 10478  df-mnf 10479  df-xr 10480  df-ltxr 10481  df-le 10482  df-sub 10674  df-neg 10675  df-nn 11442  df-z 11797  df-uz 12062  df-fz 12712

This theorem is referenced by:  elfz1end  12756  fz1ssnn  12757  bcm1k  13493  bcpasc  13499  seqcoll  13638  swrd0fv0OLD  13835  swrd0fvlswOLD  13838  pfxfv0  13877  pfxfvlsw  13880  isercolllem2  14886  isercolllem3  14887  isercoll  14888  sumeq2ii  14913  summolem3  14934  summolem2a  14935  fsum  14940  sumz  14942  fsumconst  15008  o1fsum  15031  binomlem  15047  incexc2  15056  climcndslem1  15067  climcndslem2  15068  climcnds  15069  harmonic  15077  arisum2  15079  trireciplem  15080  pwdif  15086  geo2sum  15092  geo2lim  15094  prodeq2ii  15130  prodmolem3  15150  prodmolem2a  15151  fprod  15158  prod1  15161  fprodfac  15190  fprodconst  15195  risefallfac  15241  risefacfac  15252  fallfacval4  15260  bpolydiflem  15271  rpnnen2lem10  15439  fzm1ndvds  15535  pwp1fsum  15605  lcmflefac  15851  phicl  15965  prmdivdiv  15983  pcfac  16094  pcbc  16095  prmreclem2  16112  prmreclem3  16113  prmreclem4  16114  prmreclem5  16115  prmreclem6  16116  prmrec  16117  4sqlem13  16152  vdwlem2  16177  vdwlem3  16178  vdwlem10  16185  vdwlem12  16187  prmocl  16229  prmop1  16233  fvprmselelfz  16239  fvprmselgcd1  16240  prmolefac  16241  prmodvdslcmf  16242  prmgapprmo  16257  mulgnnsubcl  18028  mulgnn0z  18041  mulgnndir  18043  oddvdsnn0  18437  odnncl  18438  gexcl3  18476  efgsres  18625  efgsresOLD  18626  mulgnn0di  18707  gsumconst  18810  srgbinomlem4  19019  chfacfscmulgsum  21175  chfacfpmmulgsum  21179  chfacfpmmulgsum2  21180  cayhamlem1  21181  cpmadugsumlemF  21191  lebnumii  23276  ovollb2lem  23795  ovolunlem1a  23803  ovoliunlem1  23809  ovoliunlem2  23810  ovoliun2  23813  ovolscalem1  23820  ovolicc2lem4  23827  voliunlem1  23857  volsup  23863  ioombl1lem4  23868  uniioovol  23886  uniioombllem3a  23891  uniioombllem3  23892  uniioombllem4  23893  uniioombllem5  23894  uniioombllem6  23895  dvply1  24579  aaliou3lem5  24642  aaliou3lem6  24643  dvtaylp  24664  taylthlem2  24668  pserdvlem2  24722  logfac  24888  atantayl  25219  birthdaylem2  25235  emcllem1  25278  emcllem2  25279  emcllem3  25280  emcllem5  25282  emcllem7  25284  harmoniclbnd  25291  harmonicubnd  25292  harmonicbnd4  25293  fsumharmonic  25294  lgamcvg2  25337  gamcvg2lem  25341  wilthlem1  25350  wilthlem2  25351  ftalem5  25359  basellem1  25363  basellem8  25370  chpf  25405  efchpcl  25407  chpp1  25437  chpwordi  25439  prmorcht  25460  dvdsflf1o  25469  dvdsflsumcom  25470  chtlepsi  25487  fsumvma2  25495  pclogsum  25496  vmasum  25497  logfac2  25498  chpval2  25499  chpchtsum  25500  logfaclbnd  25503  logexprlim  25506  logfacrlim2  25507  pcbcctr  25557  bposlem1  25565  bposlem2  25566  lgscllem  25585  lgsval2lem  25588  lgsval4a  25600  lgsneg  25602  lgsdir  25613  lgsdilem2  25614  lgsdi  25615  lgsne0  25616  lgsqrlem2  25628  lgseisenlem1  25656  lgseisenlem2  25657  lgseisenlem3  25658  lgseisenlem4  25659  lgseisen  25660  lgsquadlem1  25661  lgsquadlem2  25662  lgsquadlem3  25663  2lgslem1a1  25670  chebbnd1lem1  25750  vmadivsum  25763  vmadivsumb  25764  rplogsumlem2  25766  dchrisum0lem1a  25767  rpvmasumlem  25768  dchrisumlem2  25771  dchrmusum2  25775  dchrvmasumlem1  25776  dchrvmasum2lem  25777  dchrvmasum2if  25778  dchrvmasumlem2  25779  dchrvmasumlem3  25780  dchrvmasumiflem1  25782  dchrvmasumiflem2  25783  dchrisum0fno1  25792  rpvmasum2  25793  dchrisum0re  25794  dchrisum0lem1b  25796  dchrisum0lem1  25797  dchrisum0lem2a  25798  dchrisum0lem2  25799  dchrisum0lem3  25800  dchrisum0  25801  dchrmusumlem  25803  dchrvmasumlem  25804  rplogsum  25808  mudivsum  25811  mulogsumlem  25812  mulogsum  25813  mulog2sumlem1  25815  mulog2sumlem2  25816  mulog2sumlem3  25817  vmalogdivsum2  25819  vmalogdivsum  25820  2vmadivsumlem  25821  log2sumbnd  25825  selberglem1  25826  selberglem2  25827  selberglem3  25828  selberg  25829  selbergb  25830  selberg2lem  25831  selberg2  25832  selberg2b  25833  chpdifbndlem1  25834  logdivbnd  25837  selberg3lem1  25838  selberg3lem2  25839  selberg3  25840  selberg4lem1  25841  selberg4  25842  pntrsumo1  25846  pntrsumbnd  25847  pntrsumbnd2  25848  selbergr  25849  selberg3r  25850  selberg4r  25851  selberg34r  25852  pntsf  25854  pntsval2  25857  pntrlog2bndlem1  25858  pntrlog2bndlem2  25859  pntrlog2bndlem3  25860  pntrlog2bndlem4  25861  pntrlog2bndlem5  25862  pntrlog2bndlem6  25864  pntrlog2bnd  25865  pntpbnd2  25868  pntlemf  25886  pntlemk  25887  pntlemo  25888  eucrct2eupthOLD  27779  eucrct2eupth  27780  dipcl  28269  dipcn  28277  prmdvdsbc  30281  freshmansdream  30538  esumpcvgval  30981  esumpmono  30982  esumcvg  30989  esumcvgsum  30991  eulerpartlemgc  31265  ballotlemfc0  31396  ballotlemfcc  31397  ballotlemimin  31409  ballotlemic  31410  ballotlem1c  31411  ballotlemsel1i  31416  ballotlemsf1o  31417  erdszelem4  32026  erdszelem8  32030  erdsze2lem2  32036  cvmliftlem2  32118  cvmliftlem6  32122  cvmliftlem8  32124  cvmliftlem9  32125  cvmliftlem10  32126  bcprod  32490  faclim  32498  poimirlem6  34339  poimirlem7  34340  poimirlem8  34341  poimirlem9  34342  poimirlem11  34344  poimirlem13  34346  poimirlem14  34347  poimirlem15  34348  poimirlem16  34349  poimirlem17  34350  poimirlem18  34351  poimirlem22  34355  poimirlem32  34365  mblfinlem2  34371  eldioph3b  38757  diophin  38765  diophun  38766  eldiophss  38767  irrapxlem4  38818  sumnnodd  41343  stoweidlem34  41751  wallispilem4  41785  wallispi  41787  wallispi2lem1  41788  wallispi2  41790  stirlinglem5  41795  stirlinglem7  41797  stirlinglem10  41800  stirlinglem12  41802  fourierdlem83  41906  fourierdlem112  41935  caratheodorylem2  42241  hoidmvlelem2  42310  hoidmvlelem3  42311  altgsumbcALT  43766  nn0sumshdiglemA  44048  nn0sumshdiglemB  44049