Theorem elfzuz 13457

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  (class class class)co 7369  ℤ_≥cuz 12769  ...cfz 13444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948  df-neg 11384  df-z 12506  df-uz 12770  df-fz 13445

This theorem is referenced by:  elfzel1  13460  elfzelz  13461  elfzle1  13464  eluzfz2b  13470  fzsplit2  13486  fzsplit  13487  fzopth  13498  fzss1  13500  fzss2  13501  fzssuz  13502  fzp1elp1  13514  uzsplit  13533  elfzmlbm  13575  predfz  13590  fzosplit  13629  seqf2  13962  seqfeq2  13966  seqfeq  13968  sermono  13975  seqf1olem2  13983  seqz  13991  seqfeq3  13993  ser0  13995  seqcoll  14405  swrdval2  14587  swrdswrd  14646  pfxccatin12  14674  pfxccatpfx2  14678  spllen  14695  swrds2m  14883  limsupgre  15423  clim2ser  15597  clim2ser2  15598  isermulc2  15600  iserle  15602  climub  15604  isercolllem1  15607  isercolllem3  15609  isercoll2  15611  iseraltlem1  15624  fsumcvg  15654  fsumser  15672  isumclim3  15701  isumadd  15709  fsump1i  15711  fsum0diaglem  15718  o1fsum  15755  iserabs  15757  cvgcmp  15758  cvgcmpub  15759  cvgcmpce  15760  isumsplit  15782  isum1p  15783  isumsup2  15788  climcndslem1  15791  climcndslem2  15792  climcnds  15793  geoserg  15808  mertenslem1  15826  clim2div  15831  prodf1  15833  prodfn0  15836  ntrivcvgmullem  15843  fprodcvg  15872  fprodntriv  15884  fprodabs  15916  fprodeq0  15917  iprodclim3  15942  iprodmul  15945  fprodefsum  16037  prmind2  16631  prmdvdsfz  16651  pcfac  16846  prmreclem4  16866  prmreclem5  16867  prmgaplem1  16996  prmgaplem2  16997  prmgaplcmlem2  16999  prmgapprmolem  17008  efgtlen  19640  efgredleme  19657  ovolunlem1a  25430  ovolicc1  25450  uniioombllem3  25519  dvfsumrlimf  25964  dvfsumlem1  25965  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumlem4  25969  dvfsum2  25974  coeidlem  26175  coeid3  26178  vieta1lem2  26252  mtest  26346  mtestbdd  26347  birthdaylem2  26895  wilth  27014  ftalem4  27019  ftalem5  27020  chtub  27156  mersenne  27171  bposlem6  27233  lgsdilem2  27277  rplogsumlem1  27428  rplogsumlem2  27429  dchrisumlem2  27434  dchrisum0lem1  27460  logdivbnd  27500  pntrsumbnd2  27511  pntrlog2bndlem1  27521  pntpbnd1  27530  pntpbnd2  27531  pntlemh  27543  pntlemj  27547  axlowdimlem17  28938  fzsplit3  32766  swrdrn2  32926  swrdrn3  32927  swrdf1  32928  swrdrndisj  32929  ballotlemfrci  34512  subfacp1lem3  35162  knoppcnlem11  36484  poimirlem1  37608  poimirlem2  37609  poimirlem31  37638  poimirlem32  37639  mblfinlem2  37645  mettrifi  37744  geomcau  37746  fzsplitnd  41963  aks4d1p3  42059  iunincfi  45081  elfzfzo  45268  fsumsermpt  45570  fmulcl  45572  fmuldfeqlem1  45573  iblspltprt  45964  itgspltprt  45970  stoweidlem11  46002  stoweidlem17  46008  stirlinglem7  46071  fourierdlem15  46113  fourierdlem25  46123  sge0isum  46418  sge0seq  46437  sge0reuz  46438  sge0reuzb  46439  iundjiun  46451  meaiuninclem  46471  carageniuncllem1  46512  carageniuncllem2  46513  caratheodorylem1  46517  ssfz12  47308  iccpartgt  47421