Theorem xrltnle 9984

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977   class class class wbr 4583  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-le 9959

This theorem is referenced by:  xrletri  11860  qextltlem  11907  xralrple  11910  xltadd1  11958  xsubge0  11963  xposdif  11964  xltmul1  11994  ioo0  12071  ico0  12092  ioc0  12093  xrge0neqmnf  12147  snunioo  12169  snunioc  12171  difreicc  12175  hashbnd  12985  limsuplt  14058  pcadd  15431  pcadd2  15432  ramubcl  15560  ramlb  15561  leordtvallem1  20824  leordtvallem2  20825  leordtval2  20826  leordtval  20827  lecldbas  20833  blcld  22120  stdbdbl  22132  tmsxpsval2  22154  iocmnfcld  22382  xrsxmet  22420  metdsge  22460  bndth  22565  ovolgelb  23055  ovolunnul  23075  ioombl  23140  volsup2  23179  mbfmax  23222  ismbf3d  23227  itg2seq  23315  itg2monolem2  23324  itg2monolem3  23325  lhop2  23582  mdegleb  23628  deg1ge  23662  deg1add  23667  ig1pdvds  23740  plypf1  23772  radcnvlt1  23976  upgrfi  25758  umgrafi  25851  xrdifh  28932  xrge00  29017  gsumesum  29448  itg2gt0cn  32635  asindmre  32665  dvasin  32666  radcnvrat  37535  supxrgelem  38494  infrpge  38508  xrlexaddrp  38509  xrltnled  38520  gtnelioc  38559  ltnelicc  38566  gtnelicc  38569  snunioo1  38585  eliccnelico  38603  xrgtnelicc  38612  lptioo2  38698  stoweidlem34  38927  fourierdlem20  39020  fouriersw  39124  nltle2tri  39942  iccelpart  39971