# Metamath Proof Explorer

## Theorem xrletri3

Description: Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009)

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

### Proof

Step Hyp Ref Expression
1 xrlttri3 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}={B}↔\left(¬{A}<{B}\wedge ¬{B}<{A}\right)\right)$
2 1 biancomd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}={B}↔\left(¬{B}<{A}\wedge ¬{A}<{B}\right)\right)$
3 xrlenlt ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}\le {B}↔¬{B}<{A}\right)$
4 xrlenlt ${⊢}\left({B}\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
5 4 ancoms ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
6 3 5 anbi12d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A}\le {B}\wedge {B}\le {A}\right)↔\left(¬{B}<{A}\wedge ¬{A}<{B}\right)\right)$
7 2 6 bitr4d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}={B}↔\left({A}\le {B}\wedge {B}\le {A}\right)\right)$