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

Theorem ltnle 9111
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 9110 . . 3  |-  ( ( B  e.  RR  /\  A  e.  RR )  ->  ( B  <_  A  <->  -.  A  <  B ) )
21ancoms 440 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( B  <_  A  <->  -.  A  <  B ) )
32con2bid 320 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    e. wcel 1721   class class class wbr 4172   RRcr 8945    < clt 9076    <_ cle 9077
This theorem is referenced by:  letric  9130  ltnled  9176  leaddsub  9460  nn0n0n1ge2b  10237  znnnlt1  10264  uzwo  10495  uzwoOLD  10496  qsqueeze  10743  difreicc  10984  fzp1disj  11061  fzneuz  11083  fznuz  11084  uznfz  11085  discr1  11470  facdiv  11533  bcval5  11564  cnpart  12000  absmax  12088  rlimrege0  12328  znnenlem  12766  rpnnen2  12780  alzdvds  12854  algcvgblem  13023  pcprendvds  13169  pcdvdsb  13197  pcmpt  13216  prmunb  13237  prmreclem2  13240  prmlem1  13385  prmlem2  13397  lt6abl  15459  metdseq0  18837  xrhmeo  18924  ovolicc2lem3  19368  itg2seq  19587  dvne0  19848  coeeulem  20096  radcnvlt1  20287  argimgt0  20460  cxple2  20541  ressatans  20727  basellem2  20817  issqf  20872  bpos1  21020  bposlem3  21023  bposlem6  21026  pntpbnd2  21234  ostth2lem4  21283  eldmgm  24759  mulge0b  25144  ltflcei  26140  mblfinlem  26143  mbfposadd  26153  itgaddnclem2  26163  stoweidlem14  27630  stoweidlem34  27650  elfzonelfzo  27992  swrdnd  28001  swrdccat3  28029
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-cnv 4845  df-xr 9080  df-le 9082
  Copyright terms: Public domain W3C validator