Theorem elfznn 12370

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 12342	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
2		elfzle1 12344	. 2 ⊢ (𝐾 ∈ (1...𝑁) → 1 ≤ 𝐾)
3		elnnz1 11403	. 2 ⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℤ ∧ 1 ≤ 𝐾))
4	1, 2, 3	sylanbrc 698	1 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 1990   class class class wbr 4653  (class class class)co 6650  1c1 9937   ≤ cle 10075  ℕcn 11020  ℤcz 11377  ...cfz 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-z 11378  df-uz 11688  df-fz 12327

This theorem is referenced by:  elfz1end  12371  fz1ssnn  12372  fzossnn  12516  bcm1k  13102  bcpasc  13108  seqcoll  13248  swrd0fv0  13440  swrd0fvlsw  13443  isercolllem2  14396  isercolllem3  14397  isercoll  14398  sumeq2ii  14423  summolem3  14445  summolem2a  14446  fsum  14451  sumz  14453  fsumconst  14522  o1fsum  14545  binomlem  14561  incexc2  14570  climcndslem1  14581  climcndslem2  14582  climcnds  14583  harmonic  14591  arisum2  14593  trireciplem  14594  geo2sum  14604  geo2lim  14606  prodeq2ii  14643  prodmolem3  14663  prodmolem2a  14664  fprod  14671  prod1  14674  fprodfac  14703  fprodconst  14708  risefallfac  14755  risefacfac  14766  fallfacval4  14774  bpolydiflem  14785  rpnnen2lem10  14952  fzm1ndvds  15044  pwp1fsum  15114  lcmflefac  15361  phicl  15474  prmdivdiv  15492  pcfac  15603  pcbc  15604  prmreclem2  15621  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  prmrec  15626  4sqlem13  15661  vdwlem2  15686  vdwlem3  15687  vdwlem10  15694  vdwlem12  15696  prmocl  15738  prmop1  15742  fvprmselelfz  15748  fvprmselgcd1  15749  prmolefac  15750  prmodvdslcmf  15751  prmgapprmo  15766  mulgnnsubcl  17553  mulgnn0z  17567  mulgnndir  17569  mulgnndirOLD  17570  oddvdsnn0  17963  odnncl  17964  gexcl3  18002  efgsres  18151  mulgnn0di  18231  gsumconst  18334  srgbinomlem4  18543  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmadugsumlemF  20681  1stcfb  21248  1stckgenlem  21356  lebnumii  22765  ovollb2lem  23256  ovolunlem1a  23264  ovoliunlem1  23270  ovoliunlem2  23271  ovoliun2  23274  ovolscalem1  23281  ovolicc2lem4  23288  voliunlem1  23318  volsup  23324  ioombl1lem4  23329  uniioovol  23347  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombllem6  23356  dvply1  24039  aaliou3lem5  24102  aaliou3lem6  24103  dvtaylp  24124  taylthlem2  24128  pserdvlem2  24182  logfac  24347  atantayl  24664  birthdaylem2  24679  emcllem1  24722  emcllem2  24723  emcllem3  24724  emcllem5  24726  emcllem7  24728  harmoniclbnd  24735  harmonicubnd  24736  harmonicbnd4  24737  fsumharmonic  24738  lgamcvg2  24781  gamcvg2lem  24785  wilthlem1  24794  wilthlem2  24795  ftalem5  24803  basellem1  24807  basellem8  24814  chpf  24849  efchpcl  24851  chpp1  24881  chpwordi  24883  prmorcht  24904  dvdsflf1o  24913  dvdsflsumcom  24914  chtlepsi  24931  fsumvma2  24939  pclogsum  24940  vmasum  24941  logfac2  24942  chpval2  24943  chpchtsum  24944  logfaclbnd  24947  logexprlim  24950  logfacrlim2  24951  pcbcctr  25001  bposlem1  25009  bposlem2  25010  lgscllem  25029  lgsval2lem  25032  lgsval4a  25044  lgsneg  25046  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  lgsqrlem2  25072  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  2lgslem1a1  25114  chebbnd1lem1  25158  vmadivsum  25171  vmadivsumb  25172  rplogsumlem2  25174  dchrisum0lem1a  25175  rpvmasumlem  25176  dchrisumlem2  25179  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasum2if  25186  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrisum0  25209  dchrmusumlem  25211  dchrvmasumlem  25212  rplogsum  25216  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  mulog2sumlem1  25223  mulog2sumlem2  25224  mulog2sumlem3  25225  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  log2sumbnd  25233  selberglem1  25234  selberglem2  25235  selberglem3  25236  selberg  25237  selbergb  25238  selberg2lem  25239  selberg2  25240  selberg2b  25241  chpdifbndlem1  25242  logdivbnd  25245  selberg3lem1  25246  selberg3lem2  25247  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrsumo1  25254  pntrsumbnd  25255  pntrsumbnd2  25256  selbergr  25257  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntsf  25262  pntsval2  25265  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd2  25276  pntlemf  25294  pntlemk  25295  pntlemo  25296  eucrct2eupth  27105  dipcl  27567  dipcn  27575  esumpcvgval  30140  esumpmono  30141  esumcvg  30148  esumcvgsum  30150  eulerpartlemgc  30424  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemimin  30567  ballotlemic  30568  ballotlem1c  30569  ballotlemsel1i  30574  ballotlemsf1o  30575  erdszelem4  31176  erdszelem8  31180  erdsze2lem2  31186  cvmliftlem2  31268  cvmliftlem6  31272  cvmliftlem8  31274  cvmliftlem9  31275  cvmliftlem10  31276  bcprod  31624  faclim  31632  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem11  33420  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem22  33431  poimirlem32  33441  mblfinlem2  33447  eldioph3b  37328  diophin  37336  diophun  37337  eldiophss  37338  irrapxlem4  37389  sumnnodd  39862  stoweidlem34  40251  wallispilem4  40285  wallispi  40287  wallispi2lem1  40288  wallispi2  40290  stirlinglem5  40295  stirlinglem7  40297  stirlinglem10  40300  stirlinglem12  40302  fourierdlem83  40406  fourierdlem112  40435  caratheodorylem2  40741  hoidmvlelem2  40810  hoidmvlelem3  40811  pfxfv0  41400  pfxfvlsw  41403  pwdif  41501  altgsumbcALT  42131  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414