Metamath Proof Explorer

Theorem xrlttri

Description: Ordering on the extended reals satisfies strict trichotomy. New proofs should generally use this instead of ax-pre-lttri or axlttri . (Contributed by NM, 14-Oct-2005)

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

Proof

Step Hyp Ref Expression
1 xrltnr 
 |-  ( A e. RR* -> -. A < A )
2 1 adantr 
 |-  ( ( A e. RR* /\ A = B ) -> -. A < A )
3 breq2 
 |-  ( A = B -> ( A < A <-> A < B ) )
4 3 adantl 
 |-  ( ( A e. RR* /\ A = B ) -> ( A < A <-> A < B ) )
5 2 4 mtbid 
 |-  ( ( A e. RR* /\ A = B ) -> -. A < B )
6 5 ex 
 |-  ( A e. RR* -> ( A = B -> -. A < B ) )
7 6 adantr 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B -> -. A < B ) )
8 xrltnsym 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B < A -> -. A < B ) )
9 8 ancoms 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B < A -> -. A < B ) )
10 7 9 jaod 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A = B \/ B < A ) -> -. A < B ) )
11 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
12 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
13 axlttri 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
14 13 biimprd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. ( A = B \/ B < A ) -> A < B ) )
15 14 con1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
16 ltpnf 
 |-  ( A e. RR -> A < +oo )
17 16 adantr 
 |-  ( ( A e. RR /\ B = +oo ) -> A < +oo )
18 breq2 
 |-  ( B = +oo -> ( A < B <-> A < +oo ) )
19 18 adantl 
 |-  ( ( A e. RR /\ B = +oo ) -> ( A < B <-> A < +oo ) )
20 17 19 mpbird 
 |-  ( ( A e. RR /\ B = +oo ) -> A < B )
21 20 pm2.24d 
 |-  ( ( A e. RR /\ B = +oo ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
22 mnflt 
 |-  ( A e. RR -> -oo < A )
23 22 adantr 
 |-  ( ( A e. RR /\ B = -oo ) -> -oo < A )
24 breq1 
 |-  ( B = -oo -> ( B < A <-> -oo < A ) )
25 24 adantl 
 |-  ( ( A e. RR /\ B = -oo ) -> ( B < A <-> -oo < A ) )
26 23 25 mpbird 
 |-  ( ( A e. RR /\ B = -oo ) -> B < A )
27 26 olcd 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A = B \/ B < A ) )
28 27 a1d 
 |-  ( ( A e. RR /\ B = -oo ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
29 15 21 28 3jaodan 
 |-  ( ( A e. RR /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
30 ltpnf 
 |-  ( B e. RR -> B < +oo )
31 30 adantl 
 |-  ( ( A = +oo /\ B e. RR ) -> B < +oo )
32 breq2 
 |-  ( A = +oo -> ( B < A <-> B < +oo ) )
33 32 adantr 
 |-  ( ( A = +oo /\ B e. RR ) -> ( B < A <-> B < +oo ) )
34 31 33 mpbird 
 |-  ( ( A = +oo /\ B e. RR ) -> B < A )
35 34 olcd 
 |-  ( ( A = +oo /\ B e. RR ) -> ( A = B \/ B < A ) )
36 35 a1d 
 |-  ( ( A = +oo /\ B e. RR ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
37 eqtr3 
 |-  ( ( A = +oo /\ B = +oo ) -> A = B )
38 37 orcd 
 |-  ( ( A = +oo /\ B = +oo ) -> ( A = B \/ B < A ) )
39 38 a1d 
 |-  ( ( A = +oo /\ B = +oo ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
40 mnfltpnf 
 |-  -oo < +oo
41 breq12 
 |-  ( ( B = -oo /\ A = +oo ) -> ( B < A <-> -oo < +oo ) )
42 40 41 mpbiri 
 |-  ( ( B = -oo /\ A = +oo ) -> B < A )
43 42 ancoms 
 |-  ( ( A = +oo /\ B = -oo ) -> B < A )
44 43 olcd 
 |-  ( ( A = +oo /\ B = -oo ) -> ( A = B \/ B < A ) )
45 44 a1d 
 |-  ( ( A = +oo /\ B = -oo ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
46 36 39 45 3jaodan 
 |-  ( ( A = +oo /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
47 mnflt 
 |-  ( 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 mpbird 
 |-  ( ( A = -oo /\ B e. RR ) -> A < B )
52 51 pm2.24d 
 |-  ( ( A = -oo /\ B e. RR ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
53 breq12 
 |-  ( ( A = -oo /\ B = +oo ) -> ( A < B <-> -oo < +oo ) )
54 40 53 mpbiri 
 |-  ( ( A = -oo /\ B = +oo ) -> A < B )
55 54 pm2.24d 
 |-  ( ( A = -oo /\ B = +oo ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
56 eqtr3 
 |-  ( ( A = -oo /\ B = -oo ) -> A = B )
57 56 orcd 
 |-  ( ( A = -oo /\ B = -oo ) -> ( A = B \/ B < A ) )
58 57 a1d 
 |-  ( ( A = -oo /\ B = -oo ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
59 52 55 58 3jaodan 
 |-  ( ( A = -oo /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
60 29 46 59 3jaoian 
 |-  ( ( ( A e. RR \/ A = +oo \/ A = -oo ) /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
61 11 12 60 syl2anb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. A < B -> ( A = B \/ B < A ) ) )
62 10 61 impbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A = B \/ B < A ) <-> -. A < B ) )
63 62 con2bid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )