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

Theorem ltle 9194
Description: 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
Assertion
Ref Expression
ltle  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)

Proof of Theorem ltle
StepHypRef Expression
1 orc 376 . 2  |-  ( A  <  B  ->  ( A  <  B  \/  A  =  B ) )
2 leloe 9192 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  ( A  <  B  \/  A  =  B )
) )
31, 2syl5ibr 214 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359    /\ wa 360    = wceq 1653    e. wcel 1727   class class class wbr 4237   RRcr 9020    < clt 9151    <_ cle 9152
This theorem is referenced by:  letr  9198  letric  9205  ltlen  9206  ltlei  9226  ltled  9252  lt2add  9544  lep1  9880  lem1  9882  letrp1  9883  ltmul12a  9897  lediv12a  9934  bndndx  10251  uzind  10392  fnn0ind  10400  eluz2b2  10579  lbzbi  10595  zmin  10601  rpnnen1lem1  10631  rpnnen1lem2  10632  rpnnen1lem3  10633  rpnnen1lem5  10635  rpge0  10655  rpneg  10672  iccsplit  11060  elfzouz2  11184  fzostep1  11228  fllep1  11241  fracle1  11243  expgt1  11449  expnbnd  11539  expnlbnd2  11541  faclbnd  11612  resqrex  12087  sqrgt0  12095  absmax  12164  eqsqr2d  12203  rlim2lt  12322  mulcn2  12420  rlimo1  12441  o1rlimmul  12443  climbdd  12496  caucvgrlem  12497  supcvg  12666  efcllem  12711  sin01bnd  12817  cos01bnd  12818  sin01gt0  12822  cos01gt0  12823  absef  12829  efieq1re  12831  ruclem11  12870  pythagtriplem12  13231  pythagtriplem13  13232  pythagtriplem14  13233  pythagtriplem16  13235  pclem  13243  isabvd  15939  met2ndci  18583  blcvx  18860  icoopnst  18995  iocopnst  18996  nmoleub2a  19156  nmoleub2b  19157  nmhmcn  19159  iscmet3lem2  19276  caubl  19291  ivthlem2  19380  ovolicc2lem4  19447  ioombl1lem4  19486  volsup2  19528  itg2monolem1  19671  itg2gt0  19681  itg2cnlem1  19682  dvne0  19926  ftc1lem4  19954  dgrlt  20215  aalioulem5  20284  ulmbdd  20345  iblulm  20354  radcnvlem1  20360  abelthlem5  20382  abelthlem7  20385  sincosq1lem  20436  tangtx  20444  tanabsge  20445  sinq12ge0  20447  sineq0  20460  tanord  20471  logcj  20532  argregt0  20536  argrege0  20537  argimgt0  20538  logdmnrp  20563  logcnlem3  20566  logf1o2  20572  cxpsqrlem  20624  abscxpbnd  20668  logreclem  20691  asinneg  20757  atanlogsublem  20786  atanlogsub  20787  rlimcnp  20835  xrlimcnp  20838  basellem8  20901  chtub  21027  bposlem9  21107  chebbnd1  21197  chtppilimlem1  21198  dchrvmasumiflem1  21226  mulog2sumlem2  21260  pntrmax  21289  pntibndlem2  21316  pntibndlem3  21317  pntlemf  21330  nmblolbii  22331  ubthlem1  22403  bcsiALT  22712  nmbdoplbi  23558  nmcexi  23560  nmcoplbi  23562  lnconi  23567  nmbdfnlbi  23583  nmcfnlbi  23586  nmopcoi  23629  branmfn  23639  leopmul  23668  nmopleid  23673  esumcvg  24507  ballotlemfrceq  24817  sinccvglem  25140  mulge0b  25222  axlowdimlem16  25927  ltflcei  26271  ftc1cnnclem  26316  ftc1anclem5  26322  opnrebl2  26362  ivthALT  26376  incsequz2  26491  nnubfi  26492  bfplem2  26570  pell14qrgap  26976  pellfundre  26982  pellfundlb  26985  ioovolcl  27756  stoweidlem17  27780  stoweidlem34  27797  wallispilem1  27828  ltsubnn0  28144  2elfz2melfz  28164  ubmelfzo  28173  ubmelm1fzo  28174  subsubelfzo0  28182  swrdccat3  28273  cshwoor  28295  2cshw2lem1  28310  2cshw2lem2  28311  2cshwmod  28315  cshwssizelem4a  28341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-resscn 9078  ax-pre-lttri 9095
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-mpt 4293  df-id 4527  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-er 6934  df-en 7139  df-dom 7140  df-sdom 7141  df-pnf 9153  df-mnf 9154  df-xr 9155  df-ltxr 9156  df-le 9157
  Copyright terms: Public domain W3C validator