Theorem elfznn 12937

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 12909	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 12911	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 12009	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 585	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5066  (class class class)co 7156  1c1 10538   ≤ cle 10676  ℕcn 11638  ℤcz 11982  ...cfz 12893

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-z 11983  df-uz 12245  df-fz 12894

This theorem is referenced by:  elfz1end  12938  fz1ssnn  12939  bcm1k  13676  bcpasc  13682  seqcoll  13823  pfxfv0  14054  pfxfvlsw  14057  isercolllem2  15022  isercolllem3  15023  isercoll  15024  sumeq2ii  15050  summolem3  15071  summolem2a  15072  fsum  15077  sumz  15079  fsumconst  15145  o1fsum  15168  binomlem  15184  incexc2  15193  climcndslem1  15204  climcndslem2  15205  climcnds  15206  harmonic  15214  arisum2  15216  trireciplem  15217  pwdif  15223  geo2sum  15229  geo2lim  15231  prodeq2ii  15267  prodmolem3  15287  prodmolem2a  15288  fprod  15295  prod1  15298  fprodfac  15327  fprodconst  15332  risefallfac  15378  risefacfac  15389  fallfacval4  15397  bpolydiflem  15408  rpnnen2lem10  15576  fzm1ndvds  15672  pwp1fsum  15742  lcmflefac  15992  phicl  16106  prmdivdiv  16124  pcfac  16235  pcbc  16236  prmreclem2  16253  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  prmreclem6  16257  prmrec  16258  4sqlem13  16293  vdwlem2  16318  vdwlem3  16319  vdwlem10  16326  vdwlem12  16328  prmocl  16370  prmop1  16374  fvprmselelfz  16380  fvprmselgcd1  16381  prmolefac  16382  prmodvdslcmf  16383  prmgapprmo  16398  mulgnngsum  18233  mulgnnsubcl  18240  mulgnn0z  18254  mulgnndir  18256  oddvdsnn0  18672  odnncl  18673  gexcl3  18712  efgsres  18864  mulgnn0di  18946  gsumconst  19054  srgbinomlem4  19293  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmadugsumlemF  21484  lebnumii  23570  ovollb2lem  24089  ovolunlem1a  24097  ovoliunlem1  24103  ovoliunlem2  24104  ovoliun2  24107  ovolscalem1  24114  ovolicc2lem4  24121  voliunlem1  24151  volsup  24157  ioombl1lem4  24162  uniioovol  24180  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombllem6  24189  dvply1  24873  aaliou3lem5  24936  aaliou3lem6  24937  dvtaylp  24958  taylthlem2  24962  pserdvlem2  25016  logfac  25184  atantayl  25515  birthdaylem2  25530  emcllem1  25573  emcllem2  25574  emcllem3  25575  emcllem5  25577  emcllem7  25579  harmoniclbnd  25586  harmonicubnd  25587  harmonicbnd4  25588  fsumharmonic  25589  lgamcvg2  25632  gamcvg2lem  25636  wilthlem1  25645  wilthlem2  25646  ftalem5  25654  basellem1  25658  basellem8  25665  chpf  25700  efchpcl  25702  chpp1  25732  chpwordi  25734  prmorcht  25755  dvdsflf1o  25764  dvdsflsumcom  25765  chtlepsi  25782  fsumvma2  25790  pclogsum  25791  vmasum  25792  logfac2  25793  chpval2  25794  chpchtsum  25795  logfaclbnd  25798  logexprlim  25801  logfacrlim2  25802  pcbcctr  25852  bposlem1  25860  bposlem2  25861  lgscllem  25880  lgsval2lem  25883  lgsval4a  25895  lgsneg  25897  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  lgsqrlem2  25923  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  2lgslem1a1  25965  chebbnd1lem1  26045  vmadivsum  26058  vmadivsumb  26059  rplogsumlem2  26061  dchrisum0lem1a  26062  rpvmasumlem  26063  dchrisumlem2  26066  dchrmusum2  26070  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrvmasum2if  26073  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  dchrvmasumiflem2  26078  dchrisum0fno1  26087  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0lem3  26095  dchrisum0  26096  dchrmusumlem  26098  dchrvmasumlem  26099  rplogsum  26103  mudivsum  26106  mulogsumlem  26107  mulogsum  26108  mulog2sumlem1  26110  mulog2sumlem2  26111  mulog2sumlem3  26112  vmalogdivsum2  26114  vmalogdivsum  26115  2vmadivsumlem  26116  log2sumbnd  26120  selberglem1  26121  selberglem2  26122  selberglem3  26123  selberg  26124  selbergb  26125  selberg2lem  26126  selberg2  26127  selberg2b  26128  chpdifbndlem1  26129  logdivbnd  26132  selberg3lem1  26133  selberg3lem2  26134  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrsumo1  26141  pntrsumbnd  26142  pntrsumbnd2  26143  selbergr  26144  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntsf  26149  pntsval2  26152  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd2  26163  pntlemf  26181  pntlemk  26182  pntlemo  26183  eucrct2eupth  28024  dipcl  28489  dipcn  28497  prmdvdsbc  30532  freshmansdream  30859  esumpcvgval  31337  esumpmono  31338  esumcvg  31345  esumcvgsum  31347  eulerpartlemgc  31620  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemimin  31763  ballotlemic  31764  ballotlem1c  31765  ballotlemsel1i  31770  ballotlemsf1o  31771  erdszelem4  32441  erdszelem8  32445  erdsze2lem2  32451  cvmliftlem2  32533  cvmliftlem6  32537  cvmliftlem8  32539  cvmliftlem9  32540  cvmliftlem10  32541  bcprod  32970  faclim  32978  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem9  34916  poimirlem11  34918  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem22  34929  poimirlem32  34939  mblfinlem2  34945  eldioph3b  39411  diophin  39418  diophun  39419  eldiophss  39420  irrapxlem4  39471  sumnnodd  41960  stoweidlem34  42368  wallispilem4  42402  wallispi  42404  wallispi2lem1  42405  wallispi2  42407  stirlinglem5  42412  stirlinglem7  42414  stirlinglem10  42417  stirlinglem12  42419  fourierdlem83  42523  fourierdlem112  42552  caratheodorylem2  42858  hoidmvlelem2  42927  hoidmvlelem3  42928  altgsumbcALT  44450  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729