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

Theorem ltleii 10198
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 10197 . 2 (𝐴 < 𝐵𝐴𝐵)
51, 4ax-mp 5 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2030   class class class wbr 4685  cr 9973   < clt 10112  cle 10113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-pre-lttri 10048
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118
This theorem is referenced by:  0le1  10589  ledivp1i  10987  ltdivp1i  10988  1le2  11279  1le3  11282  halfge0  11287  decleh  11579  declecOLD  11582  uzuzle23  11767  fz0to4untppr  12481  fzo0to42pr  12595  faclbnd4lem1  13120  4bc2eq6  13156  sqrt9  14058  sqrt2gt1lt2  14059  absrdbnd  14125  sqrtpclii  14166  geo2lim  14650  0.999...  14656  0.999...OLD  14657  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  cos2bnd  14962  rpnnen2lem3  14989  rpnnen2lem4  14990  rpnnen2lem9  14995  rpnnen2lem12  14998  flodddiv4  15184  bitsp1o  15202  strlemor1OLD  16016  strleun  16019  cnfldfun  19806  elii1  22781  htpycc  22826  pcoval1  22859  pco0  22860  pcoval2  22862  pcocn  22863  pcohtpylem  22865  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevlem  22872  vitalilem4  23425  vitali  23427  mbfi1fseqlem6  23532  dveflem  23787  sinhalfpilem  24260  sincosq1lem  24294  sincos4thpi  24310  sincos6thpi  24312  tanregt0  24330  efif1olem4  24336  relogrn  24353  argregt0  24401  argrege0  24402  logneg2  24406  heron  24610  asin1  24666  reasinsin  24668  log2cnv  24716  log2tlbnd  24717  log2ub  24721  harmonicbnd3  24779  ppiublem1  24972  ppiub  24974  bposlem3  25056  bposlem4  25057  bposlem5  25058  bposlem7  25060  bposlem8  25061  bposlem9  25062  lgsdir2lem1  25095  chebbnd1lem3  25205  dchrvmasumlema  25234  logdivsum  25267  mulog2sumlem2  25269  pntpbnd1a  25319  pntpbnd2  25321  pntlemk  25340  istrkg3ld  25405  axlowdimlem16  25882  axlowdimlem17  25883  axlowdim  25886  usgrexmplef  26196  upgr4cycl4dv4e  27163  konigsbergiedgw  27226  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  ex-fl  27434  ex-sqrt  27441  ex-gcd  27444  normlem6  28100  sqsscirc1  30082  prodfzo03  30809  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  tgoldbachgnn  30865  logi  31746  dnizeq0  32590  cnndvlem1  32653  bj-pinftyccb  33238  bj-pinftynminfty  33244  tan2h  33531  fdc  33671  jm2.20nn  37881  areaquad  38119  sineq0ALT  39487  halffl  39824  itgsin0pilem1  40483  itgsinexplem1  40487  wallispilem2  40601  wallispilem4  40603  stirlinglem15  40623  stirlingr  40625  fourierdlem62  40703  fourierdlem77  40718  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem114  40755  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  etransclem23  40792  etransclem46  40815  smfmullem4  41322  fmtnoprmfac2lem1  41803  fmtno4prmfac  41809  31prm  41837  mod42tp1mod8  41844  sbgoldbo  42000  nnsum3primes4  42001  nnsum3primesgbe  42005  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  tgblthelfgott  42028  tgblthelfgottOLD  42034
  Copyright terms: Public domain W3C validator