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

Theorem xrltnle 11227
Description: "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.)
Assertion
Ref Expression
xrltnle ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))

Proof of Theorem xrltnle
StepHypRef Expression
1 xrlenlt 11225 . . 3 ((𝐵 ∈ ℝ*𝐴 ∈ ℝ*) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
21con2bid 355 . 2 ((𝐵 ∈ ℝ*𝐴 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
32ancoms 460 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wcel 2107   class class class wbr 5106  *cxr 11193   < clt 11194  cle 11195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-cnv 5642  df-le 11200
This theorem is referenced by:  xrletri  13078  qextltlem  13127  xralrple  13130  xltadd1  13181  xsubge0  13186  xposdif  13187  xltmul1  13217  ioo0  13295  ico0  13316  ioc0  13317  snunioo  13401  snunioc  13403  difreicc  13407  hashbnd  14242  limsuplt  15367  pcadd  16766  pcadd2  16767  ramubcl  16895  ramlb  16896  leordtvallem1  22577  leordtvallem2  22578  leordtval2  22579  leordtval  22580  lecldbas  22586  blcld  23877  stdbdbl  23889  tmsxpsval2  23911  iocmnfcld  24148  xrsxmet  24188  metdsge  24228  bndth  24337  ovolgelb  24860  ovolunnul  24880  ioombl  24945  volsup2  24985  mbfmax  25029  ismbf3d  25034  itg2seq  25123  itg2monolem2  25132  itg2monolem3  25133  lhop2  25395  mdegleb  25445  deg1ge  25479  deg1add  25484  ig1pdvds  25557  plypf1  25589  radcnvlt1  25793  upgrfi  28084  xrdifh  31730  xrge00  31926  gsumesum  32715  itg2gt0cn  36179  asindmre  36207  dvasin  36208  radcnvrat  42682  supxrgelem  43658  infrpge  43672  xrlexaddrp  43673  xrltnled  43684  xrpnf  43807  gtnelioc  43815  ltnelicc  43821  gtnelicc  43824  snunioo1  43836  eliccnelico  43853  xrgtnelicc  43862  lptioo2  43958  stoweidlem34  44361  fourierdlem20  44454  fouriersw  44558  nltle2tri  45631  iccelpart  45711
  Copyright terms: Public domain W3C validator