Theorem xrltnle 10973

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝ^*cxr 10939   < clt 10940   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-le 10946

This theorem is referenced by:  xrletri  12816  qextltlem  12865  xralrple  12868  xltadd1  12919  xsubge0  12924  xposdif  12925  xltmul1  12955  ioo0  13033  ico0  13054  ioc0  13055  snunioo  13139  snunioc  13141  difreicc  13145  hashbnd  13978  limsuplt  15116  pcadd  16518  pcadd2  16519  ramubcl  16647  ramlb  16648  leordtvallem1  22269  leordtvallem2  22270  leordtval2  22271  leordtval  22272  lecldbas  22278  blcld  23567  stdbdbl  23579  tmsxpsval2  23601  iocmnfcld  23838  xrsxmet  23878  metdsge  23918  bndth  24027  ovolgelb  24549  ovolunnul  24569  ioombl  24634  volsup2  24674  mbfmax  24718  ismbf3d  24723  itg2seq  24812  itg2monolem2  24821  itg2monolem3  24822  lhop2  25084  mdegleb  25134  deg1ge  25168  deg1add  25173  ig1pdvds  25246  plypf1  25278  radcnvlt1  25482  upgrfi  27364  xrdifh  31003  xrge00  31197  gsumesum  31927  itg2gt0cn  35759  asindmre  35787  dvasin  35788  radcnvrat  41821  supxrgelem  42766  infrpge  42780  xrlexaddrp  42781  xrltnled  42792  xrpnf  42916  gtnelioc  42919  ltnelicc  42925  gtnelicc  42928  snunioo1  42940  eliccnelico  42957  xrgtnelicc  42966  lptioo2  43062  stoweidlem34  43465  fourierdlem20  43558  fouriersw  43662  nltle2tri  44693  iccelpart  44773