Definition df-le 9655

Description: Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9692 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.)

Assertion

Ref	Expression
df-le

Detailed syntax breakdown of Definition df-le

Step	Hyp	Ref	Expression
1		cle 9650	. 2
2		cxr 9648	. . . 4
3	2, 2	cxp 5002	. . 3
4		clt 9649	. . . 4
5	4	ccnv 5003	. . 3
6	3, 5	cdif 3472	. 2
7	1, 6	wceq 1395	1

This definition is referenced by:  lerelxr  9671  xrlenlt  9673  leiso  12508  gtiso  27519