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

Theorem ltle 10718
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 864 . 2 (𝐴 < 𝐵 → (𝐴 < 𝐵𝐴 = 𝐵))
2 leloe 10716 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))
31, 2syl5ibr 249 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wo 844   = wceq 1538  wcel 2114   class class class wbr 5042  cr 10525   < clt 10664  cle 10665
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-resscn 10583  ax-pre-lttri 10600
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 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670
This theorem is referenced by:  ltleletr  10722  letr  10723  letric  10729  ltlen  10730  ltlei  10751  ltled  10777  lt2add  11114  lep1  11470  lem1  11472  letrp1  11473  ltmul12a  11485  mulge0b  11499  lediv12a  11522  bndndx  11884  ltsubnn0  11936  uzind  12062  fnn0ind  12069  eluz2b2  12309  zmin  12332  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  rpge0  12390  rpneg  12409  iccsplit  12863  zltaddlt1le  12883  difelfznle  13016  fvffz0  13020  elfzouz2  13047  elfzo0le  13076  fzostep1  13148  fllep1  13166  fracle1  13168  expgt1  13463  expnbnd  13589  expnlbnd2  13591  faclbnd  13646  swrdnd0  14010  swrdsbslen  14017  swrdspsleq  14018  pfxccat3  14087  swrdccat  14088  repswswrd  14137  resqrex  14601  sqrtgt0  14609  absmax  14680  eqsqrt2d  14719  rlim2lt  14845  mulcn2  14943  rlimo1  14964  o1rlimmul  14966  climbdd  15019  caucvgrlem  15020  supcvg  15202  efcllem  15422  sin01bnd  15529  cos01bnd  15530  sin01gt0  15534  cos01gt0  15535  absef  15541  efieq1re  15543  ruclem11  15584  nn0o  15723  pythagtriplem12  16152  pythagtriplem13  16153  pythagtriplem14  16154  pythagtriplem16  16156  pclem  16164  prmgaplem4  16379  cshwshashlem2  16421  isabvd  19582  met2ndci  23127  blcvx  23401  iocopnst  23543  nmoleub2a  23720  nmoleub2b  23721  nmhmcn  23723  iscmet3lem2  23894  caubl  23910  ivthlem2  24054  ovolicc2lem4  24122  ioombl1lem4  24163  ioovolcl  24172  volsup2  24207  itg2monolem1  24352  itg2gt0  24362  itg2cnlem1  24363  dvne0  24612  ftc1lem4  24640  dgrlt  24861  aalioulem5  24930  ulmbdd  24991  iblulm  25000  radcnvlem1  25006  abelthlem5  25028  abelthlem7  25031  sincosq1lem  25088  tangtx  25096  tanabsge  25097  sinq12ge0  25099  sineq0  25114  tanord  25128  logcj  25195  argregt0  25199  argrege0  25200  argimgt0  25201  logdmnrp  25230  logcnlem3  25233  logf1o2  25239  cxpsqrtlem  25291  abscxpbnd  25340  logreclem  25346  asinneg  25470  atanlogsublem  25499  atanlogsub  25500  rlimcnp  25549  xrlimcnp  25552  basellem8  25671  chtub  25794  bposlem9  25874  chebbnd1  26054  chtppilimlem1  26055  dchrvmasumiflem1  26083  mulog2sumlem2  26117  pntrmax  26146  pntibndlem2  26173  pntibndlem3  26174  pntlemf  26187  axlowdimlem16  26749  pthdlem1  27553  crctcshwlkn0lem3  27596  crctcshwlkn0lem5  27598  crctcshwlkn0lem7  27600  crctcshwlkn0  27605  nmblolbii  28580  ubthlem1  28651  bcsiALT  28960  nmbdoplbi  29805  nmcexi  29807  nmcoplbi  29809  lnconi  29814  nmbdfnlbi  29830  nmcfnlbi  29833  nmopcoi  29876  branmfn  29886  leopmul  29915  nmopleid  29920  esumcvg  31419  ballotlemfrceq  31860  sinccvglem  32989  opnrebl2  33743  ivthALT  33757  dnibndlem12  33902  poimirlem15  35030  poimirlem31  35046  ftc1cnnclem  35086  ftc1anclem5  35092  incsequz2  35145  nnubfi  35146  bfplem2  35219  60gcd7e1  39254  lcmineqlem10  39287  factwoffsmonot  39338  3cubeslem1  39555  pell14qrgap  39746  pellfundre  39752  pellfundlb  39755  reabsifneg  40262  reabsifnpos  40263  reabsifpos  40264  reabsifnneg  40265  stoweidlem17  42598  stoweidlem34  42615  wallispilem1  42646  leltletr  43789  sqrtnegnre  43803  2elfz2melfz  43814  elfzelfzlble  43817  subsubelfzo0  43822  requad01  44078  requad2  44080  bgoldbtbnd  44266  bgoldbachlt  44270  tgblthelfgott  44272  m1modmmod  44874  nnolog2flm1  44943  itsclc0yqsol  45117
  Copyright terms: Public domain W3C validator