Theorem xrltnle 11294

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 11292	. . 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 2146   class class class wbr 5114  ℝ^*cxr 11260   < clt 11261   ≤ cle 11262

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-le 11267

This theorem is used by:  xrltnled  11295  xrletri  13196  qextltlem  13246  xralrple  13249  xltadd1  13300  xsubge0  13305  xposdif  13306  xltmul1  13336  ioo0  13415  ico0  13436  ioc0  13437  snunioo  13523  snunioc  13525  difreicc  13529  hashbnd  14392  limsuplt  15556  pcadd  16974  pcadd2  16975  ramubcl  17103  ramlb  17104  leordtvallem1  23404  leordtvallem2  23405  leordtval2  23406  leordtval  23407  lecldbas  23413  blcld  24699  stdbdbl  24711  tmsxpsval2  24733  iocmnfcld  24962  xrsxmet  25004  metdsge  25044  bndth  25154  ovolgelb  25676  ovolunnul  25696  ioombl  25761  volsup2  25801  mbfmax  25845  ismbf3d  25850  itg2seq  25938  itg2monolem2  25947  itg2monolem3  25948  lhop2  26211  mdegleb  26258  deg1ge  26292  deg1add  26297  ig1pdvds  26374  plypf1  26406  radcnvlt1  26618  upgrfi  29478  xrdifh  33162  xrge00  33365  gsumesum  34480  itg2gt0cn  38367  asindmre  38395  dvasin  38396  aks6d1c6lem3  42980  aks6d1c7lem2  42989  iocioodisjd  43122  radcnvrat  45065  supxrgelem  46094  infrpge  46108  xrlexaddrp  46109  xrpnf  46240  gtnelioc  46248  ltnelicc  46254  gtnelicc  46257  snunioo1  46269  eliccnelico  46286  xrgtnelicc  46295  lptioo2  46388  stoweidlem34  46789  fourierdlem20  46882  fouriersw  46986  nltle2tri  48091  iccelpart  48223