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 ) )