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

Theorem ltle 10239
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 10237 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))
31, 2syl5ibr 236 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383   = wceq 1596  wcel 2103   class class class wbr 4760  cr 10048   < clt 10187  cle 10188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-resscn 10106  ax-pre-lttri 10123
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193
This theorem is referenced by:  ltleletr  10243  letr  10244  letric  10250  ltlen  10251  ltlei  10272  ltled  10298  lt2add  10626  lep1  10975  lem1  10977  letrp1  10978  ltmul12a  10992  mulge0b  11006  lediv12a  11029  bndndx  11404  ltsubnn0  11457  uzind  11582  fnn0ind  11589  eluz2b2  11875  zmin  11898  rpnnen1lem2  11928  rpnnen1lem1  11929  rpnnen1lem3  11930  rpnnen1lem5  11932  rpnnen1lem1OLD  11935  rpnnen1lem3OLD  11936  rpnnen1lem5OLD  11938  rpge0  11959  rpneg  11977  iccsplit  12419  zltaddlt1le  12438  difelfznle  12568  fvffz0  12572  elfzouz2  12599  elfzo0le  12627  fzostep1  12699  fllep1  12717  fracle1  12719  expgt1  13013  expnbnd  13108  expnlbnd2  13110  faclbnd  13192  swrdsbslen  13569  swrdspsleq  13570  swrdccat3  13613  repswswrd  13652  resqrex  14111  sqrtgt0  14119  absmax  14189  eqsqrt2d  14228  rlim2lt  14348  mulcn2  14446  rlimo1  14467  o1rlimmul  14469  climbdd  14522  caucvgrlem  14523  supcvg  14708  efcllem  14928  sin01bnd  15035  cos01bnd  15036  sin01gt0  15040  cos01gt0  15041  absef  15047  efieq1re  15049  ruclem11  15089  nn0o  15222  pythagtriplem12  15654  pythagtriplem13  15655  pythagtriplem14  15656  pythagtriplem16  15658  pclem  15666  prmgaplem4  15881  cshwshashlem2  15926  isabvd  18943  met2ndci  22449  blcvx  22723  iocopnst  22861  nmoleub2a  23038  nmoleub2b  23039  nmhmcn  23041  iscmet3lem2  23211  caubl  23227  ivthlem2  23342  ovolicc2lem4  23409  ioombl1lem4  23450  ioovolcl  23459  volsup2  23494  itg2monolem1  23637  itg2gt0  23647  itg2cnlem1  23648  dvne0  23894  ftc1lem4  23922  dgrlt  24142  aalioulem5  24211  ulmbdd  24272  iblulm  24281  radcnvlem1  24287  abelthlem5  24309  abelthlem7  24312  sincosq1lem  24369  tangtx  24377  tanabsge  24378  sinq12ge0  24380  sineq0  24393  tanord  24404  logcj  24472  argregt0  24476  argrege0  24477  argimgt0  24478  logdmnrp  24507  logcnlem3  24510  logf1o2  24516  cxpsqrtlem  24568  abscxpbnd  24614  logreclem  24620  asinneg  24733  atanlogsublem  24762  atanlogsub  24763  rlimcnp  24812  xrlimcnp  24815  basellem8  24934  chtub  25057  bposlem9  25137  chebbnd1  25281  chtppilimlem1  25282  dchrvmasumiflem1  25310  mulog2sumlem2  25344  pntrmax  25373  pntibndlem2  25400  pntibndlem3  25401  pntlemf  25414  axlowdimlem16  25957  pthdlem1  26793  crctcshwlkn0lem3  26836  crctcshwlkn0lem5  26838  crctcshwlkn0lem7  26840  crctcshwlkn0  26845  nmblolbii  27884  ubthlem1  27956  bcsiALT  28266  nmbdoplbi  29113  nmcexi  29115  nmcoplbi  29117  lnconi  29122  nmbdfnlbi  29138  nmcfnlbi  29141  nmopcoi  29184  branmfn  29194  leopmul  29223  nmopleid  29228  esumcvg  30378  ballotlemfrceq  30820  sinccvglem  31794  opnrebl2  32543  ivthALT  32557  dnibndlem12  32706  poimirlem15  33656  poimirlem31  33672  ftc1cnnclem  33715  ftc1anclem5  33721  incsequz2  33777  nnubfi  33778  bfplem2  33854  pell14qrgap  37858  pellfundre  37864  pellfundlb  37867  stoweidlem17  40654  stoweidlem34  40671  wallispilem1  40702  leltletr  41735  2elfz2melfz  41755  elfzelfzlble  41758  subsubelfzo0  41763  pfxccat3  41853  bgoldbtbnd  42124  bgoldbachlt  42128  tgblthelfgott  42130  bgoldbachltOLD  42134  tgblthelfgottOLD  42136  m1modmmod  42743  nnolog2flm1  42811
  Copyright terms: Public domain W3C validator