Definition df-le 6658

Description: Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 6688 relates it to 'less than' for reals.

Assertion

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

Detailed syntax breakdown of Definition df-le

Step	Hyp	Ref	Expression
1		cle 6448	. 2 class <_
2		cxr 6652	. . . 4 class RR*
3	2, 2	cxp 3984	. . 3 class (RR* X. RR*)
4		clt 6653	. . . 4 class <
5	4	ccnv 3985	. . 3 class `' <
6	3, 5	cdif 2590	. 2 class ((RR* X. RR*) \ `' < )
7	1, 6	wceq 1298	1 wff <_ = ((RR* X. RR*) \ `' < )

This definition is referenced by:  xrlenlt 6670  mlteqer 15017  ranleqt 15021  leqrl 15022  lteqtpos 15024

Copyright terms: Public domain