Metamath Proof Explorer


Definition df-le

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* ) \ `' < )

Detailed syntax breakdown

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* ) \ `' < )