Metamath Proof Explorer


Theorem xrlttr

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

Ref Expression
Assertion xrlttr
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B < C ) -> A < C ) )

Proof

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