Theorem xrltnle 11241

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ℝ^*cxr 11207   < clt 11208   ≤ cle 11209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-le 11214

This theorem is referenced by:  xrletri  13113  qextltlem  13162  xralrple  13165  xltadd1  13216  xsubge0  13221  xposdif  13222  xltmul1  13252  ioo0  13331  ico0  13352  ioc0  13353  snunioo  13439  snunioc  13441  difreicc  13445  hashbnd  14301  limsuplt  15445  pcadd  16860  pcadd2  16861  ramubcl  16989  ramlb  16990  leordtvallem1  23097  leordtvallem2  23098  leordtval2  23099  leordtval  23100  lecldbas  23106  blcld  24393  stdbdbl  24405  tmsxpsval2  24427  iocmnfcld  24656  xrsxmet  24698  metdsge  24738  bndth  24857  ovolgelb  25381  ovolunnul  25401  ioombl  25466  volsup2  25506  mbfmax  25550  ismbf3d  25555  itg2seq  25643  itg2monolem2  25652  itg2monolem3  25653  lhop2  25920  mdegleb  25969  deg1ge  26003  deg1add  26008  ig1pdvds  26085  plypf1  26117  radcnvlt1  26327  upgrfi  29018  xrdifh  32703  xrge00  32953  gsumesum  34049  itg2gt0cn  37669  asindmre  37697  dvasin  37698  aks6d1c6lem3  42160  aks6d1c7lem2  42169  iocioodisjd  42308  radcnvrat  44303  supxrgelem  45333  infrpge  45347  xrlexaddrp  45348  xrltnled  45359  xrpnf  45481  gtnelioc  45489  ltnelicc  45495  gtnelicc  45498  snunioo1  45510  eliccnelico  45527  xrgtnelicc  45536  lptioo2  45629  stoweidlem34  46032  fourierdlem20  46125  fouriersw  46229  nltle2tri  47314  iccelpart  47434