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

Theorem xrlenlt 9673
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

Proof of Theorem xrlenlt
StepHypRef Expression
1 df-br 4453 . . 3
2 opelxpi 5036 . . . 4
3 df-le 9655 . . . . . . 7
43eleq2i 2535 . . . . . 6
5 eldif 3485 . . . . . 6
64, 5bitri 249 . . . . 5
76baib 903 . . . 4
82, 7syl 16 . . 3
91, 8syl5bb 257 . 2
10 opelcnvg 5187 . . . 4
11 df-br 4453 . . . 4
1210, 11syl6rbbr 264 . . 3
1312notbid 294 . 2
149, 13bitr4d 256 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818  \cdif 3472  <.cop 4035   class class class wbr 4452  X.cxp 5002  `'ccnv 5003   cxr 9648   clt 9649   cle 9650
This theorem is referenced by:  xrltnle  9674  lenlt  9684  pnfge  11368  mnfle  11371  xrleloe  11379  xrltlen  11381  xrletri3  11387  xralrple  11433  xleneg  11446  supxr2  11534  supxrbnd1  11542  supxrbnd2  11543  supxrub  11545  supxrleub  11547  supxrbnd  11549  infmxrlb  11554  infmxrgelb  11555  ixxub  11579  ixxlb  11580  ioon0  11584  iccid  11603  icc0  11606  icoun  11673  icodisj  11674  snunico  11676  ioodisj  11679  ioojoin  11680  supicclub2  11700  hashgt0elex  12466  hashgt12el  12481  hashgt12el2  12482  0ringnnzr  17917  lecldbas  19720  xmetgt0  20861  bldisj  20901  icopnfcld  21275  icombl  21974  ioombl  21975  ioorcl2  21981  vitalilem4  22020  itg2gt0  22167  ply1divmo  22536  ig1peu  22572  radcnvle  22815  psercnlem1  22820  nmlnogt0  25712  xgepnf  27570  xlemnf  27571  xrlelttric  27572  xrsupssd  27579  xrge0infss  27580  xrge0infssd  27581  joiniooico  27585  xeqlelt  27587  iocinif  27592  esumsn  28072  oms0  28266  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  asindmre  30102  ioounsn  31177  iocmbl  31180  xrnltled  31488  snunioo2  31544  iccdifprioo  31556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-cnv 5012  df-le 9655
  Copyright terms: Public domain W3C validator