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

Theorem ltle 10164
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 10162 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))
31, 2syl5ibr 236 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383   = wceq 1523  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:  ltleletr  10168  letr  10169  letric  10175  ltlen  10176  ltlei  10197  ltled  10223  lt2add  10551  lep1  10900  lem1  10902  letrp1  10903  ltmul12a  10917  mulge0b  10931  lediv12a  10954  bndndx  11329  ltsubnn0  11382  uzind  11507  fnn0ind  11514  eluz2b2  11799  zmin  11822  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  rpge0  11883  rpneg  11901  iccsplit  12343  zltaddlt1le  12362  difelfznle  12492  fvffz0  12496  elfzouz2  12523  elfzo0le  12551  fzostep1  12624  fllep1  12642  fracle1  12644  expgt1  12938  expnbnd  13033  expnlbnd2  13035  faclbnd  13117  swrdsbslen  13494  swrdspsleq  13495  swrdccat3  13538  repswswrd  13577  resqrex  14035  sqrtgt0  14043  absmax  14113  eqsqrt2d  14152  rlim2lt  14272  mulcn2  14370  rlimo1  14391  o1rlimmul  14393  climbdd  14446  caucvgrlem  14447  supcvg  14632  efcllem  14852  sin01bnd  14959  cos01bnd  14960  sin01gt0  14964  cos01gt0  14965  absef  14971  efieq1re  14973  ruclem11  15013  nn0o  15146  pythagtriplem12  15578  pythagtriplem13  15579  pythagtriplem14  15580  pythagtriplem16  15582  pclem  15590  prmgaplem4  15805  cshwshashlem2  15850  isabvd  18868  met2ndci  22374  blcvx  22648  iocopnst  22786  nmoleub2a  22963  nmoleub2b  22964  nmhmcn  22966  iscmet3lem2  23136  caubl  23152  ivthlem2  23267  ovolicc2lem4  23334  ioombl1lem4  23375  ioovolcl  23384  volsup2  23419  itg2monolem1  23562  itg2gt0  23572  itg2cnlem1  23573  dvne0  23819  ftc1lem4  23847  dgrlt  24067  aalioulem5  24136  ulmbdd  24197  iblulm  24206  radcnvlem1  24212  abelthlem5  24234  abelthlem7  24237  sincosq1lem  24294  tangtx  24302  tanabsge  24303  sinq12ge0  24305  sineq0  24318  tanord  24329  logcj  24397  argregt0  24401  argrege0  24402  argimgt0  24403  logdmnrp  24432  logcnlem3  24435  logf1o2  24441  cxpsqrtlem  24493  abscxpbnd  24539  logreclem  24545  asinneg  24658  atanlogsublem  24687  atanlogsub  24688  rlimcnp  24737  xrlimcnp  24740  basellem8  24859  chtub  24982  bposlem9  25062  chebbnd1  25206  chtppilimlem1  25207  dchrvmasumiflem1  25235  mulog2sumlem2  25269  pntrmax  25298  pntibndlem2  25325  pntibndlem3  25326  pntlemf  25339  axlowdimlem16  25882  pthdlem1  26718  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  crctcshwlkn0lem7  26764  crctcshwlkn0  26769  nmblolbii  27782  ubthlem1  27854  bcsiALT  28164  nmbdoplbi  29011  nmcexi  29013  nmcoplbi  29015  lnconi  29020  nmbdfnlbi  29036  nmcfnlbi  29039  nmopcoi  29082  branmfn  29092  leopmul  29121  nmopleid  29126  esumcvg  30276  ballotlemfrceq  30718  sinccvglem  31692  opnrebl2  32441  ivthALT  32455  dnibndlem12  32604  poimirlem15  33554  poimirlem31  33570  ftc1cnnclem  33613  ftc1anclem5  33619  incsequz2  33675  nnubfi  33676  bfplem2  33752  pell14qrgap  37756  pellfundre  37762  pellfundlb  37765  stoweidlem17  40552  stoweidlem34  40569  wallispilem1  40600  leltletr  41633  2elfz2melfz  41653  elfzelfzlble  41656  subsubelfzo0  41661  pfxccat3  41751  bgoldbtbnd  42022  bgoldbachlt  42026  tgblthelfgott  42028  bgoldbachltOLD  42032  tgblthelfgottOLD  42034  m1modmmod  42641  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator