Theorem xrltnle 10697

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2111   class class class wbr 5030  ℝ^*cxr 10663   < clt 10664   ≤ cle 10665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-le 10670

This theorem is referenced by:  xrletri  12534  qextltlem  12583  xralrple  12586  xltadd1  12637  xsubge0  12642  xposdif  12643  xltmul1  12673  ioo0  12751  ico0  12772  ioc0  12773  snunioo  12856  snunioc  12858  difreicc  12862  hashbnd  13692  limsuplt  14828  pcadd  16215  pcadd2  16216  ramubcl  16344  ramlb  16345  leordtvallem1  21815  leordtvallem2  21816  leordtval2  21817  leordtval  21818  lecldbas  21824  blcld  23112  stdbdbl  23124  tmsxpsval2  23146  iocmnfcld  23374  xrsxmet  23414  metdsge  23454  bndth  23563  ovolgelb  24084  ovolunnul  24104  ioombl  24169  volsup2  24209  mbfmax  24253  ismbf3d  24258  itg2seq  24346  itg2monolem2  24355  itg2monolem3  24356  lhop2  24618  mdegleb  24665  deg1ge  24699  deg1add  24704  ig1pdvds  24777  plypf1  24809  radcnvlt1  25013  upgrfi  26884  xrdifh  30529  xrge00  30720  gsumesum  31428  itg2gt0cn  35112  asindmre  35140  dvasin  35141  radcnvrat  41018  supxrgelem  41969  infrpge  41983  xrlexaddrp  41984  xrltnled  41995  xrpnf  42125  gtnelioc  42128  ltnelicc  42134  gtnelicc  42137  snunioo1  42149  eliccnelico  42166  xrgtnelicc  42175  lptioo2  42273  stoweidlem34  42676  fourierdlem20  42769  fouriersw  42873  nltle2tri  43870  iccelpart  43950