# Metamath Proof Explorer

## Theorem xrlenlt

Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion xrlenlt ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}\le {B}↔¬{B}<{A}\right)$

### Proof

Step Hyp Ref Expression
1 df-br ${⊢}{A}\le {B}↔⟨{A},{B}⟩\in \le$
2 opelxpi ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to ⟨{A},{B}⟩\in \left({ℝ}^{*}×{ℝ}^{*}\right)$
3 df-le ${⊢}\le =\left({ℝ}^{*}×{ℝ}^{*}\right)\setminus {<}^{-1}$
4 3 eleq2i ${⊢}⟨{A},{B}⟩\in \le ↔⟨{A},{B}⟩\in \left(\left({ℝ}^{*}×{ℝ}^{*}\right)\setminus {<}^{-1}\right)$
5 eldif ${⊢}⟨{A},{B}⟩\in \left(\left({ℝ}^{*}×{ℝ}^{*}\right)\setminus {<}^{-1}\right)↔\left(⟨{A},{B}⟩\in \left({ℝ}^{*}×{ℝ}^{*}\right)\wedge ¬⟨{A},{B}⟩\in {<}^{-1}\right)$
6 4 5 bitri ${⊢}⟨{A},{B}⟩\in \le ↔\left(⟨{A},{B}⟩\in \left({ℝ}^{*}×{ℝ}^{*}\right)\wedge ¬⟨{A},{B}⟩\in {<}^{-1}\right)$
7 6 baib ${⊢}⟨{A},{B}⟩\in \left({ℝ}^{*}×{ℝ}^{*}\right)\to \left(⟨{A},{B}⟩\in \le ↔¬⟨{A},{B}⟩\in {<}^{-1}\right)$
8 2 7 syl ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(⟨{A},{B}⟩\in \le ↔¬⟨{A},{B}⟩\in {<}^{-1}\right)$
9 1 8 syl5bb ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}\le {B}↔¬⟨{A},{B}⟩\in {<}^{-1}\right)$
10 opelcnvg ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(⟨{A},{B}⟩\in {<}^{-1}↔⟨{B},{A}⟩\in <\right)$
11 df-br ${⊢}{B}<{A}↔⟨{B},{A}⟩\in <$
12 10 11 syl6rbbr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({B}<{A}↔⟨{A},{B}⟩\in {<}^{-1}\right)$
13 12 notbid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬{B}<{A}↔¬⟨{A},{B}⟩\in {<}^{-1}\right)$
14 9 13 bitr4d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}\le {B}↔¬{B}<{A}\right)$