MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrlenltd Structured version   Visualization version   GIF version

Theorem xrlenltd 10101
Description: 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
xrlenltd.a (𝜑𝐴 ∈ ℝ*)
xrlenltd.b (𝜑𝐵 ∈ ℝ*)
Assertion
Ref Expression
xrlenltd (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem xrlenltd
StepHypRef Expression
1 xrlenltd.a . 2 (𝜑𝐴 ∈ ℝ*)
2 xrlenltd.b . 2 (𝜑𝐵 ∈ ℝ*)
3 xrlenlt 10100 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2anc 693 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wcel 1989   class class class wbr 4651  *cxr 10070   < clt 10071  cle 10072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-br 4652  df-opab 4711  df-xp 5118  df-cnv 5120  df-le 10077
This theorem is referenced by:  infxrgelb  12162  ixxlb  12194  infxrge0gelb  29516  supxrgere  39368  supxrgelem  39372  lenelioc  39572  iccdificc  39575  limsupub  39742  fge0iccico  40356  sge0sn  40365  sge0rpcpnf  40407  pimltmnf2  40680  pimconstlt0  40683  pimgtpnf2  40686  pimdecfgtioo  40696  pimincfltioo  40697
  Copyright terms: Public domain W3C validator