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 x y ~ 𝑹 = f x y ~ 𝑹 < 𝑹 z w ~ 𝑹 f < 𝑹 z w ~ 𝑹
3 eqeq1 x y ~ 𝑹 = f x y ~ 𝑹 = z w ~ 𝑹 f = z w ~ 𝑹
4 breq2 x y ~ 𝑹 = f z w ~ 𝑹 < 𝑹 x y ~ 𝑹 z w ~ 𝑹 < 𝑹 f
5 3 4 orbi12d x y ~ 𝑹 = f x y ~ 𝑹 = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 x y ~ 𝑹 f = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 f
6 5 notbid x y ~ 𝑹 = f ¬ x y ~ 𝑹 = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 x y ~ 𝑹 ¬ f = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 f
7 2 6 bibi12d x y ~ 𝑹 = f x y ~ 𝑹 < 𝑹 z w ~ 𝑹 ¬ x y ~ 𝑹 = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 x y ~ 𝑹 f < 𝑹 z w ~ 𝑹 ¬ f = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 f
8 breq2 z w ~ 𝑹 = g f < 𝑹 z w ~ 𝑹 f < 𝑹 g
9 eqeq2 z w ~ 𝑹 = g f = z w ~ 𝑹 f = g
10 breq1 z w ~ 𝑹 = g z w ~ 𝑹 < 𝑹 f g < 𝑹 f
11 9 10 orbi12d z w ~ 𝑹 = g f = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 f f = g g < 𝑹 f
12 11 notbid z w ~ 𝑹 = g ¬ f = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 f ¬ f = g g < 𝑹 f
13 8 12 bibi12d z w ~ 𝑹 = g f < 𝑹 z w ~ 𝑹 ¬ f = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 f f < 𝑹 g ¬ f = g g < 𝑹 f
14 ltsrpr x y ~ 𝑹 < 𝑹 z w ~ 𝑹 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 + 𝑷 z y + 𝑷 z < 𝑷 x + 𝑷 w
19 17 18 mpan x + 𝑷 w 𝑷 y + 𝑷 z 𝑷 x + 𝑷 w < 𝑷 y + 𝑷 z ¬ x + 𝑷 w = y + 𝑷 z y + 𝑷 z < 𝑷 x + 𝑷 w
20 15 16 19 syl2an x 𝑷 w 𝑷 y 𝑷 z 𝑷 x + 𝑷 w < 𝑷 y + 𝑷 z ¬ x + 𝑷 w = y + 𝑷 z y + 𝑷 z < 𝑷 x + 𝑷 w
21 20 an42s x 𝑷 y 𝑷 z 𝑷 w 𝑷 x + 𝑷 w < 𝑷 y + 𝑷 z ¬ x + 𝑷 w = y + 𝑷 z y + 𝑷 z < 𝑷 x + 𝑷 w
22 enreceq x 𝑷 y 𝑷 z 𝑷 w 𝑷 x y ~ 𝑹 = z w ~ 𝑹 x + 𝑷 w = y + 𝑷 z
23 ltsrpr z w ~ 𝑹 < 𝑹 x y ~ 𝑹 z + 𝑷 y < 𝑷 w + 𝑷 x
24 addcompr z + 𝑷 y = y + 𝑷 z
25 addcompr w + 𝑷 x = x + 𝑷 w
26 24 25 breq12i z + 𝑷 y < 𝑷 w + 𝑷 x y + 𝑷 z < 𝑷 x + 𝑷 w
27 23 26 bitri z w ~ 𝑹 < 𝑹 x y ~ 𝑹 y + 𝑷 z < 𝑷 x + 𝑷 w
28 27 a1i x 𝑷 y 𝑷 z 𝑷 w 𝑷 z w ~ 𝑹 < 𝑹 x y ~ 𝑹 y + 𝑷 z < 𝑷 x + 𝑷 w
29 22 28 orbi12d x 𝑷 y 𝑷 z 𝑷 w 𝑷 x y ~ 𝑹 = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 x y ~ 𝑹 x + 𝑷 w = y + 𝑷 z y + 𝑷 z < 𝑷 x + 𝑷 w
30 29 notbid x 𝑷 y 𝑷 z 𝑷 w 𝑷 ¬ x y ~ 𝑹 = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 x y ~ 𝑹 ¬ x + 𝑷 w = y + 𝑷 z y + 𝑷 z < 𝑷 x + 𝑷 w
31 21 30 bitr4d x 𝑷 y 𝑷 z 𝑷 w 𝑷 x + 𝑷 w < 𝑷 y + 𝑷 z ¬ x y ~ 𝑹 = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 x y ~ 𝑹
32 14 31 syl5bb x 𝑷 y 𝑷 z 𝑷 w 𝑷 x y ~ 𝑹 < 𝑹 z w ~ 𝑹 ¬ x y ~ 𝑹 = z w ~ 𝑹 z w ~ 𝑹 < 𝑹 x y ~ 𝑹
33 1 7 13 32 2ecoptocl f 𝑹 g 𝑹 f < 𝑹 g ¬ f = g g < 𝑹 f
34 2 anbi1d x y ~ 𝑹 = f x y ~ 𝑹 < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 f < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹
35 breq1 x y ~ 𝑹 = f x y ~ 𝑹 < 𝑹 v u ~ 𝑹 f < 𝑹 v u ~ 𝑹
36 34 35 imbi12d x y ~ 𝑹 = f x y ~ 𝑹 < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 x y ~ 𝑹 < 𝑹 v u ~ 𝑹 f < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 f < 𝑹 v u ~ 𝑹
37 breq1 z w ~ 𝑹 = g z w ~ 𝑹 < 𝑹 v u ~ 𝑹 g < 𝑹 v u ~ 𝑹
38 8 37 anbi12d z w ~ 𝑹 = g f < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 f < 𝑹 g g < 𝑹 v u ~ 𝑹
39 38 imbi1d z w ~ 𝑹 = g f < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 f < 𝑹 v u ~ 𝑹 f < 𝑹 g g < 𝑹 v u ~ 𝑹 f < 𝑹 v u ~ 𝑹
40 breq2 v u ~ 𝑹 = h g < 𝑹 v u ~ 𝑹 g < 𝑹 h
41 40 anbi2d v u ~ 𝑹 = h f < 𝑹 g g < 𝑹 v u ~ 𝑹 f < 𝑹 g g < 𝑹 h
42 breq2 v u ~ 𝑹 = h f < 𝑹 v u ~ 𝑹 f < 𝑹 h
43 41 42 imbi12d v u ~ 𝑹 = h f < 𝑹 g g < 𝑹 v u ~ 𝑹 f < 𝑹 v u ~ 𝑹 f < 𝑹 g g < 𝑹 h f < 𝑹 h
44 ovex x + 𝑷 w V
45 ovex y + 𝑷 z V
46 ltapr h 𝑷 f < 𝑷 g h + 𝑷 f < 𝑷 h + 𝑷 g
47 vex u V
48 addcompr f + 𝑷 g = g + 𝑷 f
49 44 45 46 47 48 caovord2 u 𝑷 x + 𝑷 w < 𝑷 y + 𝑷 z x + 𝑷 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 + 𝑷 u x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 z + 𝑷 u
53 49 52 bitrdi u 𝑷 x + 𝑷 w < 𝑷 y + 𝑷 z x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 z + 𝑷 u
54 14 53 syl5bb u 𝑷 x y ~ 𝑹 < 𝑹 z w ~ 𝑹 x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 z + 𝑷 u
55 ltsrpr z w ~ 𝑹 < 𝑹 v u ~ 𝑹 z + 𝑷 u < 𝑷 w + 𝑷 v
56 ltapr y 𝑷 z + 𝑷 u < 𝑷 w + 𝑷 v y + 𝑷 z + 𝑷 u < 𝑷 y + 𝑷 w + 𝑷 v
57 55 56 syl5bb y 𝑷 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 y + 𝑷 z + 𝑷 u < 𝑷 y + 𝑷 w + 𝑷 v
58 54 57 bi2anan9r y 𝑷 u 𝑷 x y ~ 𝑹 < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 z + 𝑷 u y + 𝑷 z + 𝑷 u < 𝑷 y + 𝑷 w + 𝑷 v
59 ltrelpr < 𝑷 𝑷 × 𝑷
60 17 59 sotri x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 z + 𝑷 u y + 𝑷 z + 𝑷 u < 𝑷 y + 𝑷 w + 𝑷 v x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 w + 𝑷 v
61 dmplp dom + 𝑷 = 𝑷 × 𝑷
62 0npr ¬ 𝑷
63 ltapr w 𝑷 x + 𝑷 u < 𝑷 y + 𝑷 v w + 𝑷 x + 𝑷 u < 𝑷 w + 𝑷 y + 𝑷 v
64 61 59 62 63 ndmovordi w + 𝑷 x + 𝑷 u < 𝑷 w + 𝑷 y + 𝑷 v x + 𝑷 u < 𝑷 y + 𝑷 v
65 vex x V
66 vex w V
67 addasspr f + 𝑷 g + 𝑷 h = f + 𝑷 g + 𝑷 h
68 65 66 47 48 67 caov12 x + 𝑷 w + 𝑷 u = w + 𝑷 x + 𝑷 u
69 vex y V
70 vex v V
71 69 66 70 48 67 caov12 y + 𝑷 w + 𝑷 v = w + 𝑷 y + 𝑷 v
72 68 71 breq12i x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 w + 𝑷 v w + 𝑷 x + 𝑷 u < 𝑷 w + 𝑷 y + 𝑷 v
73 ltsrpr x y ~ 𝑹 < 𝑹 v u ~ 𝑹 x + 𝑷 u < 𝑷 y + 𝑷 v
74 64 72 73 3imtr4i x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 w + 𝑷 v x y ~ 𝑹 < 𝑹 v u ~ 𝑹
75 60 74 syl x + 𝑷 w + 𝑷 u < 𝑷 y + 𝑷 z + 𝑷 u y + 𝑷 z + 𝑷 u < 𝑷 y + 𝑷 w + 𝑷 v x y ~ 𝑹 < 𝑹 v u ~ 𝑹
76 58 75 syl6bi y 𝑷 u 𝑷 x y ~ 𝑹 < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 x y ~ 𝑹 < 𝑹 v u ~ 𝑹
77 76 ad2ant2l x 𝑷 y 𝑷 v 𝑷 u 𝑷 x y ~ 𝑹 < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 x y ~ 𝑹 < 𝑹 v u ~ 𝑹
78 77 3adant2 x 𝑷 y 𝑷 z 𝑷 w 𝑷 v 𝑷 u 𝑷 x y ~ 𝑹 < 𝑹 z w ~ 𝑹 z w ~ 𝑹 < 𝑹 v u ~ 𝑹 x y ~ 𝑹 < 𝑹 v u ~ 𝑹
79 1 36 39 43 78 3ecoptocl f 𝑹 g 𝑹 h 𝑹 f < 𝑹 g g < 𝑹 h f < 𝑹 h
80 33 79 isso2i < 𝑹 Or 𝑹