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

Theorem ltle 8910
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 8908 . 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 1623    e. wcel 1684   class class class wbr 4023   RRcr 8736    < clt 8867    <_ cle 8868
This theorem is referenced by:  letr  8914  letric  8921  ltlen  8922  ltlei  8940  ltled  8967  lt2add  9259  lep1  9595  lem1  9597  letrp1  9598  ltmul12a  9612  lediv12a  9649  bndndx  9964  uzind  10103  fnn0ind  10111  eluz2b2  10290  lbzbi  10306  zmin  10312  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  rpge0  10366  rpneg  10383  iccsplit  10768  elfzouz2  10888  fzostep1  10922  fllep1  10933  fracle1  10935  expgt1  11140  expnbnd  11230  expnlbnd2  11232  faclbnd  11303  resqrex  11736  sqrgt0  11744  absmax  11813  eqsqr2d  11852  rlim2lt  11971  mulcn2  12069  rlimo1  12090  o1rlimmul  12092  caucvgrlem  12145  supcvg  12314  efcllem  12359  sin01bnd  12465  cos01bnd  12466  sin01gt0  12470  cos01gt0  12471  absef  12477  efieq1re  12479  ruclem11  12518  pythagtriplem12  12879  pythagtriplem13  12880  pythagtriplem14  12881  pythagtriplem16  12883  pclem  12891  isabvd  15585  met2ndci  18068  blcvx  18304  icoopnst  18437  iocopnst  18438  nmoleub2a  18598  nmoleub2b  18599  nmhmcn  18601  iscmet3lem2  18718  caubl  18733  ivthlem2  18812  ovolicc2lem4  18879  ioombl1lem4  18918  volsup2  18960  itg2monolem1  19105  itg2gt0  19115  itg2cnlem1  19116  dvne0  19358  ftc1lem4  19386  dgrlt  19647  aalioulem5  19716  ulmbdd  19775  iblulm  19783  radcnvlem1  19789  abelthlem5  19811  abelthlem7  19814  sincosq1lem  19865  tangtx  19873  tanabsge  19874  sinq12ge0  19876  sineq0  19889  tanord  19900  logcj  19960  argregt0  19964  argrege0  19965  argimgt0  19966  logdmnrp  19988  logcnlem3  19991  logf1o2  19997  cxpsqrlem  20049  abscxpbnd  20093  logreclem  20116  asinneg  20182  atanlogsublem  20211  atanlogsub  20212  rlimcnp  20260  xrlimcnp  20263  basellem8  20325  chtub  20451  bposlem9  20531  chebbnd1  20621  chtppilimlem1  20622  dchrvmasumiflem1  20650  mulog2sumlem2  20684  pntrmax  20713  pntibndlem2  20740  pntibndlem3  20741  pntlemf  20754  nmblolbii  21377  ubthlem1  21449  bcsiALT  21758  nmbdoplbi  22604  nmcexi  22606  nmcoplbi  22608  lnconi  22613  nmbdfnlbi  22629  nmcfnlbi  22632  nmopcoi  22675  branmfn  22685  leopmul  22714  nmopleid  22719  ballotlemsgt1  23069  ballotlemfrceq  23087  ballotlemfrcn0  23088  esumcvg  23454  sinccvglem  24005  mulge0b  24086  axlowdimlem16  24585  mslb1  25607  2wsms  25608  lvsovso  25626  opnrebl2  26236  ivthALT  26258  incsequz2  26459  nnubfi  26460  bfplem2  26547  pell14qrgap  26960  pellfundre  26966  pellfundlb  26969  ioovolcl  27742  itgsin0pilem1  27744  itgsinexplem1  27748  stoweidlem1  27750  stoweidlem3  27752  stoweidlem7  27756  stoweidlem17  27766  stoweidlem24  27773  stoweidlem26  27775  stoweidlem34  27783  stoweidlem42  27791  wallispilem1  27814  wallispilem2  27815  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2  27822  stirlinglem15  27837
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-resscn 8794  ax-pre-lttri 8811
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873
  Copyright terms: Public domain W3C validator