Theorem xrltnle 11304

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 11302	. . 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 2145   class class class wbr 5107  ℝ^*cxr 11270   < clt 11271   ≤ cle 11272

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 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-cnv 5667  df-le 11277

This theorem is used by:  xrltnled  11305  xrletri  13208  qextltlem  13258  xralrple  13261  xltadd1  13312  xsubge0  13317  xposdif  13318  xltmul1  13348  ioo0  13427  ico0  13448  ioc0  13449  snunioo  13535  snunioc  13537  difreicc  13541  hashbnd  14404  limsuplt  15570  pcadd  16987  pcadd2  16988  ramubcl  17116  ramlb  17117  leordtvallem1  23441  leordtvallem2  23442  leordtval2  23443  leordtval  23444  lecldbas  23450  blcld  24737  stdbdbl  24749  tmsxpsval2  24771  iocmnfcld  25000  xrsxmet  25042  metdsge  25082  bndth  25192  ovolgelb  25714  ovolunnul  25734  ioombl  25799  volsup2  25839  mbfmax  25883  ismbf3d  25888  itg2seq  25976  itg2monolem2  25985  itg2monolem3  25986  lhop2  26249  mdegleb  26296  deg1ge  26330  deg1add  26335  ig1pdvds  26412  plypf1  26445  radcnvlt1  26661  upgrfi  29556  xrdifh  33259  xrge00  33462  gsumesum  34577  itg2gt0cn  38432  asindmre  38460  dvasin  38461  aks6d1c6lem3  43046  aks6d1c7lem2  43055  iocioodisjd  43203  radcnvrat  45146  supxrgelem  46175  infrpge  46189  xrlexaddrp  46190  xrpnf  46321  gtnelioc  46329  ltnelicc  46335  gtnelicc  46338  snunioo1  46350  eliccnelico  46367  xrgtnelicc  46376  lptioo2  46469  stoweidlem34  46870  fourierdlem20  46963  fouriersw  47067  nltle2tri  48209  iccelpart  48341