Metamath Proof Explorer


Definition df-lt

Description: Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr . (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion df-lt
|- . | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltrr
 |-  
1 vx
 |-  x
2 vy
 |-  y
3 1 cv
 |-  x
4 cr
 |-  RR
5 3 4 wcel
 |-  x e. RR
6 2 cv
 |-  y
7 6 4 wcel
 |-  y e. RR
8 5 7 wa
 |-  ( x e. RR /\ y e. RR )
9 vz
 |-  z
10 vw
 |-  w
11 9 cv
 |-  z
12 c0r
 |-  0R
13 11 12 cop
 |-  <. z , 0R >.
14 3 13 wceq
 |-  x = <. z , 0R >.
15 10 cv
 |-  w
16 15 12 cop
 |-  <. w , 0R >.
17 6 16 wceq
 |-  y = <. w , 0R >.
18 14 17 wa
 |-  ( x = <. z , 0R >. /\ y = <. w , 0R >. )
19 cltr
 |-  
20 11 15 19 wbr
 |-  z 
21 18 20 wa
 |-  ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
22 21 10 wex
 |-  E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
23 22 9 wex
 |-  E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
24 8 23 wa
 |-  ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
25 24 1 2 copab
 |-  { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
26 0 25 wceq
 |-  . | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z