Theorem elfznn 13469

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  (class class class)co 7358  1c1 11027   ≤ cle 11167  ℕcn 12145  ℤcz 12488  ...cfz 13423

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  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 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-z 12489  df-uz 12752  df-fz 13424

This theorem is referenced by:  elfz1end  13470  fz1ssnn  13471  bcm1k  14238  bcpasc  14244  seqcoll  14387  pfxfv0  14615  pfxfvlsw  14618  isercolllem2  15589  isercolllem3  15590  isercoll  15591  sumeq2ii  15616  summolem3  15637  summolem2a  15638  fsum  15643  sumz  15645  fsumconst  15713  o1fsum  15736  binomlem  15752  incexc2  15761  climcndslem1  15772  climcndslem2  15773  climcnds  15774  harmonic  15782  arisum2  15784  trireciplem  15785  pwdif  15791  geo2sum  15796  geo2lim  15798  prodeq2ii  15834  prodmolem3  15856  prodmolem2a  15857  fprod  15864  prod1  15867  fprodfac  15896  fprodconst  15901  risefallfac  15947  risefacfac  15958  fallfacval4  15966  bpolydiflem  15977  rpnnen2lem10  16148  fzm1ndvds  16249  pwp1fsum  16318  lcmflefac  16575  prmdvdsbc  16653  phicl  16696  prmdivdiv  16714  pcfac  16827  pcbc  16828  prmreclem2  16845  prmreclem3  16846  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  prmrec  16850  4sqlem13  16885  vdwlem2  16910  vdwlem3  16911  vdwlem10  16918  vdwlem12  16920  prmocl  16962  prmop1  16966  fvprmselelfz  16972  fvprmselgcd1  16973  prmolefac  16974  prmodvdslcmf  16975  prmgapprmo  16990  mulgnngsum  19009  mulgnnsubcl  19016  mulgnn0z  19031  mulgnndir  19033  oddvdsnn0  19473  odnncl  19474  gexcl3  19516  efgsres  19667  mulgnn0di  19754  gsumconst  19863  srgbinomlem4  20164  freshmansdream  21529  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmadugsumlemF  22820  lebnumii  24921  ovollb2lem  25445  ovolunlem1a  25453  ovoliunlem1  25459  ovoliunlem2  25460  ovoliun2  25463  ovolscalem1  25470  ovolicc2lem4  25477  voliunlem1  25507  volsup  25513  ioombl1lem4  25518  uniioovol  25536  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombllem6  25545  dvply1  26247  aaliou3lem5  26311  aaliou3lem6  26312  dvtaylp  26334  taylthlem2  26338  taylthlem2OLD  26339  pserdvlem2  26394  logfac  26566  atantayl  26903  birthdaylem2  26918  emcllem1  26962  emcllem2  26963  emcllem3  26964  emcllem5  26966  emcllem7  26968  harmoniclbnd  26975  harmonicubnd  26976  harmonicbnd4  26977  fsumharmonic  26978  lgamcvg2  27021  gamcvg2lem  27025  wilthlem1  27034  wilthlem2  27035  ftalem5  27043  basellem1  27047  basellem8  27054  chpf  27089  efchpcl  27091  chpp1  27121  chpwordi  27123  prmorcht  27144  dvdsflf1o  27153  dvdsflsumcom  27154  chtlepsi  27173  fsumvma2  27181  pclogsum  27182  vmasum  27183  logfac2  27184  chpval2  27185  chpchtsum  27186  logfaclbnd  27189  logexprlim  27192  logfacrlim2  27193  pcbcctr  27243  bposlem1  27251  bposlem2  27252  lgscllem  27271  lgsval2lem  27274  lgsval4a  27286  lgsneg  27288  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  lgsqrlem2  27314  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgseisen  27346  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  2lgslem1a1  27356  chebbnd1lem1  27436  vmadivsum  27449  vmadivsumb  27450  rplogsumlem2  27452  dchrisum0lem1a  27453  rpvmasumlem  27454  dchrisumlem2  27457  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasum2if  27464  dchrvmasumlem2  27465  dchrvmasumlem3  27466  dchrvmasumiflem1  27468  dchrvmasumiflem2  27469  dchrisum0fno1  27478  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0lem3  27486  dchrisum0  27487  dchrmusumlem  27489  dchrvmasumlem  27490  rplogsum  27494  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  mulog2sumlem1  27501  mulog2sumlem2  27502  mulog2sumlem3  27503  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  log2sumbnd  27511  selberglem1  27512  selberglem2  27513  selberglem3  27514  selberg  27515  selbergb  27516  selberg2lem  27517  selberg2  27518  selberg2b  27519  chpdifbndlem1  27520  logdivbnd  27523  selberg3lem1  27524  selberg3lem2  27525  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrsumo1  27532  pntrsumbnd  27533  pntrsumbnd2  27534  selbergr  27535  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntsf  27540  pntsval2  27543  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd2  27554  pntlemf  27572  pntlemk  27573  pntlemo  27574  eucrct2eupth  30320  dipcl  30787  dipcn  30795  gsummptp1  33140  gsummulsubdishift1  33151  esplyind  33731  esumpcvgval  34235  esumpmono  34236  esumcvg  34243  esumcvgsum  34245  eulerpartlemgc  34519  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemic  34664  ballotlem1c  34665  ballotlemsel1i  34670  ballotlemsf1o  34671  erdszelem4  35388  erdszelem8  35392  erdsze2lem2  35398  cvmliftlem2  35480  cvmliftlem6  35484  cvmliftlem8  35486  cvmliftlem9  35487  cvmliftlem10  35488  bcprod  35932  faclim  35940  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem9  37830  poimirlem11  37832  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem22  37843  poimirlem32  37853  mblfinlem2  37859  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1  42330  aks4d1p3  42332  aks4d1p4  42333  aks4d1p5  42334  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  aks4d1p9  42342  primrootlekpowne0  42359  hashscontpow1  42375  hashscontpow  42376  sticksstones1  42400  sticksstones2  42401  sticksstones3  42402  sticksstones6  42405  sticksstones7  42406  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  oddnumth  42566  nicomachus  42567  sumcubes  42568  eldioph3b  43007  diophin  43014  diophun  43015  eldiophss  43016  irrapxlem4  43067  sumnnodd  45876  stoweidlem34  46278  wallispilem4  46312  wallispi  46314  wallispi2lem1  46315  wallispi2  46317  stirlinglem5  46322  stirlinglem7  46324  stirlinglem10  46327  stirlinglem12  46329  fourierdlem83  46433  fourierdlem112  46462  caratheodorylem2  46771  hoidmvlelem2  46840  hoidmvlelem3  46841  stgrusgra  48205  isubgr3stgrlem7  48218  altgsumbcALT  48599  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866