Metamath Proof Explorer

Theorem xrletr

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

Ref Expression
Assertion xrletr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({A}\le {B}\wedge {B}\le {C}\right)\to {A}\le {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 2 adantr ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}\le {B}\right)\to \left({B}\le {C}↔\left({B}<{C}\vee {B}={C}\right)\right)$
4 xrlelttr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({A}\le {B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
5 xrltle ${⊢}\left({A}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({A}<{C}\to {A}\le {C}\right)$
6 5 3adant2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({A}<{C}\to {A}\le {C}\right)$
7 4 6 syld ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({A}\le {B}\wedge {B}<{C}\right)\to {A}\le {C}\right)$
8 7 expdimp ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}\le {B}\right)\to \left({B}<{C}\to {A}\le {C}\right)$
9 breq2 ${⊢}{B}={C}\to \left({A}\le {B}↔{A}\le {C}\right)$
10 9 biimpcd ${⊢}{A}\le {B}\to \left({B}={C}\to {A}\le {C}\right)$
11 10 adantl ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}\le {B}\right)\to \left({B}={C}\to {A}\le {C}\right)$
12 8 11 jaod ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}\le {B}\right)\to \left(\left({B}<{C}\vee {B}={C}\right)\to {A}\le {C}\right)$
13 3 12 sylbid ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge {A}\le {B}\right)\to \left({B}\le {C}\to {A}\le {C}\right)$
14 13 expimpd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({A}\le {B}\wedge {B}\le {C}\right)\to {A}\le {C}\right)$