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