Theorem xrltnle 11211

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5100  ℝ^*cxr 11177   < clt 11178   ≤ cle 11179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-le 11184

This theorem is referenced by:  xrltnled  11212  xrletri  13079  qextltlem  13129  xralrple  13132  xltadd1  13183  xsubge0  13188  xposdif  13189  xltmul1  13219  ioo0  13298  ico0  13319  ioc0  13320  snunioo  13406  snunioc  13408  difreicc  13412  hashbnd  14271  limsuplt  15414  pcadd  16829  pcadd2  16830  ramubcl  16958  ramlb  16959  leordtvallem1  23166  leordtvallem2  23167  leordtval2  23168  leordtval  23169  lecldbas  23175  blcld  24461  stdbdbl  24473  tmsxpsval2  24495  iocmnfcld  24724  xrsxmet  24766  metdsge  24806  bndth  24925  ovolgelb  25449  ovolunnul  25469  ioombl  25534  volsup2  25574  mbfmax  25618  ismbf3d  25623  itg2seq  25711  itg2monolem2  25720  itg2monolem3  25721  lhop2  25988  mdegleb  26037  deg1ge  26071  deg1add  26076  ig1pdvds  26153  plypf1  26185  radcnvlt1  26395  upgrfi  29176  xrdifh  32870  xrge00  33106  gsumesum  34236  itg2gt0cn  37923  asindmre  37951  dvasin  37952  aks6d1c6lem3  42539  aks6d1c7lem2  42548  iocioodisjd  42687  radcnvrat  44667  supxrgelem  45693  infrpge  45707  xrlexaddrp  45708  xrpnf  45840  gtnelioc  45848  ltnelicc  45854  gtnelicc  45857  snunioo1  45869  eliccnelico  45886  xrgtnelicc  45895  lptioo2  45988  stoweidlem34  46389  fourierdlem20  46482  fouriersw  46586  nltle2tri  47670  iccelpart  47790