# Metamath Proof Explorer

## Theorem xrlttr

Description: Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005)

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

### Proof

Step Hyp Ref Expression
1 elxr ${⊢}{A}\in {ℝ}^{*}↔\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)$
2 elxr ${⊢}{C}\in {ℝ}^{*}↔\left({C}\in ℝ\vee {C}=\mathrm{+\infty }\vee {C}=\mathrm{-\infty }\right)$
3 elxr ${⊢}{B}\in {ℝ}^{*}↔\left({B}\in ℝ\vee {B}=\mathrm{+\infty }\vee {B}=\mathrm{-\infty }\right)$
4 lttr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
5 4 3expa ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
6 5 an32s ${⊢}\left(\left({A}\in ℝ\wedge {C}\in ℝ\right)\wedge {B}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
7 rexr ${⊢}{C}\in ℝ\to {C}\in {ℝ}^{*}$
8 pnfnlt ${⊢}{C}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{C}$
9 7 8 syl ${⊢}{C}\in ℝ\to ¬\mathrm{+\infty }<{C}$
10 9 adantr ${⊢}\left({C}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to ¬\mathrm{+\infty }<{C}$
11 breq1 ${⊢}{B}=\mathrm{+\infty }\to \left({B}<{C}↔\mathrm{+\infty }<{C}\right)$
12 11 adantl ${⊢}\left({C}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to \left({B}<{C}↔\mathrm{+\infty }<{C}\right)$
13 10 12 mtbird ${⊢}\left({C}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to ¬{B}<{C}$
14 13 pm2.21d ${⊢}\left({C}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to \left({B}<{C}\to {A}<{C}\right)$
15 14 adantll ${⊢}\left(\left({A}\in ℝ\wedge {C}\in ℝ\right)\wedge {B}=\mathrm{+\infty }\right)\to \left({B}<{C}\to {A}<{C}\right)$
16 15 adantld ${⊢}\left(\left({A}\in ℝ\wedge {C}\in ℝ\right)\wedge {B}=\mathrm{+\infty }\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
17 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
18 nltmnf ${⊢}{A}\in {ℝ}^{*}\to ¬{A}<\mathrm{-\infty }$
19 17 18 syl ${⊢}{A}\in ℝ\to ¬{A}<\mathrm{-\infty }$
20 19 adantr ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{-\infty }\right)\to ¬{A}<\mathrm{-\infty }$
21 breq2 ${⊢}{B}=\mathrm{-\infty }\to \left({A}<{B}↔{A}<\mathrm{-\infty }\right)$
22 21 adantl ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{-\infty }\right)\to \left({A}<{B}↔{A}<\mathrm{-\infty }\right)$
23 20 22 mtbird ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{-\infty }\right)\to ¬{A}<{B}$
24 23 pm2.21d ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{-\infty }\right)\to \left({A}<{B}\to {A}<{C}\right)$
25 24 adantlr ${⊢}\left(\left({A}\in ℝ\wedge {C}\in ℝ\right)\wedge {B}=\mathrm{-\infty }\right)\to \left({A}<{B}\to {A}<{C}\right)$
26 25 adantrd ${⊢}\left(\left({A}\in ℝ\wedge {C}\in ℝ\right)\wedge {B}=\mathrm{-\infty }\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
27 6 16 26 3jaodan ${⊢}\left(\left({A}\in ℝ\wedge {C}\in ℝ\right)\wedge \left({B}\in ℝ\vee {B}=\mathrm{+\infty }\vee {B}=\mathrm{-\infty }\right)\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
28 3 27 sylan2b ${⊢}\left(\left({A}\in ℝ\wedge {C}\in ℝ\right)\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
29 28 an32s ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
30 ltpnf ${⊢}{A}\in ℝ\to {A}<\mathrm{+\infty }$
31 30 adantr ${⊢}\left({A}\in ℝ\wedge {C}=\mathrm{+\infty }\right)\to {A}<\mathrm{+\infty }$
32 breq2 ${⊢}{C}=\mathrm{+\infty }\to \left({A}<{C}↔{A}<\mathrm{+\infty }\right)$
33 32 adantl ${⊢}\left({A}\in ℝ\wedge {C}=\mathrm{+\infty }\right)\to \left({A}<{C}↔{A}<\mathrm{+\infty }\right)$
34 31 33 mpbird ${⊢}\left({A}\in ℝ\wedge {C}=\mathrm{+\infty }\right)\to {A}<{C}$
35 34 adantlr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}<{C}$
36 35 a1d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge {C}=\mathrm{+\infty }\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
37 nltmnf ${⊢}{B}\in {ℝ}^{*}\to ¬{B}<\mathrm{-\infty }$
38 37 adantr ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}=\mathrm{-\infty }\right)\to ¬{B}<\mathrm{-\infty }$
39 breq2 ${⊢}{C}=\mathrm{-\infty }\to \left({B}<{C}↔{B}<\mathrm{-\infty }\right)$
40 39 adantl ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}=\mathrm{-\infty }\right)\to \left({B}<{C}↔{B}<\mathrm{-\infty }\right)$
41 38 40 mtbird ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}=\mathrm{-\infty }\right)\to ¬{B}<{C}$
42 41 pm2.21d ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}=\mathrm{-\infty }\right)\to \left({B}<{C}\to {A}<{C}\right)$
43 42 adantld ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}=\mathrm{-\infty }\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
44 43 adantll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge {C}=\mathrm{-\infty }\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
45 29 36 44 3jaodan ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\vee {C}=\mathrm{-\infty }\right)\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
46 45 anasss ${⊢}\left({A}\in ℝ\wedge \left({B}\in {ℝ}^{*}\wedge \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\vee {C}=\mathrm{-\infty }\right)\right)\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
47 pnfnlt ${⊢}{B}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{B}$
48 47 adantl ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to ¬\mathrm{+\infty }<{B}$
49 breq1 ${⊢}{A}=\mathrm{+\infty }\to \left({A}<{B}↔\mathrm{+\infty }<{B}\right)$
50 49 adantr ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}↔\mathrm{+\infty }<{B}\right)$
51 48 50 mtbird ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to ¬{A}<{B}$
52 51 pm2.21d ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}\to {A}<{C}\right)$
53 52 adantrd ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
54 53 adantrr ${⊢}\left({A}=\mathrm{+\infty }\wedge \left({B}\in {ℝ}^{*}\wedge \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\vee {C}=\mathrm{-\infty }\right)\right)\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
55 mnflt ${⊢}{C}\in ℝ\to \mathrm{-\infty }<{C}$
56 55 adantl ${⊢}\left({A}=\mathrm{-\infty }\wedge {C}\in ℝ\right)\to \mathrm{-\infty }<{C}$
57 breq1 ${⊢}{A}=\mathrm{-\infty }\to \left({A}<{C}↔\mathrm{-\infty }<{C}\right)$
58 57 adantr ${⊢}\left({A}=\mathrm{-\infty }\wedge {C}\in ℝ\right)\to \left({A}<{C}↔\mathrm{-\infty }<{C}\right)$
59 56 58 mpbird ${⊢}\left({A}=\mathrm{-\infty }\wedge {C}\in ℝ\right)\to {A}<{C}$
60 59 a1d ${⊢}\left({A}=\mathrm{-\infty }\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
61 60 adantlr ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in {ℝ}^{*}\right)\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
62 mnfltpnf ${⊢}\mathrm{-\infty }<\mathrm{+\infty }$
63 breq12 ${⊢}\left({A}=\mathrm{-\infty }\wedge {C}=\mathrm{+\infty }\right)\to \left({A}<{C}↔\mathrm{-\infty }<\mathrm{+\infty }\right)$
64 62 63 mpbiri ${⊢}\left({A}=\mathrm{-\infty }\wedge {C}=\mathrm{+\infty }\right)\to {A}<{C}$
65 64 a1d ${⊢}\left({A}=\mathrm{-\infty }\wedge {C}=\mathrm{+\infty }\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
66 65 adantlr ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in {ℝ}^{*}\right)\wedge {C}=\mathrm{+\infty }\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
67 43 adantll ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in {ℝ}^{*}\right)\wedge {C}=\mathrm{-\infty }\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
68 61 66 67 3jaodan ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\vee {C}=\mathrm{-\infty }\right)\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
69 68 anasss ${⊢}\left({A}=\mathrm{-\infty }\wedge \left({B}\in {ℝ}^{*}\wedge \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\vee {C}=\mathrm{-\infty }\right)\right)\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
70 46 54 69 3jaoian ${⊢}\left(\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\vee {C}=\mathrm{-\infty }\right)\right)\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
71 70 3impb ${⊢}\left(\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\wedge {B}\in {ℝ}^{*}\wedge \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\vee {C}=\mathrm{-\infty }\right)\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
72 2 71 syl3an3b ${⊢}\left(\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
73 1 72 syl3an1b ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$