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

Theorem xrlenlt 9650
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 4434 . . 3  |-  ( A  <_  B  <->  <. A ,  B >.  e.  <_  )
2 opelxpi 5017 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  <. A ,  B >.  e.  ( RR*  X. 
RR* ) )
3 df-le 9632 . . . . . . 7  |-  <_  =  ( ( RR*  X.  RR* )  \  `'  <  )
43eleq2i 2519 . . . . . 6  |-  ( <. A ,  B >.  e. 
<_ 
<-> 
<. A ,  B >.  e.  ( ( RR*  X.  RR* )  \  `'  <  )
)
5 eldif 3468 . . . . . 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 901 . . . 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 5168 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( <. A ,  B >.  e.  `'  <  <->  <. B ,  A >.  e.  <  ) )
11 df-br 4434 . . . 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 1802    \ cdif 3455   <.cop 4016   class class class wbr 4433    X. cxp 4983   `'ccnv 4984   RR*cxr 9625    < clt 9626    <_ cle 9627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434  df-opab 4492  df-xp 4991  df-cnv 4993  df-le 9632
This theorem is referenced by:  xrltnle  9651  lenlt  9661  pnfge  11343  mnfle  11346  xrleloe  11354  xrltlen  11356  xrletri3  11362  xralrple  11408  xleneg  11421  supxr2  11509  supxrbnd1  11517  supxrbnd2  11518  supxrub  11520  supxrleub  11522  supxrbnd  11524  infmxrlb  11529  infmxrgelb  11530  ixxub  11554  ixxlb  11555  ioon0  11559  iccid  11578  icc0  11581  icoun  11648  icodisj  11649  snunico  11651  ioodisj  11654  ioojoin  11655  supicclub2  11675  hashgt0elex  12440  hashgt12el  12455  hashgt12el2  12456  0ringnnzr  17785  lecldbas  19586  xmetgt0  20727  bldisj  20767  icopnfcld  21141  icombl  21840  ioombl  21841  ioorcl2  21847  vitalilem4  21886  itg2gt0  22033  ply1divmo  22402  ig1peu  22438  radcnvle  22680  psercnlem1  22685  nmlnogt0  25577  xgepnf  27435  xlemnf  27436  xrlelttric  27437  xrsupssd  27444  xrge0infss  27445  xrge0infssd  27446  joiniooico  27450  xeqlelt  27452  iocinif  27457  esumsn  27938  oms0  28132  mblfinlem3  30021  mblfinlem4  30022  ismblfin  30023  asindmre  30070  ioounsn  31146  iocmbl  31149  xrnltled  31433  snunioo2  31476  iccdifprioo  31488
  Copyright terms: Public domain W3C validator