Theorem elfzuz 13561

Description: A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzuz	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))

Proof of Theorem elfzuz

Step	Hyp	Ref	Expression
1		elfzuzb 13559	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simplbi 497	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6560  (class class class)co 7432  ℤ_≥cuz 12879  ...cfz 13548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-neg 11496  df-z 12616  df-uz 12880  df-fz 13549

This theorem is referenced by:  elfzel1  13564  elfzelz  13565  elfzle1  13568  eluzfz2b  13574  fzsplit2  13590  fzsplit  13591  fzopth  13602  fzss1  13604  fzss2  13605  fzssuz  13606  fzp1elp1  13618  uzsplit  13637  elfzmlbm  13679  predfz  13694  fzosplit  13733  seqf2  14063  seqfeq2  14067  seqfeq  14069  sermono  14076  seqf1olem2  14084  seqz  14092  seqfeq3  14094  ser0  14096  seqcoll  14504  swrdval2  14685  swrdswrd  14744  pfxccatin12  14772  pfxccatpfx2  14776  spllen  14793  swrds2m  14981  limsupgre  15518  clim2ser  15692  clim2ser2  15693  isermulc2  15695  iserle  15697  climub  15699  isercolllem1  15702  isercolllem3  15704  isercoll2  15706  iseraltlem1  15719  fsumcvg  15749  fsumser  15767  isumclim3  15796  isumadd  15804  fsump1i  15806  fsum0diaglem  15813  o1fsum  15850  iserabs  15852  cvgcmp  15853  cvgcmpub  15854  cvgcmpce  15855  isumsplit  15877  isum1p  15878  isumsup2  15883  climcndslem1  15886  climcndslem2  15887  climcnds  15888  geoserg  15903  mertenslem1  15921  clim2div  15926  prodf1  15928  prodfn0  15931  ntrivcvgmullem  15938  fprodcvg  15967  fprodntriv  15979  fprodabs  16011  fprodeq0  16012  iprodclim3  16037  iprodmul  16040  fprodefsum  16132  prmind2  16723  prmdvdsfz  16743  pcfac  16938  prmreclem4  16958  prmreclem5  16959  prmgaplem1  17088  prmgaplem2  17089  prmgaplcmlem2  17091  prmgapprmolem  17100  efgtlen  19745  efgredleme  19762  ovolunlem1a  25532  ovolicc1  25552  uniioombllem3  25621  dvfsumrlimf  26066  dvfsumlem1  26067  dvfsumlem2  26068  dvfsumlem2OLD  26069  dvfsumlem3  26070  dvfsumlem4  26071  dvfsum2  26076  coeidlem  26277  coeid3  26280  vieta1lem2  26354  mtest  26448  mtestbdd  26449  birthdaylem2  26996  wilth  27115  ftalem4  27120  ftalem5  27121  chtub  27257  mersenne  27272  bposlem6  27334  lgsdilem2  27378  rplogsumlem1  27529  rplogsumlem2  27530  dchrisumlem2  27535  dchrisum0lem1  27561  logdivbnd  27601  pntrsumbnd2  27612  pntrlog2bndlem1  27622  pntpbnd1  27631  pntpbnd2  27632  pntlemh  27644  pntlemj  27648  axlowdimlem17  28974  fzsplit3  32796  swrdrn2  32940  swrdrn3  32941  swrdf1  32942  swrdrndisj  32943  ballotlemfrci  34531  subfacp1lem3  35188  knoppcnlem11  36505  poimirlem1  37629  poimirlem2  37630  poimirlem31  37659  poimirlem32  37660  mblfinlem2  37666  mettrifi  37765  geomcau  37767  fzsplitnd  41984  aks4d1p3  42080  iunincfi  45104  elfzfzo  45293  fsumsermpt  45599  fmulcl  45601  fmuldfeqlem1  45602  iblspltprt  45993  itgspltprt  45999  stoweidlem11  46031  stoweidlem17  46037  stirlinglem7  46100  fourierdlem15  46142  fourierdlem25  46152  sge0isum  46447  sge0seq  46466  sge0reuz  46467  sge0reuzb  46468  iundjiun  46480  meaiuninclem  46500  carageniuncllem1  46541  carageniuncllem2  46542  caratheodorylem1  46546  ssfz12  47331  iccpartgt  47419