Theorem elfzuz 13543

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

Syntax hints:   → wi 4   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410  ℤ_≥cuz 12857  ...cfz 13530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11439  df-z 12587  df-uz 12858  df-fz 13531

This theorem is referenced by:  elfzel1  13546  elfzelz  13547  elfzle1  13550  eluzfz2b  13556  fzsplit2  13573  fzsplit  13574  fzopth  13585  fzss1  13587  fzss2  13588  fzssuz  13589  fzp1elp1  13601  uzsplit  13620  elfzmlbm  13662  predfz  13677  fzosplit  13717  seqf2  14053  seqfeq2  14057  seqfeq  14059  sermono  14066  seqf1olem2  14074  seqz  14082  seqfeq3  14084  ser0  14086  seqcoll  14497  swrdval2  14680  swrdswrd  14738  pfxccatin12  14766  pfxccatpfx2  14770  spllen  14787  swrds2m  14974  limsupgre  15528  clim2ser  15702  clim2ser2  15703  isermulc2  15705  iserle  15707  climub  15709  isercolllem1  15712  isercolllem3  15714  isercoll2  15716  iseraltlem1  15729  fsumcvg  15759  fsumser  15777  isumclim3  15806  isumadd  15814  fsump1i  15816  fsum0diaglem  15823  o1fsum  15861  iserabs  15863  cvgcmp  15864  cvgcmpub  15865  cvgcmpce  15866  isumsplit  15890  isum1p  15891  isumsup2  15896  climcndslem1  15899  climcndslem2  15900  climcnds  15901  geoserg  15916  mertenslem1  15934  clim2div  15939  prodf1  15941  prodfn0  15944  ntrivcvgmullem  15951  fprodcvg  15980  fprodntriv  15992  fprodabs  16024  fprodeq0  16025  iprodclim3  16050  iprodmul  16053  fprodefsum  16144  prmind2  16738  prmdvdsfz  16759  pcfac  16954  prmreclem4  16974  prmreclem5  16975  prmgaplem1  17104  prmgaplem2  17105  prmgaplcmlem2  17107  prmgapprmolem  17116  efgtlen  19791  efgredleme  19808  ovolunlem1a  25655  ovolicc1  25675  uniioombllem3  25744  dvfsumrlimf  26184  dvfsumlem1  26185  dvfsumlem2  26186  dvfsumlem3  26187  dvfsumlem4  26188  dvfsum2  26193  coeidlem  26394  coeid3  26397  vieta1lem2  26472  mtest  26567  mtestbdd  26568  birthdaylem2  27117  wilth  27235  ftalem4  27240  ftalem5  27241  chtub  27376  mersenne  27391  bposlem6  27453  lgsdilem2  27497  rplogsumlem1  27648  rplogsumlem2  27649  dchrisumlem2  27654  dchrisum0lem1  27680  logdivbnd  27720  pntrsumbnd2  27731  pntrlog2bndlem1  27741  pntpbnd1  27750  pntpbnd2  27751  pntlemh  27763  pntlemj  27767  axlowdimlem17  29308  fzsplit3  33138  swrdrn2  33274  swrdrn3  33275  swrdf1  33276  swrdrndisj  33277  ballotlemfrci  34918  subfacp1lem3  35674  knoppcnlem11  37112  poimirlem1  38292  poimirlem2  38293  poimirlem31  38322  poimirlem32  38323  mblfinlem2  38329  mettrifi  38428  geomcau  38430  fzsplitnd  42769  aks4d1p3  42865  iunincfi  45832  elfzfzo  46016  fsumsermpt  46315  fmulcl  46317  fmuldfeqlem1  46318  iblspltprt  46707  itgspltprt  46713  stoweidlem11  46745  stoweidlem17  46751  stirlinglem7  46814  fourierdlem15  46856  fourierdlem25  46866  sge0isum  47161  sge0seq  47180  sge0reuz  47181  sge0reuzb  47182  iundjiun  47194  meaiuninclem  47214  carageniuncllem1  47255  carageniuncllem2  47256  caratheodorylem1  47260  ssfz12  48071  iccpartgt  48196  indprmfz  48402