Theorem xrltnle 11380

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102  ℝ^*cxr 11346   < clt 11347   ≤ cle 11348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-le 11353

This theorem is used by:  xrltnled  11381  xrletri  13286  qextltlem  13336  xralrple  13339  xltadd1  13390  xsubge0  13395  xposdif  13396  xltmul1  13426  ioo0  13505  ico0  13526  ioc0  13527  snunioo  13613  snunioc  13615  difreicc  13619  hashbnd  14484  limsuplt  15652  pcadd  17073  pcadd2  17074  ramubcl  17202  ramlb  17203  leordtvallem1  23534  leordtvallem2  23535  leordtval2  23536  leordtval  23537  lecldbas  23543  blcld  24830  stdbdbl  24842  tmsxpsval2  24864  iocmnfcld  25093  xrsxmet  25135  metdsge  25175  bndth  25285  ovolgelb  25807  ovolunnul  25827  ioombl  25892  volsup2  25932  mbfmax  25976  ismbf3d  25981  itg2seq  26069  itg2monolem2  26078  itg2monolem3  26079  lhop2  26341  mdegleb  26388  deg1ge  26422  deg1add  26427  ig1pdvds  26504  plypf1  26537  radcnvlt1  26751  upgrfi  29675  xrdifh  33419  xrge00  33622  gsumesum  34738  itg2gt0cn  38687  asindmre  38715  dvasin  38716  aks6d1c6lem3  43316  aks6d1c7lem2  43325  iocioodisjd  43471  radcnvrat  45392  supxrgelem  46443  infrpge  46457  xrlexaddrp  46458  xrpnf  46589  gtnelioc  46597  ltnelicc  46603  gtnelicc  46606  snunioo1  46618  eliccnelico  46635  xrgtnelicc  46644  lptioo2  46737  stoweidlem34  47138  fourierdlem20  47231  fouriersw  47335  nltle2tri  48477  iccelpart  48609