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

Theorem lenlt 8901
Description: 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.)
Assertion
Ref Expression
lenlt  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )

Proof of Theorem lenlt
StepHypRef Expression
1 rexr 8877 . 2  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 8877 . 2  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xrlenlt 8890 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2an 463 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1684   class class class wbr 4023   RRcr 8736   RR*cxr 8866    < clt 8867    <_ cle 8868
This theorem is referenced by:  ltnle  8902  letri3  8907  leloe  8908  eqlelt  8909  ne0gt0  8925  lelttric  8927  lenlti  8938  lenltd  8965  ltaddsub  9248  leord1  9300  lediv1  9621  suprleub  9718  dfinfmr  9731  infmrgelb  9734  nnge1  9772  nnnlt1  9776  avgle1  9951  avgle2  9952  nn0nlt0  9992  recnz  10087  btwnnz  10088  prime  10092  indstr  10287  uzsupss  10310  zbtwnre  10314  rpneg  10383  fzn  10810  fllt  10938  om2uzlt2i  11014  leexp2  11156  discr  11238  bcval4  11320  sqrneglem  11752  harmonic  12317  efle  12398  dvdsle  12574  infpnlem1  12957  pgpssslw  14925  dvferm1  19332  dvferm2  19334  dgrlt  19647  logleb  19957  argrege0  19965  ellogdm  19986  dvlog2lem  19999  cxple  20042  cxple3  20048  asinneg  20182  birthdaylem3  20248  ppieq0  20414  chpeq0  20447  chteq0  20448  lgsval2lem  20545  lgsneg  20558  lgsdilem  20561  ostth2lem1  20767  ostth3  20787  nmounbi  21354  nmlno0lem  21371  nmlnop0iALT  22575  supfz  24094  inffz  24095  fz0n  24097  nn0prpw  26239  nninfnub  26461  ellz1  26846  rencldnfilem  26903  stoweidlem14  27763  stoweidlem52  27801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-cnv 4697  df-xr 8871  df-le 8873
  Copyright terms: Public domain W3C validator