Theorem xrltnle 11188

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 11186	. . 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 5095  ℝ^*cxr 11154   < clt 11155   ≤ cle 11156

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 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-cnv 5629  df-le 11161

This theorem is referenced by:  xrltnled  11189  xrletri  13056  qextltlem  13105  xralrple  13108  xltadd1  13159  xsubge0  13164  xposdif  13165  xltmul1  13195  ioo0  13274  ico0  13295  ioc0  13296  snunioo  13382  snunioc  13384  difreicc  13388  hashbnd  14247  limsuplt  15390  pcadd  16805  pcadd2  16806  ramubcl  16934  ramlb  16935  leordtvallem1  23128  leordtvallem2  23129  leordtval2  23130  leordtval  23131  lecldbas  23137  blcld  24423  stdbdbl  24435  tmsxpsval2  24457  iocmnfcld  24686  xrsxmet  24728  metdsge  24768  bndth  24887  ovolgelb  25411  ovolunnul  25431  ioombl  25496  volsup2  25536  mbfmax  25580  ismbf3d  25585  itg2seq  25673  itg2monolem2  25682  itg2monolem3  25683  lhop2  25950  mdegleb  25999  deg1ge  26033  deg1add  26038  ig1pdvds  26115  plypf1  26147  radcnvlt1  26357  upgrfi  29073  xrdifh  32769  xrge00  33004  gsumesum  34095  itg2gt0cn  37738  asindmre  37766  dvasin  37767  aks6d1c6lem3  42288  aks6d1c7lem2  42297  iocioodisjd  42441  radcnvrat  44434  supxrgelem  45463  infrpge  45477  xrlexaddrp  45478  xrpnf  45610  gtnelioc  45618  ltnelicc  45624  gtnelicc  45627  snunioo1  45639  eliccnelico  45656  xrgtnelicc  45665  lptioo2  45758  stoweidlem34  46159  fourierdlem20  46252  fouriersw  46356  nltle2tri  47440  iccelpart  47560