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

Theorem lenlt 9159
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 9135 . 2  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9135 . 2  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xrlenlt 9148 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2an 465 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    e. wcel 1726   class class class wbr 4215   RRcr 8994   RR*cxr 9124    < clt 9125    <_ cle 9126
This theorem is referenced by:  ltnle  9160  letri3  9165  leloe  9166  eqlelt  9167  ne0gt0  9183  lelttric  9185  lenlti  9198  lenltd  9224  ltaddsub  9507  leord1  9559  lediv1  9880  suprleub  9977  dfinfmr  9990  infmrgelb  9993  nnge1  10031  nnnlt1  10035  avgle1  10212  avgle2  10213  nn0nlt0  10253  recnz  10350  btwnnz  10351  prime  10355  indstr  10550  uzsupss  10573  zbtwnre  10577  rpneg  10646  fzn  11076  fllt  11220  om2uzlt2i  11296  leexp2  11439  discr  11521  bcval4  11603  sqrneglem  12077  harmonic  12643  efle  12724  dvdsle  12900  infpnlem1  13283  pgpssslw  15253  dvferm1  19874  dvferm2  19876  dgrlt  20189  logleb  20503  argrege0  20511  ellogdm  20535  dvlog2lem  20548  cxple  20591  cxple3  20597  asinneg  20731  birthdaylem3  20797  ppieq0  20964  chpeq0  20997  chteq0  20998  lgsval2lem  21095  lgsneg  21108  lgsdilem  21111  ostth2lem1  21317  ostth3  21337  nmounbi  22282  nmlno0lem  22299  nmlnop0iALT  23503  supfz  25204  inffz  25205  fz0n  25207  leceifl  26248  lxflflp1  26249  ftc1anclem1  26294  nn0prpw  26340  nninfnub  26469  ellz1  26839  rencldnfilem  26895  subsubelfzo0  28158  modifeq2int  28184  wrdsymb0  28202  ccatsymb  28211  swrdnd  28216  swrdvalodm2  28222  2cshwmod  28291
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-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  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-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-xp 4887  df-cnv 4889  df-xr 9129  df-le 9131
  Copyright terms: Public domain W3C validator