Theorem xrltnle 10708

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114   class class class wbr 5066  ℝ^*cxr 10674   < clt 10675   ≤ cle 10676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-le 10681

This theorem is referenced by:  xrletri  12547  qextltlem  12596  xralrple  12599  xltadd1  12650  xsubge0  12655  xposdif  12656  xltmul1  12686  ioo0  12764  ico0  12785  ioc0  12786  snunioo  12865  snunioc  12867  difreicc  12871  hashbnd  13697  limsuplt  14836  pcadd  16225  pcadd2  16226  ramubcl  16354  ramlb  16355  leordtvallem1  21818  leordtvallem2  21819  leordtval2  21820  leordtval  21821  lecldbas  21827  blcld  23115  stdbdbl  23127  tmsxpsval2  23149  iocmnfcld  23377  xrsxmet  23417  metdsge  23457  bndth  23562  ovolgelb  24081  ovolunnul  24101  ioombl  24166  volsup2  24206  mbfmax  24250  ismbf3d  24255  itg2seq  24343  itg2monolem2  24352  itg2monolem3  24353  lhop2  24612  mdegleb  24658  deg1ge  24692  deg1add  24697  ig1pdvds  24770  plypf1  24802  radcnvlt1  25006  upgrfi  26876  xrdifh  30503  xrge00  30673  gsumesum  31318  itg2gt0cn  34962  asindmre  34992  dvasin  34993  radcnvrat  40695  supxrgelem  41654  infrpge  41668  xrlexaddrp  41669  xrltnled  41680  xrpnf  41811  gtnelioc  41814  ltnelicc  41821  gtnelicc  41824  snunioo1  41837  eliccnelico  41854  xrgtnelicc  41863  lptioo2  41961  stoweidlem34  42368  fourierdlem20  42461  fouriersw  42565  nltle2tri  43562  iccelpart  43642