Description: Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | df-le | |- <_ = ( ( RR* X. RR* ) \ `' < ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cle | |- <_ |
|
1 | cxr | |- RR* |
|
2 | 1 1 | cxp | |- ( RR* X. RR* ) |
3 | clt | |- < |
|
4 | 3 | ccnv | |- `' < |
5 | 2 4 | cdif | |- ( ( RR* X. RR* ) \ `' < ) |
6 | 0 5 | wceq | |- <_ = ( ( RR* X. RR* ) \ `' < ) |