Definition df-lt 9526

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

Assertion

Ref	Expression
df-lt

Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-lt

Step	Hyp	Ref	Expression
1		cltrr 9517	. 2
2		vx	. . . . . . 7
3	2	cv 1394	. . . . . 6
4		cr 9512	. . . . . 6
5	3, 4	wcel 1818	. . . . 5
6		vy	. . . . . . 7
7	6	cv 1394	. . . . . 6
8	7, 4	wcel 1818	. . . . 5
9	5, 8	wa 369	. . . 4
10		vz	. . . . . . . . . . 11
11	10	cv 1394	. . . . . . . . . 10
12		c0r 9265	. . . . . . . . . 10
13	11, 12	cop 4035	. . . . . . . . 9
14	3, 13	wceq 1395	. . . . . . . 8
15		vw	. . . . . . . . . . 11
16	15	cv 1394	. . . . . . . . . 10
17	16, 12	cop 4035	. . . . . . . . 9
18	7, 17	wceq 1395	. . . . . . . 8
19	14, 18	wa 369	. . . . . . 7
20		cltr 9270	. . . . . . . 8
21	11, 16, 20	wbr 4452	. . . . . . 7
22	19, 21	wa 369	. . . . . 6
23	22, 15	wex 1612	. . . . 5
24	23, 10	wex 1612	. . . 4
25	9, 24	wa 369	. . 3
26	25, 2, 6	copab 4509	. 2
27	1, 26	wceq 1395	1

This definition is referenced by:  ltrelre  9532  ltresr  9538