Theorem elfznn 13692

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  (class class class)co 7422  1c1 11206   ≤ cle 11349  ℕcn 12340  ℤcz 12698  ...cfz 13644

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7753  ax-cnex 11261  ax-resscn 11262  ax-1cn 11263  ax-icn 11264  ax-addcl 11265  ax-addrcl 11266  ax-mulcl 11267  ax-mulrcl 11268  ax-mulcom 11269  ax-addass 11270  ax-mulass 11271  ax-distr 11272  ax-i2m1 11273  ax-1ne0 11274  ax-1rid 11275  ax-rnegex 11276  ax-rrecex 11277  ax-cnre 11278  ax-pre-lttri 11279  ax-pre-lttrn 11280  ax-pre-ltadd 11281  ax-pre-mulgt0 11282

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7379  df-ov 7425  df-oprab 7426  df-mpo 7427  df-om 7880  df-1st 8003  df-2nd 8004  df-frecs 8304  df-wrecs 8335  df-recs 8384  df-rdg 8423  df-er 8722  df-en 8979  df-dom 8980  df-sdom 8981  df-pnf 11350  df-mnf 11351  df-xr 11352  df-ltxr 11353  df-le 11354  df-sub 11548  df-neg 11549  df-nn 12341  df-z 12699  df-uz 12971  df-fz 13645

