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

Theorem lenlt 9714
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 9688 . 2  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9688 . 2  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xrlenlt 9701 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2an 480 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    e. wcel 1869   class class class wbr 4421   RRcr 9540   RR*cxr 9676    < clt 9677    <_ cle 9678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-xp 4857  df-cnv 4859  df-xr 9681  df-le 9683
This theorem is referenced by:  ltnle  9715  letri3  9721  leloe  9722  eqlelt  9723  ne0gt0  9741  lelttric  9743  lenlti  9756  lenltd  9783  ltaddsub  10090  leord1  10143  lediv1  10472  suprleub  10575  dfinfre  10590  dfinfmrOLD  10591  infregelb  10596  infmrgelbOLD  10597  nnge1  10637  nnnlt1  10641  avgle1  10854  avgle2  10855  nn0nlt0  10898  recnz  11013  btwnnz  11014  prime  11018  indstr  11229  uzsupss  11258  zbtwnre  11264  rpneg  11334  fzn  11817  nelfzo  11927  fzonlt0  11943  fllt  12043  flflp1  12044  modifeq2int  12153  om2uzlt2i  12166  fsuppmapnn0fiub0  12206  suppssfz  12207  leexp2  12328  discr  12410  bcval4  12493  ccatsymb  12725  swrd0  12786  sqrtneglem  13324  harmonic  13910  efle  14165  dvdsle  14343  lcmf  14599  infpnlem1  14847  pgpssslw  17259  gsummoncoe1  18891  mp2pm2mplem4  19825  dvferm1  22929  dvferm2  22931  dgrlt  23212  logleb  23544  argrege0  23552  ellogdm  23576  dvlog2lem  23589  cxple  23632  cxple3  23638  asinneg  23804  birthdaylem3  23871  ppieq0  24095  chpeq0  24128  chteq0  24129  lgsval2lem  24226  lgsneg  24239  lgsdilem  24242  ostth2lem1  24448  ostth3  24468  clwlkisclwwlklem2a  25505  rusgranumwlks  25676  frgrareg  25837  friendship  25842  nmounbi  26409  nmlno0lem  26426  nmlnop0iALT  27640  supfz  30363  inffz  30364  fz0n  30365  nn0prpw  30978  leceifl  31854  poimirlem15  31875  poimirlem16  31876  poimirlem17  31877  poimirlem20  31880  poimirlem24  31884  poimirlem31  31891  poimirlem32  31892  ftc1anclem1  31937  nninfnub  32000  ellz1  35534  rencldnfilem  35588  icccncfext  37591  subsubelfzo0  38757  digexp  39724
  Copyright terms: Public domain W3C validator