Theorem elfzuz 13420

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6481  (class class class)co 7346  ℤ_≥cuz 12732  ...cfz 13407

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-resscn 11063

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-neg 11347  df-z 12469  df-uz 12733  df-fz 13408

This theorem is referenced by:  elfzel1  13423  elfzelz  13424  elfzle1  13427  eluzfz2b  13433  fzsplit2  13449  fzsplit  13450  fzopth  13461  fzss1  13463  fzss2  13464  fzssuz  13465  fzp1elp1  13477  uzsplit  13496  elfzmlbm  13538  predfz  13553  fzosplit  13592  seqf2  13928  seqfeq2  13932  seqfeq  13934  sermono  13941  seqf1olem2  13949  seqz  13957  seqfeq3  13959  ser0  13961  seqcoll  14371  swrdval2  14554  swrdswrd  14612  pfxccatin12  14640  pfxccatpfx2  14644  spllen  14661  swrds2m  14848  limsupgre  15388  clim2ser  15562  clim2ser2  15563  isermulc2  15565  iserle  15567  climub  15569  isercolllem1  15572  isercolllem3  15574  isercoll2  15576  iseraltlem1  15589  fsumcvg  15619  fsumser  15637  isumclim3  15666  isumadd  15674  fsump1i  15676  fsum0diaglem  15683  o1fsum  15720  iserabs  15722  cvgcmp  15723  cvgcmpub  15724  cvgcmpce  15725  isumsplit  15747  isum1p  15748  isumsup2  15753  climcndslem1  15756  climcndslem2  15757  climcnds  15758  geoserg  15773  mertenslem1  15791  clim2div  15796  prodf1  15798  prodfn0  15801  ntrivcvgmullem  15808  fprodcvg  15837  fprodntriv  15849  fprodabs  15881  fprodeq0  15882  iprodclim3  15907  iprodmul  15910  fprodefsum  16002  prmind2  16596  prmdvdsfz  16616  pcfac  16811  prmreclem4  16831  prmreclem5  16832  prmgaplem1  16961  prmgaplem2  16962  prmgaplcmlem2  16964  prmgapprmolem  16973  efgtlen  19638  efgredleme  19655  ovolunlem1a  25424  ovolicc1  25444  uniioombllem3  25513  dvfsumrlimf  25958  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  dvfsumlem4  25963  dvfsum2  25968  coeidlem  26169  coeid3  26172  vieta1lem2  26246  mtest  26340  mtestbdd  26341  birthdaylem2  26889  wilth  27008  ftalem4  27013  ftalem5  27014  chtub  27150  mersenne  27165  bposlem6  27227  lgsdilem2  27271  rplogsumlem1  27422  rplogsumlem2  27423  dchrisumlem2  27428  dchrisum0lem1  27454  logdivbnd  27494  pntrsumbnd2  27505  pntrlog2bndlem1  27515  pntpbnd1  27524  pntpbnd2  27525  pntlemh  27537  pntlemj  27541  axlowdimlem17  28936  fzsplit3  32776  swrdrn2  32935  swrdrn3  32936  swrdf1  32937  swrdrndisj  32938  ballotlemfrci  34541  subfacp1lem3  35226  knoppcnlem11  36547  poimirlem1  37671  poimirlem2  37672  poimirlem31  37701  poimirlem32  37702  mblfinlem2  37708  mettrifi  37807  geomcau  37809  fzsplitnd  42085  aks4d1p3  42181  iunincfi  45201  elfzfzo  45388  fsumsermpt  45689  fmulcl  45691  fmuldfeqlem1  45692  iblspltprt  46081  itgspltprt  46087  stoweidlem11  46119  stoweidlem17  46125  stirlinglem7  46188  fourierdlem15  46230  fourierdlem25  46240  sge0isum  46535  sge0seq  46554  sge0reuz  46555  sge0reuzb  46556  iundjiun  46568  meaiuninclem  46588  carageniuncllem1  46629  carageniuncllem2  46630  caratheodorylem1  46634  ssfz12  47424  iccpartgt  47537