# Metamath Proof Explorer

## Theorem xrltnsym

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

Ref Expression
Assertion xrltnsym ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}\to ¬{B}<{A}\right)$

### Proof

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