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

Theorem ltnle 8947
Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)
Assertion
Ref Expression
ltnle  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)

Proof of Theorem ltnle
StepHypRef Expression
1 lenlt 8946 . . 3  |-  ( ( B  e.  RR  /\  A  e.  RR )  ->  ( B  <_  A  <->  -.  A  <  B ) )
21ancoms 439 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( B  <_  A  <->  -.  A  <  B ) )
32con2bid 319 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 1701   class class class wbr 4060   RRcr 8781    < clt 8912    <_ cle 8913
This theorem is referenced by:  letric  8966  ltnled  9011  leaddsub  9295  znnnlt1  10097  uzwo  10328  uzwoOLD  10329  qsqueeze  10575  difreicc  10814  fzp1disj  10890  fzneuz  10910  fznuz  10911  uznfz  10912  discr1  11284  facdiv  11347  bcval5  11377  cnpart  11772  absmax  11860  rlimrege0  12100  znnenlem  12537  rpnnen2  12551  alzdvds  12625  algcvgblem  12794  pcprendvds  12940  pcdvdsb  12968  pcmpt  12987  prmunb  13008  prmreclem2  13011  prmlem1  13156  prmlem2  13168  lt6abl  15230  metdseq0  18410  xrhmeo  18497  ovolicc2lem3  18931  itg2seq  19150  dvne0  19411  coeeulem  19659  radcnvlt1  19847  argimgt0  20019  cxple2  20097  ressatans  20283  basellem2  20372  issqf  20427  bpos1  20575  bposlem3  20578  bposlem6  20581  pntpbnd2  20789  ostth2lem4  20838  eldmgm  23978  mulge0b  24372  ltflcei  25312  itgaddnclem2  25324  stoweidlem14  26911  stoweidlem26  26923  stoweidlem34  26931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061  df-opab 4115  df-xp 4732  df-cnv 4734  df-xr 8916  df-le 8918
  Copyright terms: Public domain W3C validator