# Metamath Proof Explorer

## Theorem xrleloe

Description: 'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006)

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

### Proof

Step Hyp Ref Expression
1 xrlenlt ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}\le {B}↔¬{B}<{A}\right)$
2 eqcom ${⊢}{B}={A}↔{A}={B}$
3 2 orbi1i ${⊢}\left({B}={A}\vee {A}<{B}\right)↔\left({A}={B}\vee {A}<{B}\right)$
4 orcom ${⊢}\left({A}={B}\vee {A}<{B}\right)↔\left({A}<{B}\vee {A}={B}\right)$
5 3 4 bitri ${⊢}\left({B}={A}\vee {A}<{B}\right)↔\left({A}<{B}\vee {A}={B}\right)$
6 xrlttri ${⊢}\left({B}\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left({B}<{A}↔¬\left({B}={A}\vee {A}<{B}\right)\right)$
7 6 ancoms ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({B}<{A}↔¬\left({B}={A}\vee {A}<{B}\right)\right)$
8 7 con2bid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({B}={A}\vee {A}<{B}\right)↔¬{B}<{A}\right)$
9 5 8 syl5rbbr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(¬{B}<{A}↔\left({A}<{B}\vee {A}={B}\right)\right)$
10 1 9 bitrd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}\le {B}↔\left({A}<{B}\vee {A}={B}\right)\right)$