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*B*A<B¬A=BB<A

Proof

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