Theorem xrltnle 11277

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143   class class class wbr 5110  ℝ^*cxr 11243   < clt 11244   ≤ cle 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-le 11250

This theorem is referenced by:  xrltnled  11278  xrletri  13179  qextltlem  13229  xralrple  13232  xltadd1  13283  xsubge0  13288  xposdif  13289  xltmul1  13319  ioo0  13398  ico0  13419  ioc0  13420  snunioo  13506  snunioc  13508  difreicc  13512  hashbnd  14374  limsuplt  15532  pcadd  16950  pcadd2  16951  ramubcl  17079  ramlb  17080  leordtvallem1  23348  leordtvallem2  23349  leordtval2  23350  leordtval  23351  lecldbas  23357  blcld  24643  stdbdbl  24655  tmsxpsval2  24677  iocmnfcld  24906  xrsxmet  24948  metdsge  24988  bndth  25098  ovolgelb  25620  ovolunnul  25640  ioombl  25705  volsup2  25745  mbfmax  25789  ismbf3d  25794  itg2seq  25882  itg2monolem2  25891  itg2monolem3  25892  lhop2  26155  mdegleb  26202  deg1ge  26236  deg1add  26241  ig1pdvds  26318  plypf1  26350  radcnvlt1  26562  upgrfi  29422  xrdifh  33106  xrge00  33315  gsumesum  34430  itg2gt0cn  38307  asindmre  38335  dvasin  38336  aks6d1c6lem3  42920  aks6d1c7lem2  42929  iocioodisjd  43062  radcnvrat  45007  supxrgelem  46036  infrpge  46050  xrlexaddrp  46051  xrpnf  46182  gtnelioc  46190  ltnelicc  46196  gtnelicc  46199  snunioo1  46211  eliccnelico  46228  xrgtnelicc  46237  lptioo2  46330  stoweidlem34  46731  fourierdlem20  46824  fouriersw  46928  nltle2tri  48033  iccelpart  48165