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

Theorem ltle 8997
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 374 . 2  |-  ( A  <  B  ->  ( A  <  B  \/  A  =  B ) )
2 leloe 8995 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  ( A  <  B  \/  A  =  B )
) )
31, 2syl5ibr 212 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    /\ wa 358    = wceq 1642    e. wcel 1710   class class class wbr 4102   RRcr 8823    < clt 8954    <_ cle 8955
This theorem is referenced by:  letr  9001  letric  9008  ltlen  9009  ltlei  9027  ltled  9054  lt2add  9346  lep1  9682  lem1  9684  letrp1  9685  ltmul12a  9699  lediv12a  9736  bndndx  10053  uzind  10192  fnn0ind  10200  eluz2b2  10379  lbzbi  10395  zmin  10401  rpnnen1lem1  10431  rpnnen1lem2  10432  rpnnen1lem3  10433  rpnnen1lem5  10435  rpge0  10455  rpneg  10472  iccsplit  10857  elfzouz2  10977  fzostep1  11011  fllep1  11022  fracle1  11024  expgt1  11230  expnbnd  11320  expnlbnd2  11322  faclbnd  11393  resqrex  11826  sqrgt0  11834  absmax  11903  eqsqr2d  11942  rlim2lt  12061  mulcn2  12159  rlimo1  12180  o1rlimmul  12182  climbdd  12235  caucvgrlem  12236  supcvg  12405  efcllem  12450  sin01bnd  12556  cos01bnd  12557  sin01gt0  12561  cos01gt0  12562  absef  12568  efieq1re  12570  ruclem11  12609  pythagtriplem12  12970  pythagtriplem13  12971  pythagtriplem14  12972  pythagtriplem16  12974  pclem  12982  isabvd  15678  met2ndci  18164  blcvx  18400  icoopnst  18535  iocopnst  18536  nmoleub2a  18696  nmoleub2b  18697  nmhmcn  18699  iscmet3lem2  18816  caubl  18831  ivthlem2  18910  ovolicc2lem4  18977  ioombl1lem4  19016  volsup2  19058  itg2monolem1  19203  itg2gt0  19213  itg2cnlem1  19214  dvne0  19456  ftc1lem4  19484  dgrlt  19745  aalioulem5  19814  ulmbdd  19875  iblulm  19884  radcnvlem1  19890  abelthlem5  19912  abelthlem7  19915  sincosq1lem  19966  tangtx  19974  tanabsge  19975  sinq12ge0  19977  sineq0  19990  tanord  20001  logcj  20062  argregt0  20066  argrege0  20067  argimgt0  20068  logdmnrp  20093  logcnlem3  20096  logf1o2  20102  cxpsqrlem  20154  abscxpbnd  20198  logreclem  20221  asinneg  20287  atanlogsublem  20316  atanlogsub  20317  rlimcnp  20365  xrlimcnp  20368  basellem8  20431  chtub  20557  bposlem9  20637  chebbnd1  20727  chtppilimlem1  20728  dchrvmasumiflem1  20756  mulog2sumlem2  20790  pntrmax  20819  pntibndlem2  20846  pntibndlem3  20847  pntlemf  20860  nmblolbii  21485  ubthlem1  21557  bcsiALT  21866  nmbdoplbi  22712  nmcexi  22714  nmcoplbi  22716  lnconi  22721  nmbdfnlbi  22737  nmcfnlbi  22740  nmopcoi  22783  branmfn  22793  leopmul  22822  nmopleid  22827  esumcvg  23742  ballotlemsgt1  24017  ballotlemfrceq  24035  ballotlemfrcn0  24036  sinccvglem  24409  mulge0b  24492  axlowdimlem16  25144  ltflcei  25485  itg2addnclem  25492  itg2addnc  25494  ftc1cnnclem  25513  opnrebl2  25560  ivthALT  25582  incsequz2  25783  nnubfi  25784  bfplem2  25870  pell14qrgap  26283  pellfundre  26289  pellfundlb  26292  ioovolcl  27065  itgsin0pilem1  27067  itgsinexplem1  27071  stoweidlem1  27073  stoweidlem3  27075  stoweidlem7  27079  stoweidlem17  27089  stoweidlem24  27096  stoweidlem26  27098  stoweidlem34  27106  stoweidlem42  27114  wallispilem1  27137  wallispilem2  27138  wallispilem4  27140  wallispilem5  27141  wallispi  27142  wallispi2  27145  stirlinglem15  27160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-resscn 8881  ax-pre-lttri 8898
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-mpt 4158  df-id 4388  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-er 6744  df-en 6949  df-dom 6950  df-sdom 6951  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960
  Copyright terms: Public domain W3C validator