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

Theorem ltleii 9227
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 9226 . 2  |-  ( A  <  B  ->  A  <_  B )
51, 4ax-mp 5 1  |-  A  <_  B
Colors of variables: wff set class
Syntax hints:    e. wcel 1727   class class class wbr 4237   RRcr 9020    < clt 9151    <_ cle 9152
This theorem is referenced by:  0le1  9582  ledivp1i  9967  ltdivp1i  9968  4fvwrd4  11152  fzo0to42pr  11217  expubnd  11471  faclbnd4lem1  11615  sqr4  12109  sqr9  12110  sqr2gt1lt2  12111  absrdbnd  12176  sqreulem  12194  amgm2  12204  sqrpclii  12217  climcndslem1  12660  climcndslem2  12661  geo2lim  12683  0.999...  12689  efcllem  12711  ege2le3  12723  ef01bndlem  12816  sin01bnd  12817  cos01bnd  12818  cos2bnd  12820  sin01gt0  12822  rpnnen2lem3  12847  rpnnen2lem4  12848  rpnnen2lem9  12853  rpnnen2  12856  bitsp1o  12976  bitsmod  12979  isprm3  13119  strlemor1  13587  strleun  13590  abvtrivd  15959  iihalf1  18987  elii1  18991  htpycc  19036  pcoval1  19069  pco0  19070  pcoval2  19072  pcocn  19073  pcohtpylem  19075  pcopt  19078  pcopt2  19079  pcoass  19080  pcorevlem  19082  minveclem2  19358  vitalilem4  19534  vitali  19536  mbfi1fseqlem6  19641  iblcnlem1  19708  dveflem  19894  aaliou3lem2  20291  aaliou3lem8  20293  sinhalfpilem  20405  sincosq1lem  20436  sincos4thpi  20452  tan4thpi  20453  sincos6thpi  20454  tanregt0  20472  efif1olem4  20478  relogrn  20490  argregt0  20536  argrege0  20537  logneg2  20541  asin1  20765  reasinsin  20767  log2cnv  20815  log2tlbnd  20816  log2ub  20820  harmonicbnd3  20877  ppisval  20917  ppiublem1  21017  ppiub  21019  bcmono  21092  bposlem1  21099  bposlem3  21101  bposlem4  21102  bposlem5  21103  bposlem7  21105  bposlem8  21106  bposlem9  21107  lgsdir2lem1  21138  m1lgs  21177  2sqlem11  21190  chebbnd1lem3  21196  chpchtlim  21204  dchrvmasumlem2  21223  dchrvmasumlema  21225  dchrvmasumiflem1  21226  logdivsum  21258  mulog2sumlem2  21260  log2sumbnd  21269  chpdifbndlem1  21278  pntpbnd1a  21310  pntpbnd2  21312  pntibndlem3  21317  pntlemk  21331  usgraexvlem  21445  usgraex0elv  21446  usgraex1elv  21447  usgraex2elv  21448  usgraex3elv  21449  constr3pthlem3  21675  4cycl4v4e  21684  4cycl4dv4e  21686  konigsberg  21740  ex-fl  21786  ipidsq  22240  minvecolem2  22408  normlem6  22648  normpar2i  22689  sqsscirc1  24337  rnlogblem  24430  4bc2eq6  25235  axlowdimlem3  25914  axlowdimlem6  25917  axlowdimlem7  25918  axlowdimlem16  25927  axlowdimlem17  25928  axlowdim  25931  tan2h  26276  fdc  26487  heiborlem8  26565  jm2.20nn  27106  lhe4.4ex1a  27561  itgsin0pilem1  27758  itgsinexplem1  27762  stoweidlem26  27789  wallispilem2  27829  wallispilem4  27831  wallispi  27833  wallispi2  27836  stirlinglem1  27837  stirlinglem6  27842  stirlinglem7  27843  stirlinglem15  27851  stirlingr  27853  2eluzge0  28148  2eluzge1  28149  usgra2pthlem1  28372  sineq0ALT  29147
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