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

Theorem xrlenlt 9546
Description: 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
xrlenlt  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )

Proof of Theorem xrlenlt
StepHypRef Expression
1 df-br 4394 . . 3  |-  ( A  <_  B  <->  <. A ,  B >.  e.  <_  )
2 opelxpi 4972 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  <. A ,  B >.  e.  ( RR*  X. 
RR* ) )
3 df-le 9528 . . . . . . 7  |-  <_  =  ( ( RR*  X.  RR* )  \  `'  <  )
43eleq2i 2529 . . . . . 6  |-  ( <. A ,  B >.  e. 
<_ 
<-> 
<. A ,  B >.  e.  ( ( RR*  X.  RR* )  \  `'  <  )
)
5 eldif 3439 . . . . . 6  |-  ( <. A ,  B >.  e.  ( ( RR*  X.  RR* )  \  `'  <  )  <->  (
<. A ,  B >.  e.  ( RR*  X.  RR* )  /\  -.  <. A ,  B >.  e.  `'  <  )
)
64, 5bitri 249 . . . . 5  |-  ( <. A ,  B >.  e. 
<_ 
<->  ( <. A ,  B >.  e.  ( RR*  X.  RR* )  /\  -.  <. A ,  B >.  e.  `'  <  ) )
76baib 896 . . . 4  |-  ( <. A ,  B >.  e.  ( RR*  X.  RR* )  ->  ( <. A ,  B >.  e.  <_  <->  -.  <. A ,  B >.  e.  `'  <  ) )
82, 7syl 16 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( <. A ,  B >.  e. 
<_ 
<->  -.  <. A ,  B >.  e.  `'  <  )
)
91, 8syl5bb 257 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  <. A ,  B >.  e.  `'  <  ) )
10 opelcnvg 5120 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( <. A ,  B >.  e.  `'  <  <->  <. B ,  A >.  e.  <  ) )
11 df-br 4394 . . . 4  |-  ( B  <  A  <->  <. B ,  A >.  e.  <  )
1210, 11syl6rbbr 264 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( B  <  A  <->  <. A ,  B >.  e.  `'  <  ) )
1312notbid 294 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( -.  B  <  A  <->  -.  <. A ,  B >.  e.  `'  <  ) )
149, 13bitr4d 256 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 1758    \ cdif 3426   <.cop 3984   class class class wbr 4393    X. cxp 4939   `'ccnv 4940   RR*cxr 9521    < clt 9522    <_ cle 9523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-br 4394  df-opab 4452  df-xp 4947  df-cnv 4949  df-le 9528
This theorem is referenced by:  xrltnle  9547  lenlt  9557  pnfge  11214  mnfle  11217  xrleloe  11225  xrltlen  11227  xrletri3  11233  xralrple  11279  xleneg  11292  supxr2  11380  supxrbnd1  11388  supxrbnd2  11389  supxrub  11391  supxrleub  11393  supxrbnd  11395  infmxrlb  11400  infmxrgelb  11401  ixxub  11425  ixxlb  11426  ioon0  11430  iccid  11449  icc0  11452  icoun  11519  icodisj  11520  snunico  11522  ioodisj  11525  ioojoin  11526  supicclub2  11546  hashgt0elex  12270  hashgt12el  12284  hashgt12el2  12285  lecldbas  18948  xmetgt0  20058  bldisj  20098  icopnfcld  20472  icombl  21171  ioombl  21172  ioorcl2  21178  vitalilem4  21217  itg2gt0  21364  ply1divmo  21733  ig1peu  21769  radcnvle  22011  psercnlem1  22016  nmlnogt0  24342  xgepnf  26187  xlemnf  26188  xrlelttric  26189  xrsupssd  26196  xrge0infss  26197  xrge0infssd  26198  joiniooico  26202  xeqlelt  26204  iocinif  26209  esumsn  26653  oms0  26847  mblfinlem3  28571  mblfinlem4  28572  ismblfin  28573  asindmre  28620  ioounsn  29726  iocmbl  29729  0rngnnzr  30919
  Copyright terms: Public domain W3C validator