Metamath Proof Explorer

Theorem xrltnsym

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

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

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
3 ltnsym 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
4 rexr 
 |-  ( A e. RR -> A e. RR* )
5 pnfnlt 
 |-  ( A e. RR* -> -. +oo < A )
6 4 5 syl 
 |-  ( A e. RR -> -. +oo < A )
7 6 adantr 
 |-  ( ( A e. RR /\ B = +oo ) -> -. +oo < A )
8 breq1 
 |-  ( B = +oo -> ( B < A <-> +oo < A ) )
9 8 adantl 
 |-  ( ( A e. RR /\ B = +oo ) -> ( B < A <-> +oo < A ) )
10 7 9 mtbird 
 |-  ( ( A e. RR /\ B = +oo ) -> -. B < A )
11 10 a1d 
 |-  ( ( A e. RR /\ B = +oo ) -> ( A < B -> -. B < A ) )
12 nltmnf 
 |-  ( A e. RR* -> -. A < -oo )
13 4 12 syl 
 |-  ( A e. RR -> -. A < -oo )
14 13 adantr 
 |-  ( ( A e. RR /\ B = -oo ) -> -. A < -oo )
15 breq2 
 |-  ( B = -oo -> ( A < B <-> A < -oo ) )
16 15 adantl 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A < B <-> A < -oo ) )
17 14 16 mtbird 
 |-  ( ( A e. RR /\ B = -oo ) -> -. A < B )
18 17 pm2.21d 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A < B -> -. B < A ) )
19 3 11 18 3jaodan 
 |-  ( ( A e. RR /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A < B -> -. B < A ) )
20 pnfnlt 
 |-  ( B e. RR* -> -. +oo < B )
21 20 adantl 
 |-  ( ( A = +oo /\ B e. RR* ) -> -. +oo < B )
22 breq1 
 |-  ( A = +oo -> ( A < B <-> +oo < B ) )
23 22 adantr 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( A < B <-> +oo < B ) )
24 21 23 mtbird 
 |-  ( ( A = +oo /\ B e. RR* ) -> -. A < B )
25 24 pm2.21d 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( A < B -> -. B < A ) )
26 2 25 sylan2br 
 |-  ( ( A = +oo /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A < B -> -. B < A ) )
27 rexr 
 |-  ( B e. RR -> B e. RR* )
28 nltmnf 
 |-  ( B e. RR* -> -. B < -oo )
29 27 28 syl 
 |-  ( B e. RR -> -. B < -oo )
30 29 adantl 
 |-  ( ( A = -oo /\ B e. RR ) -> -. B < -oo )
31 breq2 
 |-  ( A = -oo -> ( B < A <-> B < -oo ) )
32 31 adantr 
 |-  ( ( A = -oo /\ B e. RR ) -> ( B < A <-> B < -oo ) )
33 30 32 mtbird 
 |-  ( ( A = -oo /\ B e. RR ) -> -. B < A )
34 33 a1d 
 |-  ( ( A = -oo /\ B e. RR ) -> ( A < B -> -. B < A ) )
35 mnfxr 
 |-  -oo e. RR*
36 pnfnlt 
 |-  ( -oo e. RR* -> -. +oo < -oo )
37 35 36 ax-mp 
 |-  -. +oo < -oo
38 breq12 
 |-  ( ( B = +oo /\ A = -oo ) -> ( B < A <-> +oo < -oo ) )
39 37 38 mtbiri 
 |-  ( ( B = +oo /\ A = -oo ) -> -. B < A )
40 39 ancoms 
 |-  ( ( A = -oo /\ B = +oo ) -> -. B < A )
41 40 a1d 
 |-  ( ( A = -oo /\ B = +oo ) -> ( A < B -> -. B < A ) )
42 xrltnr 
 |-  ( -oo e. RR* -> -. -oo < -oo )
43 35 42 ax-mp 
 |-  -. -oo < -oo
44 breq12 
 |-  ( ( A = -oo /\ B = -oo ) -> ( A < B <-> -oo < -oo ) )
45 43 44 mtbiri 
 |-  ( ( A = -oo /\ B = -oo ) -> -. A < B )
46 45 pm2.21d 
 |-  ( ( A = -oo /\ B = -oo ) -> ( A < B -> -. B < A ) )
47 34 41 46 3jaodan 
 |-  ( ( A = -oo /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A < B -> -. B < A ) )
48 19 26 47 3jaoian 
 |-  ( ( ( A e. RR \/ A = +oo \/ A = -oo ) /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A < B -> -. B < A ) )
49 1 2 48 syl2anb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> -. B < A ) )