Theorem elfzuz 13556

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 13554	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simplbi 497	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6562  (class class class)co 7430  ℤ_≥cuz 12875  ...cfz 13543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-neg 11492  df-z 12611  df-uz 12876  df-fz 13544

This theorem is referenced by:  elfzel1  13559  elfzelz  13560  elfzle1  13563  eluzfz2b  13569  fzsplit2  13585  fzsplit  13586  fzopth  13597  fzss1  13599  fzss2  13600  fzssuz  13601  fzp1elp1  13613  uzsplit  13632  elfzmlbm  13674  predfz  13689  fzosplit  13728  seqf2  14058  seqfeq2  14062  seqfeq  14064  sermono  14071  seqf1olem2  14079  seqz  14087  seqfeq3  14089  ser0  14091  seqcoll  14499  swrdval2  14680  swrdswrd  14739  pfxccatin12  14767  pfxccatpfx2  14771  spllen  14788  swrds2m  14976  limsupgre  15513  clim2ser  15687  clim2ser2  15688  isermulc2  15690  iserle  15692  climub  15694  isercolllem1  15697  isercolllem3  15699  isercoll2  15701  iseraltlem1  15714  fsumcvg  15744  fsumser  15762  isumclim3  15791  isumadd  15799  fsump1i  15801  fsum0diaglem  15808  o1fsum  15845  iserabs  15847  cvgcmp  15848  cvgcmpub  15849  cvgcmpce  15850  isumsplit  15872  isum1p  15873  isumsup2  15878  climcndslem1  15881  climcndslem2  15882  climcnds  15883  geoserg  15898  mertenslem1  15916  clim2div  15921  prodf1  15923  prodfn0  15926  ntrivcvgmullem  15933  fprodcvg  15962  fprodntriv  15974  fprodabs  16006  fprodeq0  16007  iprodclim3  16032  iprodmul  16035  fprodefsum  16127  prmind2  16718  prmdvdsfz  16738  pcfac  16932  prmreclem4  16952  prmreclem5  16953  prmgaplem1  17082  prmgaplem2  17083  prmgaplcmlem2  17085  prmgapprmolem  17094  efgtlen  19758  efgredleme  19775  ovolunlem1a  25544  ovolicc1  25564  uniioombllem3  25633  dvfsumrlimf  26079  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsum2  26089  coeidlem  26290  coeid3  26293  vieta1lem2  26367  mtest  26461  mtestbdd  26462  birthdaylem2  27009  wilth  27128  ftalem4  27133  ftalem5  27134  chtub  27270  mersenne  27285  bposlem6  27347  lgsdilem2  27391  rplogsumlem1  27542  rplogsumlem2  27543  dchrisumlem2  27548  dchrisum0lem1  27574  logdivbnd  27614  pntrsumbnd2  27625  pntrlog2bndlem1  27635  pntpbnd1  27644  pntpbnd2  27645  pntlemh  27657  pntlemj  27661  axlowdimlem17  28987  fzsplit3  32801  swrdrn2  32923  swrdrn3  32924  swrdf1  32925  swrdrndisj  32926  ballotlemfrci  34508  subfacp1lem3  35166  knoppcnlem11  36485  poimirlem1  37607  poimirlem2  37608  poimirlem31  37637  poimirlem32  37638  mblfinlem2  37644  mettrifi  37743  geomcau  37745  fzsplitnd  41963  aks4d1p3  42059  iunincfi  45033  elfzfzo  45226  fsumsermpt  45534  fmulcl  45536  fmuldfeqlem1  45537  iblspltprt  45928  itgspltprt  45934  stoweidlem11  45966  stoweidlem17  45972  stirlinglem7  46035  fourierdlem15  46077  fourierdlem25  46087  sge0isum  46382  sge0seq  46401  sge0reuz  46402  sge0reuzb  46403  iundjiun  46415  meaiuninclem  46435  carageniuncllem1  46476  carageniuncllem2  46477  caratheodorylem1  46481  ssfz12  47263  iccpartgt  47351