Theorem xrlenltd 11230

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

Step	Hyp	Ref	Expression
1		xrlenltd.a	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
2		xrlenltd.b	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
3		xrlenlt 11229	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2106   class class class wbr 5110  ℝ^*cxr 11197   < clt 11198   ≤ cle 11199

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-le 11204

This theorem is referenced by:  xrnltled  11232  supxrleub  13255  infxrgelb  13264  ixxub  13295  ixxlb  13296  icodisj  13403  supicclub2  13431  bldisj  23788  icombl  24965  ioorcl2  24973  ply1divmo  25537  ig1peu  25573  psercnlem1  25821  infxrge0gelb  31739  supxrgere  43688  supxrgelem  43692  lenelioc  43894  iccdificc  43897  limsupub  44065  fge0iccico  44731  sge0sn  44740  sge0rpcpnf  44782  pimltmnf2f  45058  pimconstlt0  45062  pimgtpnf2f  45066  pimdecfgtioo  45078  pimincfltioo  45079