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

Theorem lenlt 9652
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 9628 . 2  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9628 . 2  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xrlenlt 9641 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2an 475 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367    e. wcel 1823   class class class wbr 4439   RRcr 9480   RR*cxr 9616    < clt 9617    <_ cle 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-xp 4994  df-cnv 4996  df-xr 9621  df-le 9623
This theorem is referenced by:  ltnle  9653  letri3  9659  leloe  9660  eqlelt  9661  ne0gt0  9678  lelttric  9680  lenlti  9693  lenltd  9720  ltaddsub  10022  leord1  10076  lediv1  10403  suprleub  10502  dfinfmr  10515  infmrgelb  10518  nnge1  10557  nnnlt1  10561  avgle1  10774  avgle2  10775  nn0nlt0  10818  recnz  10934  btwnnz  10935  prime  10939  indstr  11151  uzsupss  11175  zbtwnre  11181  rpneg  11251  fzn  11705  nelfzo  11809  fzonlt0  11825  fllt  11924  flflp1  11925  modifeq2int  12031  om2uzlt2i  12044  fsuppmapnn0fiub0  12081  suppssfz  12082  leexp2  12202  discr  12285  bcval4  12367  ccatsymb  12589  swrd0  12650  sqrtneglem  13182  harmonic  13752  efle  13935  dvdsle  14115  infpnlem1  14512  pgpssslw  16833  gsummoncoe1  18541  mp2pm2mplem4  19477  dvferm1  22552  dvferm2  22554  dgrlt  22829  logleb  23156  argrege0  23164  ellogdm  23188  dvlog2lem  23201  cxple  23244  cxple3  23250  asinneg  23414  birthdaylem3  23481  ppieq0  23648  chpeq0  23681  chteq0  23682  lgsval2lem  23779  lgsneg  23792  lgsdilem  23795  ostth2lem1  24001  ostth3  24021  clwlkisclwwlklem2a  24987  rusgranumwlks  25158  frgrareg  25319  friendship  25324  nmounbi  25889  nmlno0lem  25906  nmlnop0iALT  27112  supfz  29348  inffz  29349  fz0n  29351  leceifl  30284  ftc1anclem1  30330  nn0prpw  30381  nninfnub  30484  ellz1  30939  rencldnfilem  30993  icccncfext  31929  subsubelfzo0  32712  digexp  33482
  Copyright terms: Public domain W3C validator