Theorem xrltnle 11217

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 11215	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	con2bid 354	. 2 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
3	2	ancoms 458	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5102  ℝ^*cxr 11183   < clt 11184   ≤ cle 11185

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-le 11190

This theorem is referenced by:  xrletri  13089  qextltlem  13138  xralrple  13141  xltadd1  13192  xsubge0  13197  xposdif  13198  xltmul1  13228  ioo0  13307  ico0  13328  ioc0  13329  snunioo  13415  snunioc  13417  difreicc  13421  hashbnd  14277  limsuplt  15421  pcadd  16836  pcadd2  16837  ramubcl  16965  ramlb  16966  leordtvallem1  23073  leordtvallem2  23074  leordtval2  23075  leordtval  23076  lecldbas  23082  blcld  24369  stdbdbl  24381  tmsxpsval2  24403  iocmnfcld  24632  xrsxmet  24674  metdsge  24714  bndth  24833  ovolgelb  25357  ovolunnul  25377  ioombl  25442  volsup2  25482  mbfmax  25526  ismbf3d  25531  itg2seq  25619  itg2monolem2  25628  itg2monolem3  25629  lhop2  25896  mdegleb  25945  deg1ge  25979  deg1add  25984  ig1pdvds  26061  plypf1  26093  radcnvlt1  26303  upgrfi  28994  xrdifh  32676  xrge00  32926  gsumesum  34022  itg2gt0cn  37642  asindmre  37670  dvasin  37671  aks6d1c6lem3  42133  aks6d1c7lem2  42142  iocioodisjd  42281  radcnvrat  44276  supxrgelem  45306  infrpge  45320  xrlexaddrp  45321  xrltnled  45332  xrpnf  45454  gtnelioc  45462  ltnelicc  45468  gtnelicc  45471  snunioo1  45483  eliccnelico  45500  xrgtnelicc  45509  lptioo2  45602  stoweidlem34  46005  fourierdlem20  46098  fouriersw  46202  nltle2tri  47287  iccelpart  47407