Definition df-le 9177

Description: Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9212 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 9172	. 2
2		cxr 9170	. . . 4
3	2, 2	cxp 4917	. . 3
4		clt 9171	. . . 4
5	4	ccnv 4918	. . 3
6	3, 5	cdif 3306	. 2
7	1, 6	wceq 1654	1

This definition is referenced by:  lerelxr  9192  xrlenlt  9194  leiso  11759  gtiso  24136