Theorem xrltnle 11328

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5143  ℝ^*cxr 11294   < clt 11295   ≤ cle 11296

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-le 11301

This theorem is referenced by:  xrletri  13195  qextltlem  13244  xralrple  13247  xltadd1  13298  xsubge0  13303  xposdif  13304  xltmul1  13334  ioo0  13412  ico0  13433  ioc0  13434  snunioo  13518  snunioc  13520  difreicc  13524  hashbnd  14375  limsuplt  15515  pcadd  16927  pcadd2  16928  ramubcl  17056  ramlb  17057  leordtvallem1  23218  leordtvallem2  23219  leordtval2  23220  leordtval  23221  lecldbas  23227  blcld  24518  stdbdbl  24530  tmsxpsval2  24552  iocmnfcld  24789  xrsxmet  24831  metdsge  24871  bndth  24990  ovolgelb  25515  ovolunnul  25535  ioombl  25600  volsup2  25640  mbfmax  25684  ismbf3d  25689  itg2seq  25777  itg2monolem2  25786  itg2monolem3  25787  lhop2  26054  mdegleb  26103  deg1ge  26137  deg1add  26142  ig1pdvds  26219  plypf1  26251  radcnvlt1  26461  upgrfi  29108  xrdifh  32782  xrge00  33017  gsumesum  34060  itg2gt0cn  37682  asindmre  37710  dvasin  37711  aks6d1c6lem3  42173  aks6d1c7lem2  42182  iocioodisjd  42355  radcnvrat  44333  supxrgelem  45348  infrpge  45362  xrlexaddrp  45363  xrltnled  45374  xrpnf  45496  gtnelioc  45504  ltnelicc  45510  gtnelicc  45513  snunioo1  45525  eliccnelico  45542  xrgtnelicc  45551  lptioo2  45646  stoweidlem34  46049  fourierdlem20  46142  fouriersw  46246  nltle2tri  47325  iccelpart  47420