Metamath Proof Explorer


Theorem xrlttr

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

Ref Expression
Assertion xrlttr A * B * C * A < B B < C A < C

Proof

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