MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfzuz Structured version   Visualization version   GIF version

Theorem elfzuz 12892
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
StepHypRef Expression
1 elfzuzb 12890 . 2 (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝐾)))
21simplbi 498 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cfv 6348  (class class class)co 7145  cuz 12231  ...cfz 12880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7678  df-2nd 7679  df-neg 10861  df-z 11970  df-uz 12232  df-fz 12881
This theorem is referenced by:  elfzel1  12895  elfzelz  12896  elfzle1  12898  eluzfz2b  12904  fzsplit2  12920  fzsplit  12921  fzopth  12932  fzss1  12934  fzss2  12935  fzssuz  12936  fzp1elp1  12948  uzsplit  12967  elfzmlbm  13005  predfz  13020  fzosplit  13058  seqf2  13377  seqfeq2  13381  seqfeq  13383  sermono  13390  seqf1olem2  13398  seqz  13406  seqfeq3  13408  ser0  13410  seqcoll  13810  swrdval2  13996  swrdswrd  14055  pfxccatin12  14083  pfxccatpfx2  14087  spllen  14104  swrds2m  14291  limsupgre  14826  clim2ser  14999  clim2ser2  15000  isermulc2  15002  iserle  15004  climub  15006  isercolllem1  15009  isercolllem3  15011  isercoll2  15013  iseraltlem1  15026  fsumcvg  15057  fsumser  15075  isumclim3  15102  isumadd  15110  fsump1i  15112  fsum0diaglem  15119  o1fsum  15156  iserabs  15158  cvgcmp  15159  cvgcmpub  15160  cvgcmpce  15161  isumsplit  15183  isum1p  15184  isumsup2  15189  climcndslem1  15192  climcndslem2  15193  climcnds  15194  geoserg  15209  mertenslem1  15228  clim2div  15233  prodf1  15235  prodfn0  15238  ntrivcvgmullem  15245  fprodcvg  15272  fprodntriv  15284  fprodabs  15316  fprodeq0  15317  iprodclim3  15342  iprodmul  15345  fprodefsum  15436  prmind2  16017  prmdvdsfz  16037  pcfac  16223  prmreclem4  16243  prmreclem5  16244  prmgaplem1  16373  prmgaplem2  16374  prmgaplcmlem2  16376  prmgapprmolem  16385  efgtlen  18781  efgredleme  18798  ovolunlem1a  24024  ovolicc1  24044  uniioombllem3  24113  dvfsumrlimf  24549  dvfsumlem1  24550  dvfsumlem2  24551  dvfsumlem3  24552  dvfsumlem4  24553  dvfsum2  24558  coeidlem  24754  coeid3  24757  vieta1lem2  24827  mtest  24919  mtestbdd  24920  birthdaylem2  25457  wilth  25575  ftalem4  25580  ftalem5  25581  chtub  25715  mersenne  25730  bposlem6  25792  lgsdilem2  25836  rplogsumlem1  25987  rplogsumlem2  25988  dchrisumlem2  25993  dchrisum0lem1  26019  logdivbnd  26059  pntrsumbnd2  26070  pntrlog2bndlem1  26080  pntpbnd1  26089  pntpbnd2  26090  pntlemh  26102  pntlemj  26106  axlowdimlem17  26671  fzsplit3  30443  swrdrn2  30555  swrdrn3  30556  swrdf1  30557  swrdrndisj  30558  ballotlemfrci  31684  subfacp1lem3  32326  knoppcnlem11  33739  poimirlem1  34774  poimirlem2  34775  poimirlem31  34804  poimirlem32  34805  mblfinlem2  34811  mettrifi  34913  geomcau  34915  iunincfi  41237  elfzfzo  41418  fsumsermpt  41736  fmulcl  41738  fmuldfeqlem1  41739  iblspltprt  42134  itgspltprt  42140  stoweidlem11  42173  stoweidlem17  42179  stirlinglem7  42242  fourierdlem15  42284  fourierdlem25  42294  sge0isum  42586  sge0seq  42605  sge0reuz  42606  sge0reuzb  42607  iundjiun  42619  meaiuninclem  42639  carageniuncllem1  42680  carageniuncllem2  42681  caratheodorylem1  42685  ssfz12  43391  iccpartgt  43464
  Copyright terms: Public domain W3C validator