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

Theorem ltnle 9663
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 9662 . . 3  |-  ( ( B  e.  RR  /\  A  e.  RR )  ->  ( B  <_  A  <->  -.  A  <  B ) )
21ancoms 453 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( B  <_  A  <->  -.  A  <  B ) )
32con2bid 329 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1767   class class class wbr 4447   RRcr 9490    < clt 9627    <_ cle 9628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-cnv 5007  df-xr 9631  df-le 9633
This theorem is referenced by:  letric  9684  ltnled  9730  leaddsub  10027  mulge0b  10411  nn0n0n1ge2b  10859  znnnlt1  10890  uzwo  11143  uzwoOLD  11144  qsqueeze  11399  difreicc  11651  fzp1disj  11737  fzneuz  11758  fznuz  11759  uznfz  11760  difelfznle  11785  ssfzoulel  11873  elfzonelfzo  11879  ssnn0fi  12061  discr1  12269  facdiv  12332  bcval5  12363  wrdsymb0  12539  ccatsymb  12564  swrdnd  12619  swrdvalodm2  12626  swrdspsleq  12635  swrdccat3  12679  repswswrd  12718  cnpart  13035  absmax  13124  rlimrege0  13364  znnenlem  13805  rpnnen2  13819  alzdvds  13894  algcvgblem  14064  pcprendvds  14222  pcdvdsb  14250  pcmpt  14269  prmunb  14290  prmreclem2  14293  prmlem1  14450  prmlem2  14462  lt6abl  16697  metdseq0  21109  xrhmeo  21197  ovolicc2lem3  21681  itg2seq  21900  dvne0  22163  coeeulem  22372  radcnvlt1  22563  argimgt0  22741  cxple2  22822  ressatans  23009  basellem2  23099  issqf  23154  bpos1  23302  bposlem3  23305  bposlem6  23308  pntpbnd2  23516  ostth2lem4  23565  eldmgm  28220  ltflcei  29636  mblfinlem1  29644  mbfposadd  29655  itgaddnclem2  29667  ftc1anclem1  29683  ftc1anclem5  29687  dvasin  29696  divlt0gt0d  31062  icccncfext  31242  stoweidlem14  31330  stoweidlem34  31350  dirkercncflem1  31419  ltnltne  31804  ply1mulgsumlem2  32077
  Copyright terms: Public domain W3C validator