Theorem xrltnle 11302

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

Step	Hyp	Ref	Expression
1		xrlenlt 11300	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	con2bid 354	. 2 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
3	2	ancoms 458	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119  ℝ^*cxr 11268   < clt 11269   ≤ cle 11270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-le 11275

This theorem is referenced by:  xrletri  13169  qextltlem  13218  xralrple  13221  xltadd1  13272  xsubge0  13277  xposdif  13278  xltmul1  13308  ioo0  13387  ico0  13408  ioc0  13409  snunioo  13495  snunioc  13497  difreicc  13501  hashbnd  14354  limsuplt  15495  pcadd  16909  pcadd2  16910  ramubcl  17038  ramlb  17039  leordtvallem1  23148  leordtvallem2  23149  leordtval2  23150  leordtval  23151  lecldbas  23157  blcld  24444  stdbdbl  24456  tmsxpsval2  24478  iocmnfcld  24707  xrsxmet  24749  metdsge  24789  bndth  24908  ovolgelb  25433  ovolunnul  25453  ioombl  25518  volsup2  25558  mbfmax  25602  ismbf3d  25607  itg2seq  25695  itg2monolem2  25704  itg2monolem3  25705  lhop2  25972  mdegleb  26021  deg1ge  26055  deg1add  26060  ig1pdvds  26137  plypf1  26169  radcnvlt1  26379  upgrfi  29070  xrdifh  32757  xrge00  33007  gsumesum  34090  itg2gt0cn  37699  asindmre  37727  dvasin  37728  aks6d1c6lem3  42185  aks6d1c7lem2  42194  iocioodisjd  42369  radcnvrat  44338  supxrgelem  45364  infrpge  45378  xrlexaddrp  45379  xrltnled  45390  xrpnf  45512  gtnelioc  45520  ltnelicc  45526  gtnelicc  45529  snunioo1  45541  eliccnelico  45558  xrgtnelicc  45567  lptioo2  45660  stoweidlem34  46063  fourierdlem20  46156  fouriersw  46260  nltle2tri  47342  iccelpart  47447