Metamath Proof Explorer

Definition df-ltr

Description: Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.4 of Gleason p. 127. (Contributed by NM, 14-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion df-ltr 
|- . | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltr 
 |-
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 cnr 
 |-  R.
5 3 4 wcel 
 |-  x e. R.
6 2 cv 
 |-  y
7 6 4 wcel 
 |-  y e. R.
8 5 7 wa 
 |-  ( x e. R. /\ y e. R. )
9 vz 
 |-  z
10 vw 
 |-  w
11 vv 
 |-  v
12 vu 
 |-  u
13 9 cv 
 |-  z
14 10 cv 
 |-  w
15 13 14 cop 
 |-  <. z , w >.
16 cer 
 |-  ~R
17 15 16 cec 
 |-  [ <. z , w >. ] ~R
18 3 17 wceq 
 |-  x = [ <. z , w >. ] ~R
19 11 cv 
 |-  v
20 12 cv 
 |-  u
21 19 20 cop 
 |-  <. v , u >.
22 21 16 cec 
 |-  [ <. v , u >. ] ~R
23 6 22 wceq 
 |-  y = [ <. v , u >. ] ~R
24 18 23 wa 
 |-  ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R )
25 cpp 
 |-  +P.
26 13 20 25 co 
 |-  ( z +P. u )
27 cltp 
 |-
28 14 19 25 co 
 |-  ( w +P. v )
29 26 28 27 wbr 
 |-  ( z +P. u )
30 24 29 wa 
 |-  ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
31 30 12 wex 
 |-  E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
32 31 11 wex 
 |-  E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
33 32 10 wex 
 |-  E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
34 33 9 wex 
 |-  E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
35 8 34 wa 
 |-  ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
36 35 1 2 copab 
 |-  { <. x , y >. | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
37 0 36 wceq 
 |-  . | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )