Theorem xrltnle 10900

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2110   class class class wbr 5053  ℝ^*cxr 10866   < clt 10867   ≤ cle 10868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-xp 5557  df-cnv 5559  df-le 10873

This theorem is referenced by:  xrletri  12743  qextltlem  12792  xralrple  12795  xltadd1  12846  xsubge0  12851  xposdif  12852  xltmul1  12882  ioo0  12960  ico0  12981  ioc0  12982  snunioo  13066  snunioc  13068  difreicc  13072  hashbnd  13902  limsuplt  15040  pcadd  16442  pcadd2  16443  ramubcl  16571  ramlb  16572  leordtvallem1  22107  leordtvallem2  22108  leordtval2  22109  leordtval  22110  lecldbas  22116  blcld  23403  stdbdbl  23415  tmsxpsval2  23437  iocmnfcld  23666  xrsxmet  23706  metdsge  23746  bndth  23855  ovolgelb  24377  ovolunnul  24397  ioombl  24462  volsup2  24502  mbfmax  24546  ismbf3d  24551  itg2seq  24640  itg2monolem2  24649  itg2monolem3  24650  lhop2  24912  mdegleb  24962  deg1ge  24996  deg1add  25001  ig1pdvds  25074  plypf1  25106  radcnvlt1  25310  upgrfi  27182  xrdifh  30821  xrge00  31014  gsumesum  31739  itg2gt0cn  35569  asindmre  35597  dvasin  35598  radcnvrat  41605  supxrgelem  42549  infrpge  42563  xrlexaddrp  42564  xrltnled  42575  xrpnf  42701  gtnelioc  42704  ltnelicc  42710  gtnelicc  42713  snunioo1  42725  eliccnelico  42742  xrgtnelicc  42751  lptioo2  42847  stoweidlem34  43250  fourierdlem20  43343  fouriersw  43447  nltle2tri  44478  iccelpart  44558