Theorem xrltnle 11303

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 11301	. . 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 11269   < clt 11270   ≤ cle 11271

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 11276

This theorem is used by:  xrltnled  11304  xrletri  13206  qextltlem  13256  xralrple  13259  xltadd1  13310  xsubge0  13315  xposdif  13316  xltmul1  13346  ioo0  13425  ico0  13446  ioc0  13447  snunioo  13533  snunioc  13535  difreicc  13539  hashbnd  14402  limsuplt  15568  pcadd  16985  pcadd2  16986  ramubcl  17114  ramlb  17115  leordtvallem1  23439  leordtvallem2  23440  leordtval2  23441  leordtval  23442  lecldbas  23448  blcld  24735  stdbdbl  24747  tmsxpsval2  24769  iocmnfcld  24998  xrsxmet  25040  metdsge  25080  bndth  25190  ovolgelb  25712  ovolunnul  25732  ioombl  25797  volsup2  25837  mbfmax  25881  ismbf3d  25886  itg2seq  25974  itg2monolem2  25983  itg2monolem3  25984  lhop2  26247  mdegleb  26294  deg1ge  26328  deg1add  26333  ig1pdvds  26410  plypf1  26442  radcnvlt1  26654  upgrfi  29549  xrdifh  33253  xrge00  33456  gsumesum  34571  itg2gt0cn  38426  asindmre  38454  dvasin  38455  aks6d1c6lem3  43040  aks6d1c7lem2  43049  iocioodisjd  43197  radcnvrat  45140  supxrgelem  46169  infrpge  46183  xrlexaddrp  46184  xrpnf  46315  gtnelioc  46323  ltnelicc  46329  gtnelicc  46332  snunioo1  46344  eliccnelico  46361  xrgtnelicc  46370  lptioo2  46463  stoweidlem34  46864  fourierdlem20  46957  fouriersw  47061  nltle2tri  48203  iccelpart  48335