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

Theorem ltle 10411
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 885 . 2 (𝐴 < 𝐵 → (𝐴 < 𝐵𝐴 = 𝐵))
2 leloe 10409 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))
31, 2syl5ibr 237 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wo 865   = wceq 1637  wcel 2156   class class class wbr 4844  cr 10220   < clt 10359  cle 10360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-resscn 10278  ax-pre-lttri 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365
This theorem is referenced by:  ltleletr  10415  letr  10416  letric  10422  ltlen  10423  ltlei  10444  ltled  10470  lt2add  10798  lep1  11147  lem1  11149  letrp1  11150  ltmul12a  11164  mulge0b  11178  lediv12a  11201  bndndx  11558  ltsubnn0  11610  uzind  11735  fnn0ind  11742  eluz2b2  11980  zmin  12003  rpnnen1lem2  12033  rpnnen1lem1  12034  rpnnen1lem3  12035  rpnnen1lem5  12037  rpge0  12059  rpneg  12077  iccsplit  12528  zltaddlt1le  12547  difelfznle  12677  fvffz0  12681  elfzouz2  12708  elfzo0le  12736  fzostep1  12808  fllep1  12826  fracle1  12828  expgt1  13121  expnbnd  13216  expnlbnd2  13218  faclbnd  13297  swrdsbslen  13672  swrdspsleq  13673  swrdccat3  13716  repswswrd  13755  resqrex  14214  sqrtgt0  14222  absmax  14292  eqsqrt2d  14331  rlim2lt  14451  mulcn2  14549  rlimo1  14570  o1rlimmul  14572  climbdd  14625  caucvgrlem  14626  supcvg  14810  efcllem  15028  sin01bnd  15135  cos01bnd  15136  sin01gt0  15140  cos01gt0  15141  absef  15147  efieq1re  15149  ruclem11  15189  nn0o  15319  pythagtriplem12  15748  pythagtriplem13  15749  pythagtriplem14  15750  pythagtriplem16  15752  pclem  15760  prmgaplem4  15975  cshwshashlem2  16015  isabvd  19024  met2ndci  22540  blcvx  22814  iocopnst  22952  nmoleub2a  23129  nmoleub2b  23130  nmhmcn  23132  iscmet3lem2  23302  caubl  23318  ivthlem2  23433  ovolicc2lem4  23501  ioombl1lem4  23542  ioovolcl  23551  volsup2  23586  itg2monolem1  23731  itg2gt0  23741  itg2cnlem1  23742  dvne0  23988  ftc1lem4  24016  dgrlt  24236  aalioulem5  24305  ulmbdd  24366  iblulm  24375  radcnvlem1  24381  abelthlem5  24403  abelthlem7  24406  sincosq1lem  24464  tangtx  24472  tanabsge  24473  sinq12ge0  24475  sineq0  24488  tanord  24499  logcj  24566  argregt0  24570  argrege0  24571  argimgt0  24572  logdmnrp  24601  logcnlem3  24604  logf1o2  24610  cxpsqrtlem  24662  abscxpbnd  24708  logreclem  24714  asinneg  24827  atanlogsublem  24856  atanlogsub  24857  rlimcnp  24906  xrlimcnp  24909  basellem8  25028  chtub  25151  bposlem9  25231  chebbnd1  25375  chtppilimlem1  25376  dchrvmasumiflem1  25404  mulog2sumlem2  25438  pntrmax  25467  pntibndlem2  25494  pntibndlem3  25495  pntlemf  25508  axlowdimlem16  26051  pthdlem1  26890  crctcshwlkn0lem3  26933  crctcshwlkn0lem5  26935  crctcshwlkn0lem7  26937  crctcshwlkn0  26942  nmblolbii  27982  ubthlem1  28054  bcsiALT  28364  nmbdoplbi  29211  nmcexi  29213  nmcoplbi  29215  lnconi  29220  nmbdfnlbi  29236  nmcfnlbi  29239  nmopcoi  29282  branmfn  29292  leopmul  29321  nmopleid  29326  esumcvg  30473  ballotlemfrceq  30915  sinccvglem  31888  opnrebl2  32637  ivthALT  32651  dnibndlem12  32796  poimirlem15  33737  poimirlem31  33753  ftc1cnnclem  33795  ftc1anclem5  33801  incsequz2  33856  nnubfi  33857  bfplem2  33933  pell14qrgap  37941  pellfundre  37947  pellfundlb  37950  stoweidlem17  40713  stoweidlem34  40730  wallispilem1  40761  leltletr  41884  2elfz2melfz  41903  elfzelfzlble  41906  subsubelfzo0  41911  pfxccat3  42001  bgoldbtbnd  42272  bgoldbachlt  42276  tgblthelfgott  42278  m1modmmod  42884  nnolog2flm1  42952
  Copyright terms: Public domain W3C validator