Theorem xrltnle 11248

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 11246	. . 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 5110  ℝ^*cxr 11214   < clt 11215   ≤ cle 11216

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-le 11221

This theorem is referenced by:  xrletri  13120  qextltlem  13169  xralrple  13172  xltadd1  13223  xsubge0  13228  xposdif  13229  xltmul1  13259  ioo0  13338  ico0  13359  ioc0  13360  snunioo  13446  snunioc  13448  difreicc  13452  hashbnd  14308  limsuplt  15452  pcadd  16867  pcadd2  16868  ramubcl  16996  ramlb  16997  leordtvallem1  23104  leordtvallem2  23105  leordtval2  23106  leordtval  23107  lecldbas  23113  blcld  24400  stdbdbl  24412  tmsxpsval2  24434  iocmnfcld  24663  xrsxmet  24705  metdsge  24745  bndth  24864  ovolgelb  25388  ovolunnul  25408  ioombl  25473  volsup2  25513  mbfmax  25557  ismbf3d  25562  itg2seq  25650  itg2monolem2  25659  itg2monolem3  25660  lhop2  25927  mdegleb  25976  deg1ge  26010  deg1add  26015  ig1pdvds  26092  plypf1  26124  radcnvlt1  26334  upgrfi  29025  xrdifh  32710  xrge00  32960  gsumesum  34056  itg2gt0cn  37676  asindmre  37704  dvasin  37705  aks6d1c6lem3  42167  aks6d1c7lem2  42176  iocioodisjd  42315  radcnvrat  44310  supxrgelem  45340  infrpge  45354  xrlexaddrp  45355  xrltnled  45366  xrpnf  45488  gtnelioc  45496  ltnelicc  45502  gtnelicc  45505  snunioo1  45517  eliccnelico  45534  xrgtnelicc  45543  lptioo2  45636  stoweidlem34  46039  fourierdlem20  46132  fouriersw  46236  nltle2tri  47318  iccelpart  47438