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

Theorem ltnle 9454
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 9453 . . 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 1756   class class class wbr 4292   RRcr 9281    < clt 9418    <_ cle 9419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-xp 4846  df-cnv 4848  df-xr 9422  df-le 9424
This theorem is referenced by:  letric  9475  ltnled  9521  leaddsub  9815  mulge0b  10199  nn0n0n1ge2b  10644  znnnlt1  10673  uzwo  10917  uzwoOLD  10918  qsqueeze  11171  difreicc  11417  fzp1disj  11515  fzneuz  11541  fznuz  11542  uznfz  11543  ssfzoulel  11621  elfzonelfzo  11627  discr1  12000  facdiv  12063  bcval5  12094  wrdsymb0  12259  ccatsymb  12281  swrdnd  12326  swrdvalodm2  12333  swrdspsleq  12342  swrdccat3  12383  repswswrd  12422  cnpart  12729  absmax  12817  rlimrege0  13057  znnenlem  13494  rpnnen2  13508  alzdvds  13583  algcvgblem  13752  pcprendvds  13907  pcdvdsb  13935  pcmpt  13954  prmunb  13975  prmreclem2  13978  prmlem1  14135  prmlem2  14147  lt6abl  16371  metdseq0  20430  xrhmeo  20518  ovolicc2lem3  21002  itg2seq  21220  dvne0  21483  coeeulem  21692  radcnvlt1  21883  argimgt0  22061  cxple2  22142  ressatans  22329  basellem2  22419  issqf  22474  bpos1  22622  bposlem3  22625  bposlem6  22628  pntpbnd2  22836  ostth2lem4  22885  eldmgm  27008  ltflcei  28419  mblfinlem1  28428  mbfposadd  28439  itgaddnclem2  28451  ftc1anclem1  28467  ftc1anclem5  28471  dvasin  28480  stoweidlem14  29809  stoweidlem34  29829  ltnltne  30176  difelfznle  30488  ssnn0fi  30746  ply1mulgsumlem2  30845
  Copyright terms: Public domain W3C validator