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

Theorem ltleii 9028
Description: 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)
Hypotheses
Ref Expression
lt.1  |-  A  e.  RR
lt.2  |-  B  e.  RR
ltlei.1  |-  A  < 
B
Assertion
Ref Expression
ltleii  |-  A  <_  B

Proof of Theorem ltleii
StepHypRef Expression
1 ltlei.1 . 2  |-  A  < 
B
2 lt.1 . . 3  |-  A  e.  RR
3 lt.2 . . 3  |-  B  e.  RR
42, 3ltlei 9027 . 2  |-  ( A  <  B  ->  A  <_  B )
51, 4ax-mp 8 1  |-  A  <_  B
Colors of variables: wff set class
Syntax hints:    e. wcel 1710   class class class wbr 4102   RRcr 8823    < clt 8954    <_ cle 8955
This theorem is referenced by:  0le1  9384  ledivp1i  9769  ltdivp1i  9770  expubnd  11252  faclbnd4lem1  11396  sqr4  11848  sqr9  11849  sqr2gt1lt2  11850  absrdbnd  11915  sqreulem  11933  amgm2  11943  sqrpclii  11956  climcndslem1  12399  climcndslem2  12400  geo2lim  12422  0.999...  12428  efcllem  12450  ege2le3  12462  ef01bndlem  12555  sin01bnd  12556  cos01bnd  12557  cos2bnd  12559  sin01gt0  12561  rpnnen2lem3  12586  rpnnen2lem4  12587  rpnnen2lem9  12592  rpnnen2  12595  bitsp1o  12715  bitsmod  12718  isprm3  12858  strlemor1  13326  strleun  13329  abvtrivd  15698  iihalf1  18527  elii1  18531  htpycc  18576  pcoval1  18609  pco0  18610  pcoval2  18612  pcocn  18613  pcohtpylem  18615  pcopt  18618  pcopt2  18619  pcoass  18620  pcorevlem  18622  minveclem2  18888  vitalilem4  19064  vitali  19066  mbfi1fseqlem6  19173  iblcnlem1  19240  dveflem  19424  aaliou3lem2  19821  aaliou3lem8  19823  sinhalfpilem  19935  sincosq1lem  19966  sincos4thpi  19982  tan4thpi  19983  sincos6thpi  19984  tanregt0  20002  efif1olem4  20008  relogrn  20020  argregt0  20066  argrege0  20067  logneg2  20071  asin1  20295  reasinsin  20297  log2cnv  20345  log2tlbnd  20346  log2ub  20350  harmonicbnd3  20407  ppisval  20447  ppiublem1  20547  ppiub  20549  bcmono  20622  bposlem1  20629  bposlem3  20631  bposlem4  20632  bposlem5  20633  bposlem7  20635  bposlem8  20636  bposlem9  20637  lgsdir2lem1  20668  m1lgs  20707  2sqlem11  20720  chebbnd1lem3  20726  chpchtlim  20734  dchrvmasumlem2  20753  dchrvmasumlema  20755  dchrvmasumiflem1  20756  logdivsum  20788  mulog2sumlem2  20790  log2sumbnd  20799  chpdifbndlem1  20808  pntpbnd1a  20840  pntpbnd2  20842  pntibndlem3  20847  pntlemk  20861  ex-fl  20940  ipidsq  21394  minvecolem2  21562  normlem6  21802  normpar2i  21843  sqsscirc1  23462  rnlogblem  23665  konigsberg  24315  4bc2eq6  24505  axlowdimlem3  25131  axlowdimlem6  25134  axlowdimlem7  25135  axlowdimlem16  25144  axlowdimlem17  25145  axlowdim  25148  fdc  25779  heiborlem8  25865  jm2.20nn  26413  lhe4.4ex1a  26869  stirlinglem11  27156  stirlinglem15  27160  stirlingr  27162  fzo0to42pr  27456  4fvwrd4  27491  usgraexvlem  27560  usgraex0elv  27561  usgraex1elv  27562  usgraex2elv  27563  usgraex3elv  27564  constr3pthlem3  27764  4cycl4v4e  27773  4cycl4dv4e  27775
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