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