Definition df-le 9303

Description: Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9340 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 9298	. 2
2		cxr 9296	. . . 4
3	2, 2	cxp 4860	. . 3
4		clt 9297	. . . 4
5	4	ccnv 4861	. . 3
6	3, 5	cdif 3362	. 2
7	1, 6	wceq 1670	1

This definition is referenced by:  lerelxr  9319  xrlenlt  9321  leiso  12059  gtiso  25126