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

Theorem ltle 9978
Description: 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
Assertion
Ref Expression
ltle ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))

Proof of Theorem ltle
StepHypRef Expression
1 orc 399 . 2 (𝐴 < 𝐵 → (𝐴 < 𝐵𝐴 = 𝐵))
2 leloe 9976 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))
31, 2syl5ibr 235 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383   = wceq 1475  wcel 1977   class class class wbr 4578  cr 9792   < clt 9931  cle 9932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-pre-lttri 9867
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937
This theorem is referenced by:  ltleletr  9982  letr  9983  letric  9989  ltlen  9990  ltlei  10011  ltled  10037  lt2add  10365  lep1  10714  lem1  10716  letrp1  10717  ltmul12a  10731  mulge0b  10745  lediv12a  10768  bndndx  11141  ltsubnn0  11194  uzind  11304  fnn0ind  11311  eluz2b2  11596  zmin  11619  rpnnen1lem2  11649  rpnnen1lem1  11650  rpnnen1lem3  11651  rpnnen1lem5  11653  rpnnen1lem1OLD  11656  rpnnen1lem3OLD  11657  rpnnen1lem5OLD  11659  rpge0  11680  rpneg  11698  iccsplit  12135  zltaddlt1le  12154  difelfznle  12280  fvffz0  12284  elfzouz2  12311  elfzo0le  12337  fzosplitprm1  12401  fzostep1  12404  fllep1  12422  fracle1  12424  expgt1  12718  expnbnd  12813  expnlbnd2  12815  faclbnd  12897  swrdsbslen  13249  swrdspsleq  13250  swrdccat3  13292  repswswrd  13331  resqrex  13788  sqrtgt0  13796  absmax  13866  eqsqrt2d  13905  rlim2lt  14025  mulcn2  14123  rlimo1  14144  o1rlimmul  14146  climbdd  14199  caucvgrlem  14200  supcvg  14376  efcllem  14596  sin01bnd  14703  cos01bnd  14704  sin01gt0  14708  cos01gt0  14709  absef  14715  efieq1re  14717  ruclem11  14757  nn0o  14886  pythagtriplem12  15318  pythagtriplem13  15319  pythagtriplem14  15320  pythagtriplem16  15322  pclem  15330  prmgaplem4  15545  cshwshashlem2  15590  isabvd  18592  met2ndci  22085  blcvx  22357  iocopnst  22495  nmoleub2a  22673  nmoleub2b  22674  nmhmcn  22676  iscmet3lem2  22843  caubl  22859  ivthlem2  22973  ovolicc2lem4  23040  ioombl1lem4  23081  ioovolcl  23089  volsup2  23124  itg2monolem1  23268  itg2gt0  23278  itg2cnlem1  23279  dvne0  23523  ftc1lem4  23551  dgrlt  23771  aalioulem5  23840  ulmbdd  23901  iblulm  23910  radcnvlem1  23916  abelthlem5  23938  abelthlem7  23941  sincosq1lem  23998  tangtx  24006  tanabsge  24007  sinq12ge0  24009  sineq0  24022  tanord  24033  logcj  24101  argregt0  24105  argrege0  24106  argimgt0  24107  logdmnrp  24132  logcnlem3  24135  logf1o2  24141  cxpsqrtlem  24193  abscxpbnd  24239  logreclem  24245  asinneg  24358  atanlogsublem  24387  atanlogsub  24388  rlimcnp  24437  xrlimcnp  24440  basellem8  24559  chtub  24682  bposlem9  24762  chebbnd1  24906  chtppilimlem1  24907  dchrvmasumiflem1  24935  mulog2sumlem2  24969  pntrmax  24998  pntibndlem2  25025  pntibndlem3  25026  pntlemf  25039  axlowdimlem16  25583  nmblolbii  26832  ubthlem1  26904  bcsiALT  27214  nmbdoplbi  28061  nmcexi  28063  nmcoplbi  28065  lnconi  28070  nmbdfnlbi  28086  nmcfnlbi  28089  nmopcoi  28132  branmfn  28142  leopmul  28171  nmopleid  28176  esumcvg  29269  ballotlemfrceq  29711  sinccvglem  30614  opnrebl2  31280  ivthALT  31294  dnibndlem12  31443  poimirlem15  32388  poimirlem31  32404  ftc1cnnclem  32447  ftc1anclem5  32453  incsequz2  32509  nnubfi  32510  bfplem2  32586  pell14qrgap  36251  pellfundre  36257  pellfundlb  36260  stoweidlem17  38704  stoweidlem34  38721  wallispilem1  38752  leltletr  39735  bgoldbtbnd  40020  bgoldbachlt  40022  tgblthelfgott  40024  bgoldbachltOLD  40029  tgblthelfgottOLD  40031  pfxccat3  40084  2elfz2melfz  40172  elfzelfzlble  40175  subsubelfzo0  40176  pthdlem1  40964  crctcsh1wlkn0lem3  41007  crctcsh1wlkn0lem5  41009  crctcsh1wlkn0lem7  41011  crctcsh1wlkn0  41016  m1modmmod  42102  nnolog2flm1  42174
  Copyright terms: Public domain W3C validator