Theorem xrltnle 11280

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   class class class wbr 5148  ℝ^*cxr 11246   < clt 11247   ≤ cle 11248

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-le 11253

This theorem is referenced by:  xrletri  13131  qextltlem  13180  xralrple  13183  xltadd1  13234  xsubge0  13239  xposdif  13240  xltmul1  13270  ioo0  13348  ico0  13369  ioc0  13370  snunioo  13454  snunioc  13456  difreicc  13460  hashbnd  14295  limsuplt  15422  pcadd  16821  pcadd2  16822  ramubcl  16950  ramlb  16951  leordtvallem1  22713  leordtvallem2  22714  leordtval2  22715  leordtval  22716  lecldbas  22722  blcld  24013  stdbdbl  24025  tmsxpsval2  24047  iocmnfcld  24284  xrsxmet  24324  metdsge  24364  bndth  24473  ovolgelb  24996  ovolunnul  25016  ioombl  25081  volsup2  25121  mbfmax  25165  ismbf3d  25170  itg2seq  25259  itg2monolem2  25268  itg2monolem3  25269  lhop2  25531  mdegleb  25581  deg1ge  25615  deg1add  25620  ig1pdvds  25693  plypf1  25725  radcnvlt1  25929  upgrfi  28348  xrdifh  31986  xrge00  32182  gsumesum  33052  itg2gt0cn  36538  asindmre  36566  dvasin  36567  radcnvrat  43063  supxrgelem  44037  infrpge  44051  xrlexaddrp  44052  xrltnled  44063  xrpnf  44186  gtnelioc  44194  ltnelicc  44200  gtnelicc  44203  snunioo1  44215  eliccnelico  44232  xrgtnelicc  44241  lptioo2  44337  stoweidlem34  44740  fourierdlem20  44833  fouriersw  44937  nltle2tri  46011  iccelpart  46091