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

Theorem ltnle 8902
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 8901 . . 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 1684   class class class wbr 4023   RRcr 8736    < clt 8867    <_ cle 8868
This theorem is referenced by:  letric  8921  ltnled  8966  leaddsub  9250  znnnlt1  10050  uzwo  10281  uzwoOLD  10282  qsqueeze  10528  difreicc  10767  fzp1disj  10843  fzneuz  10863  fznuz  10864  uznfz  10865  discr1  11237  facdiv  11300  bcval5  11330  cnpart  11725  absmax  11813  rlimrege0  12053  znnenlem  12490  rpnnen2  12504  alzdvds  12578  algcvgblem  12747  pcprendvds  12893  pcdvdsb  12921  pcmpt  12940  prmunb  12961  prmreclem2  12964  prmlem1  13109  prmlem2  13121  lt6abl  15181  metdseq0  18358  xrhmeo  18444  ovolicc2lem3  18878  itg2seq  19097  dvne0  19358  coeeulem  19606  radcnvlt1  19794  argimgt0  19966  cxple2  20044  ressatans  20230  basellem2  20319  issqf  20374  bpos1  20522  bposlem3  20525  bposlem6  20528  pntpbnd2  20736  ostth2lem4  20785  eldmgm  23694  mulge0b  24086  stoweidlem14  27763  stoweidlem26  27775  stoweidlem34  27783
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