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

Theorem xrltle 12187
Description: 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
Assertion
Ref Expression
xrltle ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵𝐴𝐵))

Proof of Theorem xrltle
StepHypRef Expression
1 orc 856 . 2 (𝐴 < 𝐵 → (𝐴 < 𝐵𝐴 = 𝐵))
2 xrleloe 12182 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))
31, 2syl5ibr 236 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wo 836   = wceq 1631  wcel 2145   class class class wbr 4786  *cxr 10275   < clt 10276  cle 10277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-pre-lttri 10212  ax-pre-lttrn 10213
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282
This theorem is referenced by:  xrletri  12189  xrletr  12194  qextltlem  12238  xmulge0  12319  supxrunb1  12354  ico0  12426  ioc0  12427  ioossicc  12464  icossicc  12466  iocssicc  12467  ioossico  12468  snunioo  12505  snunico  12506  snunioc  12507  ioopnfsup  12871  icopnfsup  12872  hashnnn0genn0  13335  pcadd2  15801  leordtval2  21237  lecldbas  21244  xblss2ps  22426  xblss2  22427  blhalf  22430  blssps  22449  blss  22450  blcls  22531  stdbdxmet  22540  stdbdmopn  22543  metcnpi3  22571  blcvx  22821  tgqioo  22823  xrsmopn  22835  metdcnlem  22859  metnrmlem1a  22881  bndth  22977  ovolgelb  23468  icombl  23552  ioorcl2  23560  ioorf  23561  ioorinv2  23563  volivth  23595  itg2seq  23729  itg2monolem2  23738  itg2cnlem2  23749  dvferm1lem  23967  dvferm2lem  23969  dvferm  23971  dvivthlem1  23991  lhop2  23998  radcnvle  24394  tanord1  24504  dvloglem  24615  iocinif  29883  difioo  29884  esumpinfsum  30479  omssubadd  30702  elicc3  32648  tan2h  33734  heicant  33777  itg2addnclem  33793  ftc1anclem7  33823  ioounsn  38321  radcnvrat  39039  xrltled  40004  ioossioc  40234  ioossioobi  40262  fouriersw  40965  iccpartleu  41892  iccpartgel  41893  iccpartnel  41902
  Copyright terms: Public domain W3C validator