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

Theorem ltleii 11285
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 11284 . 2 (𝐴 < 𝐵𝐴𝐵)
51, 4ax-mp 5 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2107   class class class wbr 5110  cr 11057   < clt 11196  cle 11197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11115  ax-pre-lttri 11132
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202
This theorem is referenced by:  0le1  11685  ledivp1i  12087  ltdivp1i  12088  1le2  12369  1le3  12372  halfge0  12377  decleh  12660  eluz4eluz2  12817  uzuzle23  12821  fz0to4untppr  13551  fzo0to42pr  13666  faclbnd4lem1  14200  4bc2eq6  14236  sqrt9  15165  sqrt2gt1lt2  15166  absrdbnd  15233  sqrtpclii  15274  0.999...  15773  ef01bndlem  16073  sin01bnd  16074  cos01bnd  16075  cos2bnd  16077  rpnnen2lem3  16105  rpnnen2lem4  16106  rpnnen2lem9  16111  rpnnen2lem12  16114  flodddiv4  16302  strleun  17036  cnfldfunALTOLD  20826  elii1  24314  htpycc  24359  pcoval1  24392  pcocn  24396  pcohtpylem  24398  pcopt  24401  pcopt2  24402  pcoass  24403  pcorevlem  24405  vitalilem4  24991  vitali  24993  dveflem  25359  sinhalfpilem  25836  sincosq1lem  25870  sincos4thpi  25886  sincos6thpi  25888  pige3  25891  cos0pilt1  25904  tanregt0  25911  efif1olem4  25917  relogrn  25933  argregt0  25981  argrege0  25982  logneg2  25986  2logb9irr  26161  asin1  26260  reasinsin  26262  log2cnv  26310  log2tlbnd  26311  log2ub  26315  harmonicbnd3  26373  ppiublem1  26566  ppiub  26568  bposlem3  26650  bposlem4  26651  bposlem5  26652  bposlem7  26654  bposlem8  26655  bposlem9  26656  lgsdir2lem1  26689  chebbnd1lem3  26835  dchrvmasumlema  26864  logdivsum  26897  mulog2sumlem2  26899  pntpbnd1a  26949  pntpbnd2  26951  pntlemk  26970  istrkg3ld  27445  axlowdimlem16  27948  axlowdimlem17  27949  axlowdim  27952  usgrexmplef  28249  upgr4cycl4dv4e  29171  konigsbergiedgw  29234  konigsberglem1  29238  konigsberglem2  29239  konigsberglem3  29240  ex-fl  29433  ex-sqrt  29440  ex-gcd  29443  normlem6  30099  sqsscirc1  32529  prodfzo03  33256  hgt750lemd  33301  hgt750lem  33304  hgt750lem2  33305  hgt750leme  33311  tgoldbachgnn  33312  logi  34346  dnizeq0  34967  cnndvlem1  35029  bj-pinftyccb  35721  bj-pinftynminfty  35727  tan2h  36099  fdc  36233  jm2.20nn  41350  areaquad  41579  sineq0ALT  43293  halffl  43604  itgsin0pilem1  44265  itgsinexplem1  44269  wallispilem2  44381  wallispilem4  44383  stirlinglem15  44403  stirlingr  44405  fourierdlem62  44483  fourierdlem77  44498  fourierdlem102  44523  fourierdlem103  44524  fourierdlem104  44525  fourierdlem111  44532  fourierdlem112  44533  fourierdlem114  44535  sqwvfoura  44543  sqwvfourb  44544  fourierswlem  44545  fouriersw  44546  etransclem23  44572  etransclem46  44595  smfmullem4  45109  fmtnoprmfac2lem1  45832  fmtno4prmfac  45838  31prm  45863  mod42tp1mod8  45868  2exp340mod341  45999  341fppr2  46000  9fppr8  46003  nfermltl8rev  46008  nfermltl2rev  46009  sbgoldbo  46053  nnsum3primes4  46054  nnsum3primesgbe  46058  nnsum4primeseven  46066  nnsum4primesevenALTV  46067  wtgoldbnnsum4prm  46068  bgoldbnnsum3prm  46070  tgblthelfgott  46081  ackval42  46856  itsclc0yqsollem2  46923  sepfsepc  47034
  Copyright terms: Public domain W3C validator