MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluzle Unicode version

Theorem eluzle 10332
Description: Implication of membership in a set of upper integers. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
eluzle  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  <_  N )

Proof of Theorem eluzle
StepHypRef Expression
1 eluz2 10328 . 2  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
21simp3bi 972 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  <_  N )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   class class class wbr 4104   ` cfv 5337    <_ cle 8958   ZZcz 10116   ZZ>=cuz 10322
This theorem is referenced by:  uztrn  10336  uzneg  10338  uzss  10340  uz11  10342  eluzp1l  10344  uzm1  10350  uzin  10352  uzind4  10368  uzwo  10373  uzwoOLD  10374  uzinfmi  10389  uzsupss  10402  elfz5  10882  elfzle1  10891  elfzle2  10892  elfzle3  10894  elfz2nn0  10913  uzsplit  10947  uzdisj  10948  uznfz  10957  fzouzdisj  10994  expmulnbnd  11326  seqcoll  11497  rexuzre  11932  rlimclim1  12115  isercoll  12237  iseralt  12254  o1fsum  12368  mertenslem1  12437  efcllem  12456  rpnnen2lem9  12598  smuval2  12770  smupvallem  12771  hashdvds  12940  pcmpt2  13038  pcfaclem  13043  pcfac  13044  vdwlem6  13130  ramtlecl  13144  prmlem1  13206  prmlem2  13218  znfld  16620  lmnn  18793  mbflimsup  19125  mbfi1fseqlem6  19179  dvfsumge  19473  plyco0  19678  coeeulem  19710  radcnvlem2  19897  log2tlbnd  20352  chtub  20563  chpval2  20569  chpchtsum  20570  bcmax  20629  bpos1lem  20633  bpos1  20634  bposlem3  20637  bposlem4  20638  bposlem5  20639  bposlem6  20640  lgslem1  20647  lgsdirprm  20680  lgseisen  20704  m1lgs  20713  dchrisumlema  20749  dchrisumlem2  20751  dchrisum0lem1  20777  minvecolem3  21569  minvecolem4  21573  lgamgulmlem4  24065  lgamcvg2  24088  subfacval3  24124  climuzcnv  24408  fprodeq0  24600  axlowdimlem3  25131  axlowdimlem6  25134  axlowdimlem7  25135  axlowdimlem16  25144  axlowdimlem17  25145  fdc  25779  jm2.24nn  26369  jm2.23  26412  expdiophlem1  26437  fmul01lt1lem1  27037  climsuselem1  27056  climsuse  27057  stoweidlem11  27083  stirlinglem11  27156  constr3trllem3  27776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-cnex 8883  ax-resscn 8884
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-fv 5345  df-ov 5948  df-neg 9130  df-z 10117  df-uz 10323
  Copyright terms: Public domain W3C validator