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

Theorem ltleii 10748
Description: 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)
Hypotheses
Ref Expression
lt.1 𝐴 ∈ ℝ
lt.2 𝐵 ∈ ℝ
ltlei.1 𝐴 < 𝐵
Assertion
Ref Expression
ltleii 𝐴𝐵

Proof of Theorem ltleii
StepHypRef Expression
1 ltlei.1 . 2 𝐴 < 𝐵
2 lt.1 . . 3 𝐴 ∈ ℝ
3 lt.2 . . 3 𝐵 ∈ ℝ
42, 3ltlei 10747 . 2 (𝐴 < 𝐵𝐴𝐵)
51, 4ax-mp 5 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2115   class class class wbr 5047  cr 10521   < clt 10660  cle 10661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-resscn 10579  ax-pre-lttri 10596
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10662  df-mnf 10663  df-xr 10664  df-ltxr 10665  df-le 10666
This theorem is referenced by:  0le1  11148  ledivp1i  11550  ltdivp1i  11551  1le2  11832  1le3  11835  halfge0  11840  decleh  12119  eluz4eluz2  12271  uzuzle23  12275  fz0to4untppr  13003  fzo0to42pr  13117  faclbnd4lem1  13647  4bc2eq6  13683  sqrt9  14622  sqrt2gt1lt2  14623  absrdbnd  14690  sqrtpclii  14731  0.999...  15226  ef01bndlem  15526  sin01bnd  15527  cos01bnd  15528  cos2bnd  15530  rpnnen2lem3  15558  rpnnen2lem4  15559  rpnnen2lem9  15564  rpnnen2lem12  15567  flodddiv4  15751  strleun  16580  cnfldfun  20543  elii1  23529  htpycc  23574  pcoval1  23607  pcocn  23611  pcohtpylem  23613  pcopt  23616  pcopt2  23617  pcoass  23618  pcorevlem  23620  vitalilem4  24204  vitali  24206  dveflem  24571  sinhalfpilem  25045  sincosq1lem  25079  sincos4thpi  25095  sincos6thpi  25097  pige3  25100  cos0pilt1  25113  tanregt0  25120  efif1olem4  25126  relogrn  25142  argregt0  25190  argrege0  25191  logneg2  25195  2logb9irr  25370  asin1  25469  reasinsin  25471  log2cnv  25519  log2tlbnd  25520  log2ub  25524  harmonicbnd3  25582  ppiublem1  25775  ppiub  25777  bposlem3  25859  bposlem4  25860  bposlem5  25861  bposlem7  25863  bposlem8  25864  bposlem9  25865  lgsdir2lem1  25898  chebbnd1lem3  26044  dchrvmasumlema  26073  logdivsum  26106  mulog2sumlem2  26108  pntpbnd1a  26158  pntpbnd2  26160  pntlemk  26179  istrkg3ld  26244  axlowdimlem16  26740  axlowdimlem17  26741  axlowdim  26744  usgrexmplef  27038  upgr4cycl4dv4e  27959  konigsbergiedgw  28022  konigsberglem1  28026  konigsberglem2  28027  konigsberglem3  28028  ex-fl  28221  ex-sqrt  28228  ex-gcd  28231  normlem6  28887  sqsscirc1  31169  prodfzo03  31892  hgt750lemd  31937  hgt750lem  31940  hgt750lem2  31941  hgt750leme  31947  tgoldbachgnn  31948  logi  32984  dnizeq0  33832  cnndvlem1  33894  bj-pinftyccb  34539  bj-pinftynminfty  34545  tan2h  34949  fdc  35083  jm2.20nn  39770  areaquad  39998  sineq0ALT  41479  halffl  41770  itgsin0pilem1  42434  itgsinexplem1  42438  wallispilem2  42550  wallispilem4  42552  stirlinglem15  42572  stirlingr  42574  fourierdlem62  42652  fourierdlem77  42667  fourierdlem102  42692  fourierdlem103  42693  fourierdlem104  42694  fourierdlem111  42701  fourierdlem112  42702  fourierdlem114  42704  sqwvfoura  42712  sqwvfourb  42713  fourierswlem  42714  fouriersw  42715  etransclem23  42741  etransclem46  42764  smfmullem4  43268  fmtnoprmfac2lem1  43925  fmtno4prmfac  43931  31prm  43956  mod42tp1mod8  43962  2exp340mod341  44093  341fppr2  44094  9fppr8  44097  nfermltl8rev  44102  nfermltl2rev  44103  sbgoldbo  44147  nnsum3primes4  44148  nnsum3primesgbe  44152  nnsum4primeseven  44160  nnsum4primesevenALTV  44161  wtgoldbnnsum4prm  44162  bgoldbnnsum3prm  44164  tgblthelfgott  44175  ackval42  44940  itsclc0yqsollem2  45007
  Copyright terms: Public domain W3C validator