Theorem xrltnle 11199

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2113   class class class wbr 5098  ℝ^*cxr 11165   < clt 11166   ≤ cle 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-le 11172

This theorem is referenced by:  xrltnled  11200  xrletri  13067  qextltlem  13117  xralrple  13120  xltadd1  13171  xsubge0  13176  xposdif  13177  xltmul1  13207  ioo0  13286  ico0  13307  ioc0  13308  snunioo  13394  snunioc  13396  difreicc  13400  hashbnd  14259  limsuplt  15402  pcadd  16817  pcadd2  16818  ramubcl  16946  ramlb  16947  leordtvallem1  23154  leordtvallem2  23155  leordtval2  23156  leordtval  23157  lecldbas  23163  blcld  24449  stdbdbl  24461  tmsxpsval2  24483  iocmnfcld  24712  xrsxmet  24754  metdsge  24794  bndth  24913  ovolgelb  25437  ovolunnul  25457  ioombl  25522  volsup2  25562  mbfmax  25606  ismbf3d  25611  itg2seq  25699  itg2monolem2  25708  itg2monolem3  25709  lhop2  25976  mdegleb  26025  deg1ge  26059  deg1add  26064  ig1pdvds  26141  plypf1  26173  radcnvlt1  26383  upgrfi  29164  xrdifh  32860  xrge00  33096  gsumesum  34216  itg2gt0cn  37876  asindmre  37904  dvasin  37905  aks6d1c6lem3  42426  aks6d1c7lem2  42435  iocioodisjd  42575  radcnvrat  44555  supxrgelem  45582  infrpge  45596  xrlexaddrp  45597  xrpnf  45729  gtnelioc  45737  ltnelicc  45743  gtnelicc  45746  snunioo1  45758  eliccnelico  45775  xrgtnelicc  45784  lptioo2  45877  stoweidlem34  46278  fourierdlem20  46371  fouriersw  46475  nltle2tri  47559  iccelpart  47679