Definition df-le 7159

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

Assertion

Ref	Expression
df-le	|- <_ = ( ( RR* X. RR* ) \ `' < )

Detailed syntax breakdown of Definition df-le

Step	Hyp	Ref	Expression
1		cle 7154	. 2 class <_
2		cxr 7152	. . . 4 class RR*
3	2, 2	cxp 4361	. . 3 class ( RR* X. RR* )
4		clt 7153	. . . 4 class <
5	4	ccnv 4362	. . 3 class `' <
6	3, 5	cdif 2970	. 2 class ( ( RR* X. RR* ) \ `' < )
7	1, 6	wceq 1284	1 wff <_ = ( ( RR* X. RR* ) \ `' < )

This definition is referenced by:  lerelxr  7175  xrlenlt  7177