This theorem is used by:  elfz1end  13693  fz1ssnn  13694  bcm1k  14464  bcpasc  14470  seqcoll  14614  pfxfv0  14847  pfxfvlsw  14850  isercolllem2  15840  isercolllem3  15841  isercoll  15842  sumeq2ii  15867  summolem3  15887  summolem2a  15888  fsum  15893  sumz  15895  fsumconst  15963  o1fsum  15987  binomlem  16005  incexc2  16014  climcndslem1  16025  climcndslem2  16026  climcnds  16027  harmonic  16035  arisum2  16037  trireciplem  16038  pwdif  16044  geo2sum  16049  geo2lim  16051  prodeq2ii  16087  prodmolem3  16107  prodmolem2a  16108  fprod  16115  prod1  16118  fprodfac  16147  fprodconst  16152  risefallfac  16198  risefacfac  16208  fallfacval4  16216  bpolydiflem  16227  rpnnen2lem10  16398  fzm1ndvds  16499  pwp1fsum  16568  lcmflefac  16830  prmdvdsbc  16909  phicl  16953  prmdivdiv  16971  pcfac  17084  pcbc  17085  prmreclem2  17102  prmreclem3  17103  prmreclem4  17104  prmreclem5  17105  prmreclem6  17106  prmrec  17107  4sqlem13  17142  vdwlem2  17167  vdwlem3  17168  vdwlem10  17175  vdwlem12  17177  prmocl  17219  prmop1  17223  fvprmselelfz  17229  fvprmselgcd1  17230  prmolefac  17231  prmodvdslcmf  17232  prmgapprmo  17247  mulgnngsum  19296  mulgnnsubcl  19303  mulgnn0z  19318  mulgnndir  19320  oddvdsnn0  19765  odnncl  19766  gexcl3  19808  efgsres  19959  mulgnn0di  20046  gsumconst  20155  srgbinomlem4  20462  freshmansdream  21887  chfacfscmulgsum  23185  chfacfpmmulgsum  23189  chfacfpmmulgsum2  23190  cayhamlem1  23191  cpmadugsumlemF  23201  lebnumii  25294  ovollb2lem  25816  ovolunlem1a  25824  ovoliunlem1  25830  ovoliunlem2  25831  ovoliun2  25834  ovolscalem1  25841  ovolicc2lem4  25848  voliunlem1  25878  volsup  25884  ioombl1lem4  25889  uniioovol  25907  uniioombllem3a  25912  uniioombllem3  25913  uniioombllem4  25914  uniioombllem5  25915  uniioombllem6  25916  dvply1  26612  aaliou3lem5  26681  aaliou3lem6  26682  dvtaylp  26704  taylthlem2  26708  pserdvlem2  26762  logfac  26936  atantayl  27272  birthdaylem2  27287  emcllem1  27330  emcllem2  27331  emcllem3  27332  emcllem5  27334  emcllem7  27336  harmoniclbnd  27343  harmonicubnd  27344  harmonicbnd4  27345  fsumharmonic  27346  lgamcvg2  27389  gamcvg2lem  27393  wilthlem1  27402  wilthlem2  27403  ftalem5  27411  basellem1  27415  basellem8  27422  chpf  27457  efchpcl  27459  chpp1  27489  chpwordi  27491  prmorcht  27512  dvdsflf1o  27521  dvdsflsumcom  27522  chtlepsi  27540  fsumvma2  27548  pclogsum  27549  vmasum  27550  logfac2  27551  chpval2  27552  chpchtsum  27553  logfaclbnd  27556  logexprlim  27559  logfacrlim2  27560  pcbcctr  27610  bposlem1  27618  bposlem2  27619  lgscllem  27638  lgsval2lem  27641  lgsval4a  27653  lgsneg  27655  lgsdir  27666  lgsdilem2  27667  lgsdi  27668  lgsne0  27669  lgsqrlem2  27681  lgseisenlem1  27709  lgseisenlem2  27710  lgseisenlem3  27711  lgseisenlem4  27712  lgseisen  27713  lgsquadlem1  27714  lgsquadlem2  27715  lgsquadlem3  27716  2lgslem1a1  27723  chebbnd1lem1  27803  vmadivsum  27816  vmadivsumb  27817  rplogsumlem2  27819  dchrisum0lem1a  27820  rpvmasumlem  27821  dchrisumlem2  27824  dchrmusum2  27828  dchrvmasumlem1  27829  dchrvmasum2lem  27830  dchrvmasum2if  27831  dchrvmasumlem2  27832  dchrvmasumlem3  27833  dchrvmasumiflem1  27835  dchrvmasumiflem2  27836  dchrisum0fno1  27845  rpvmasum2  27846  dchrisum0re  27847  dchrisum0lem1b  27849  dchrisum0lem1  27850  dchrisum0lem2a  27851  dchrisum0lem2  27852  dchrisum0lem3  27853  dchrisum0  27854  dchrmusumlem  27856  dchrvmasumlem  27857  rplogsum  27861  mudivsum  27864  mulogsumlem  27865  mulogsum  27866  mulog2sumlem1  27868  mulog2sumlem2  27869  mulog2sumlem3  27870  vmalogdivsum2  27872  vmalogdivsum  27873  2vmadivsumlem  27874  log2sumbnd  27878  selberglem1  27879  selberglem2  27880  selberglem3  27881  selberg  27882  selbergb  27883  selberg2lem  27884  selberg2  27885  selberg2b  27886  chpdifbndlem1  27887  logdivbnd  27890  selberg3lem1  27891  selberg3lem2  27892  selberg3  27893  selberg4lem1  27894  selberg4  27895  pntrsumo1  27899  pntrsumbnd  27900  pntrsumbnd2  27901  selbergr  27902  selberg3r  27903  selberg4r  27904  selberg34r  27905  pntsf  27907  pntsval2  27910  pntrlog2bndlem1  27911  pntrlog2bndlem2  27912  pntrlog2bndlem3  27913  pntrlog2bndlem4  27914  pntrlog2bndlem5  27915  pntrlog2bndlem6  27917  pntrlog2bnd  27918  pntpbnd2  27921  pntlemf  27939  pntlemk  27940  pntlemo  27941  eucrct2eupth  30853  dipcl  31321  dipcn  31329  gsummptp1  33666  gsummulsubdishift1  33677  esplyind  34255  esumpcvgval  34758  esumpmono  34759  esumcvg  34766  esumcvgsum  34768  eulerpartlemgc  35042  ballotlemfc0  35173  ballotlemfcc  35174  ballotlemic  35187  ballotlem1c  35188  ballotlemsel1i  35193  ballotlemsf1o  35194  erdszelem4  36047  erdszelem8  36051  erdsze2lem2  36057  cvmliftlem2  36139  cvmliftlem6  36143  cvmliftlem8  36145  cvmliftlem9  36146  cvmliftlem10  36147  bcprod  36597  faclim  36605  poimirlem6  38651  poimirlem7  38652  poimirlem8  38653  poimirlem9  38654  poimirlem11  38656  poimirlem13  38658  poimirlem14  38659  poimirlem15  38660  poimirlem16  38661  poimirlem17  38662  poimirlem18  38663  poimirlem22  38667  poimirlem32  38677  mblfinlem2  38683  aks4d1p1p2  43227  aks4d1p1p4  43228  aks4d1p1  43233  aks4d1p3  43235  aks4d1p4  43236  aks4d1p5  43237  aks4d1p6  43238  aks4d1p7d1  43239  aks4d1p7  43240  aks4d1p8  43244  aks4d1p9  43245  primrootlekpowne0  43262  hashscontpow1  43278  hashscontpow  43279  sticksstones1  43303  sticksstones2  43304  sticksstones3  43305  sticksstones6  43308  sticksstones7  43309  sticksstones10  43312  sticksstones12a  43314  sticksstones12  43315  oddnumth  43475  nicomachus  43476  sumcubes  43477  eldioph3b  43883  diophin  43890  diophun  43891  eldiophss  43892  irrapxlem4  43939  sumnnodd  46749  stoweidlem34  47151  wallispilem4  47185  wallispi  47187  wallispi2lem1  47188  wallispi2  47190  stirlinglem5  47195  stirlinglem7  47197  stirlinglem10  47200  stirlinglem12  47202  fourierdlem83  47306  fourierdlem112  47335  caratheodorylem2  47644  hoidmvlelem2  47713  hoidmvlelem3  47714  elfz2nn  48499  stgrusgra  49164  isubgr3stgrlem7  49177  altgsumbcALT  49572  nn0sumshdiglemA  49838  nn0sumshdiglemB  49839