Metamath Proof Explorer


Theorem ltsosr

Description: Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltsosr <𝑹Or𝑹

Proof

Step Hyp Ref Expression
1 df-nr 𝑹=𝑷×𝑷/~𝑹
2 breq1 xy~𝑹=fxy~𝑹<𝑹zw~𝑹f<𝑹zw~𝑹
3 eqeq1 xy~𝑹=fxy~𝑹=zw~𝑹f=zw~𝑹
4 breq2 xy~𝑹=fzw~𝑹<𝑹xy~𝑹zw~𝑹<𝑹f
5 3 4 orbi12d xy~𝑹=fxy~𝑹=zw~𝑹zw~𝑹<𝑹xy~𝑹f=zw~𝑹zw~𝑹<𝑹f
6 5 notbid xy~𝑹=f¬xy~𝑹=zw~𝑹zw~𝑹<𝑹xy~𝑹¬f=zw~𝑹zw~𝑹<𝑹f
7 2 6 bibi12d xy~𝑹=fxy~𝑹<𝑹zw~𝑹¬xy~𝑹=zw~𝑹zw~𝑹<𝑹xy~𝑹f<𝑹zw~𝑹¬f=zw~𝑹zw~𝑹<𝑹f
8 breq2 zw~𝑹=gf<𝑹zw~𝑹f<𝑹g
9 eqeq2 zw~𝑹=gf=zw~𝑹f=g
10 breq1 zw~𝑹=gzw~𝑹<𝑹fg<𝑹f
11 9 10 orbi12d zw~𝑹=gf=zw~𝑹zw~𝑹<𝑹ff=gg<𝑹f
12 11 notbid zw~𝑹=g¬f=zw~𝑹zw~𝑹<𝑹f¬f=gg<𝑹f
13 8 12 bibi12d zw~𝑹=gf<𝑹zw~𝑹¬f=zw~𝑹zw~𝑹<𝑹ff<𝑹g¬f=gg<𝑹f
14 ltsrpr xy~𝑹<𝑹zw~𝑹x+𝑷w<𝑷y+𝑷z
15 addclpr x𝑷w𝑷x+𝑷w𝑷
16 addclpr y𝑷z𝑷y+𝑷z𝑷
17 ltsopr <𝑷Or𝑷
18 sotric <𝑷Or𝑷x+𝑷w𝑷y+𝑷z𝑷x+𝑷w<𝑷y+𝑷z¬x+𝑷w=y+𝑷zy+𝑷z<𝑷x+𝑷w
19 17 18 mpan x+𝑷w𝑷y+𝑷z𝑷x+𝑷w<𝑷y+𝑷z¬x+𝑷w=y+𝑷zy+𝑷z<𝑷x+𝑷w
20 15 16 19 syl2an x𝑷w𝑷y𝑷z𝑷x+𝑷w<𝑷y+𝑷z¬x+𝑷w=y+𝑷zy+𝑷z<𝑷x+𝑷w
21 20 an42s x𝑷y𝑷z𝑷w𝑷x+𝑷w<𝑷y+𝑷z¬x+𝑷w=y+𝑷zy+𝑷z<𝑷x+𝑷w
22 enreceq x𝑷y𝑷z𝑷w𝑷xy~𝑹=zw~𝑹x+𝑷w=y+𝑷z
23 ltsrpr zw~𝑹<𝑹xy~𝑹z+𝑷y<𝑷w+𝑷x
24 addcompr z+𝑷y=y+𝑷z
25 addcompr w+𝑷x=x+𝑷w
26 24 25 breq12i z+𝑷y<𝑷w+𝑷xy+𝑷z<𝑷x+𝑷w
27 23 26 bitri zw~𝑹<𝑹xy~𝑹y+𝑷z<𝑷x+𝑷w
28 27 a1i x𝑷y𝑷z𝑷w𝑷zw~𝑹<𝑹xy~𝑹y+𝑷z<𝑷x+𝑷w
29 22 28 orbi12d x𝑷y𝑷z𝑷w𝑷xy~𝑹=zw~𝑹zw~𝑹<𝑹xy~𝑹x+𝑷w=y+𝑷zy+𝑷z<𝑷x+𝑷w
30 29 notbid x𝑷y𝑷z𝑷w𝑷¬xy~𝑹=zw~𝑹zw~𝑹<𝑹xy~𝑹¬x+𝑷w=y+𝑷zy+𝑷z<𝑷x+𝑷w
31 21 30 bitr4d x𝑷y𝑷z𝑷w𝑷x+𝑷w<𝑷y+𝑷z¬xy~𝑹=zw~𝑹zw~𝑹<𝑹xy~𝑹
32 14 31 syl5bb x𝑷y𝑷z𝑷w𝑷xy~𝑹<𝑹zw~𝑹¬xy~𝑹=zw~𝑹zw~𝑹<𝑹xy~𝑹
33 1 7 13 32 2ecoptocl f𝑹g𝑹f<𝑹g¬f=gg<𝑹f
34 2 anbi1d xy~𝑹=fxy~𝑹<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹f<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹
35 breq1 xy~𝑹=fxy~𝑹<𝑹vu~𝑹f<𝑹vu~𝑹
36 34 35 imbi12d xy~𝑹=fxy~𝑹<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹xy~𝑹<𝑹vu~𝑹f<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹f<𝑹vu~𝑹
37 breq1 zw~𝑹=gzw~𝑹<𝑹vu~𝑹g<𝑹vu~𝑹
38 8 37 anbi12d zw~𝑹=gf<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹f<𝑹gg<𝑹vu~𝑹
39 38 imbi1d zw~𝑹=gf<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹f<𝑹vu~𝑹f<𝑹gg<𝑹vu~𝑹f<𝑹vu~𝑹
40 breq2 vu~𝑹=hg<𝑹vu~𝑹g<𝑹h
41 40 anbi2d vu~𝑹=hf<𝑹gg<𝑹vu~𝑹f<𝑹gg<𝑹h
42 breq2 vu~𝑹=hf<𝑹vu~𝑹f<𝑹h
43 41 42 imbi12d vu~𝑹=hf<𝑹gg<𝑹vu~𝑹f<𝑹vu~𝑹f<𝑹gg<𝑹hf<𝑹h
44 ovex x+𝑷wV
45 ovex y+𝑷zV
46 ltapr h𝑷f<𝑷gh+𝑷f<𝑷h+𝑷g
47 vex uV
48 addcompr f+𝑷g=g+𝑷f
49 44 45 46 47 48 caovord2 u𝑷x+𝑷w<𝑷y+𝑷zx+𝑷w+𝑷u<𝑷y+𝑷z+𝑷u
50 addasspr x+𝑷w+𝑷u=x+𝑷w+𝑷u
51 addasspr y+𝑷z+𝑷u=y+𝑷z+𝑷u
52 50 51 breq12i x+𝑷w+𝑷u<𝑷y+𝑷z+𝑷ux+𝑷w+𝑷u<𝑷y+𝑷z+𝑷u
53 49 52 bitrdi u𝑷x+𝑷w<𝑷y+𝑷zx+𝑷w+𝑷u<𝑷y+𝑷z+𝑷u
54 14 53 syl5bb u𝑷xy~𝑹<𝑹zw~𝑹x+𝑷w+𝑷u<𝑷y+𝑷z+𝑷u
55 ltsrpr zw~𝑹<𝑹vu~𝑹z+𝑷u<𝑷w+𝑷v
56 ltapr y𝑷z+𝑷u<𝑷w+𝑷vy+𝑷z+𝑷u<𝑷y+𝑷w+𝑷v
57 55 56 syl5bb y𝑷zw~𝑹<𝑹vu~𝑹y+𝑷z+𝑷u<𝑷y+𝑷w+𝑷v
58 54 57 bi2anan9r y𝑷u𝑷xy~𝑹<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹x+𝑷w+𝑷u<𝑷y+𝑷z+𝑷uy+𝑷z+𝑷u<𝑷y+𝑷w+𝑷v
59 ltrelpr <𝑷𝑷×𝑷
60 17 59 sotri x+𝑷w+𝑷u<𝑷y+𝑷z+𝑷uy+𝑷z+𝑷u<𝑷y+𝑷w+𝑷vx+𝑷w+𝑷u<𝑷y+𝑷w+𝑷v
61 dmplp dom+𝑷=𝑷×𝑷
62 0npr ¬𝑷
63 ltapr w𝑷x+𝑷u<𝑷y+𝑷vw+𝑷x+𝑷u<𝑷w+𝑷y+𝑷v
64 61 59 62 63 ndmovordi w+𝑷x+𝑷u<𝑷w+𝑷y+𝑷vx+𝑷u<𝑷y+𝑷v
65 vex xV
66 vex wV
67 addasspr f+𝑷g+𝑷h=f+𝑷g+𝑷h
68 65 66 47 48 67 caov12 x+𝑷w+𝑷u=w+𝑷x+𝑷u
69 vex yV
70 vex vV
71 69 66 70 48 67 caov12 y+𝑷w+𝑷v=w+𝑷y+𝑷v
72 68 71 breq12i x+𝑷w+𝑷u<𝑷y+𝑷w+𝑷vw+𝑷x+𝑷u<𝑷w+𝑷y+𝑷v
73 ltsrpr xy~𝑹<𝑹vu~𝑹x+𝑷u<𝑷y+𝑷v
74 64 72 73 3imtr4i x+𝑷w+𝑷u<𝑷y+𝑷w+𝑷vxy~𝑹<𝑹vu~𝑹
75 60 74 syl x+𝑷w+𝑷u<𝑷y+𝑷z+𝑷uy+𝑷z+𝑷u<𝑷y+𝑷w+𝑷vxy~𝑹<𝑹vu~𝑹
76 58 75 syl6bi y𝑷u𝑷xy~𝑹<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹xy~𝑹<𝑹vu~𝑹
77 76 ad2ant2l x𝑷y𝑷v𝑷u𝑷xy~𝑹<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹xy~𝑹<𝑹vu~𝑹
78 77 3adant2 x𝑷y𝑷z𝑷w𝑷v𝑷u𝑷xy~𝑹<𝑹zw~𝑹zw~𝑹<𝑹vu~𝑹xy~𝑹<𝑹vu~𝑹
79 1 36 39 43 78 3ecoptocl f𝑹g𝑹h𝑹f<𝑹gg<𝑹hf<𝑹h
80 33 79 isso2i <𝑹Or𝑹