# Metamath Proof Explorer

## Theorem xrltletr

Description: Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006)

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

### Proof

Step Hyp Ref Expression
1 xrleloe ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B}\le {C}↔\left({B}<{C}\vee {B}={C}\right)\right)$
2 1 3adant1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B}\le {C}↔\left({B}<{C}\vee {B}={C}\right)\right)$
3 xrlttr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
4 3 expcomd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B}<{C}\to \left({A}<{B}\to {A}<{C}\right)\right)$
5 breq2 ${⊢}{B}={C}\to \left({A}<{B}↔{A}<{C}\right)$
6 5 biimpd ${⊢}{B}={C}\to \left({A}<{B}\to {A}<{C}\right)$
7 6 a1i ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B}={C}\to \left({A}<{B}\to {A}<{C}\right)\right)$
8 4 7 jaod ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({B}<{C}\vee {B}={C}\right)\to \left({A}<{B}\to {A}<{C}\right)\right)$
9 2 8 sylbid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B}\le {C}\to \left({A}<{B}\to {A}<{C}\right)\right)$
10 9 impcomd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({A}<{B}\wedge {B}\le {C}\right)\to {A}<{C}\right)$