Theorem xrltnle 11042

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   class class class wbr 5074  ℝ^*cxr 11008   < clt 11009   ≤ cle 11010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-le 11015

This theorem is referenced by:  xrletri  12887  qextltlem  12936  xralrple  12939  xltadd1  12990  xsubge0  12995  xposdif  12996  xltmul1  13026  ioo0  13104  ico0  13125  ioc0  13126  snunioo  13210  snunioc  13212  difreicc  13216  hashbnd  14050  limsuplt  15188  pcadd  16590  pcadd2  16591  ramubcl  16719  ramlb  16720  leordtvallem1  22361  leordtvallem2  22362  leordtval2  22363  leordtval  22364  lecldbas  22370  blcld  23661  stdbdbl  23673  tmsxpsval2  23695  iocmnfcld  23932  xrsxmet  23972  metdsge  24012  bndth  24121  ovolgelb  24644  ovolunnul  24664  ioombl  24729  volsup2  24769  mbfmax  24813  ismbf3d  24818  itg2seq  24907  itg2monolem2  24916  itg2monolem3  24917  lhop2  25179  mdegleb  25229  deg1ge  25263  deg1add  25268  ig1pdvds  25341  plypf1  25373  radcnvlt1  25577  upgrfi  27461  xrdifh  31101  xrge00  31295  gsumesum  32027  itg2gt0cn  35832  asindmre  35860  dvasin  35861  radcnvrat  41932  supxrgelem  42876  infrpge  42890  xrlexaddrp  42891  xrltnled  42902  xrpnf  43026  gtnelioc  43029  ltnelicc  43035  gtnelicc  43038  snunioo1  43050  eliccnelico  43067  xrgtnelicc  43076  lptioo2  43172  stoweidlem34  43575  fourierdlem20  43668  fouriersw  43772  nltle2tri  44805  iccelpart  44885