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

Theorem eluzle 10503
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 10499 . 2  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
21simp3bi 975 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  <_  N )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   class class class wbr 4215   ` cfv 5457    <_ cle 9126   ZZcz 10287   ZZ>=cuz 10493
This theorem is referenced by:  uztrn  10507  uzneg  10509  uzss  10511  uz11  10513  eluzp1l  10515  uzm1  10521  uzin  10523  uzind4  10539  uzwo  10544  uzwoOLD  10545  uzinfmi  10560  uzsupss  10573  elfz5  11056  elfzle1  11065  elfzle2  11066  elfzle3  11068  elfz2nn0  11087  uzsplit  11123  uzdisj  11124  uznfz  11135  fzouzdisj  11174  expmulnbnd  11516  seqcoll  11717  rexuzre  12161  rlimclim1  12344  isercoll  12466  iseralt  12483  o1fsum  12597  mertenslem1  12666  efcllem  12685  rpnnen2lem9  12827  smuval2  12999  smupvallem  13000  hashdvds  13169  pcmpt2  13267  pcfaclem  13272  pcfac  13273  vdwlem6  13359  ramtlecl  13373  prmlem1  13435  prmlem2  13447  znfld  16846  lmnn  19221  mbflimsup  19561  mbfi1fseqlem6  19615  dvfsumge  19911  plyco0  20116  coeeulem  20148  radcnvlem2  20335  log2tlbnd  20790  chtub  21001  chpval2  21007  chpchtsum  21008  bcmax  21067  bpos1lem  21071  bpos1  21072  bposlem3  21075  bposlem4  21076  bposlem5  21077  bposlem6  21078  lgslem1  21085  lgsdirprm  21118  lgseisen  21142  m1lgs  21151  dchrisumlema  21187  dchrisumlem2  21189  dchrisum0lem1  21215  constr3trllem3  21644  minvecolem3  22383  minvecolem4  22387  rnlogblem  24404  lgamgulmlem4  24821  lgamcvg2  24844  subfacval3  24880  climuzcnv  25113  fprodeq0  25304  axlowdimlem3  25888  axlowdimlem6  25891  axlowdimlem7  25892  axlowdimlem16  25901  axlowdimlem17  25902  fdc  26463  jm2.24nn  27038  jm2.23  27081  expdiophlem1  27106  fmul01lt1lem1  27704  climsuselem1  27723  climsuse  27724  stoweidlem11  27750  stirlinglem11  27823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-cnex 9051  ax-resscn 9052
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-fv 5465  df-ov 6087  df-neg 9299  df-z 10288  df-uz 10494
  Copyright terms: Public domain W3C validator