MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-le Unicode version

Definition df-le 9177
Description: Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9212 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.)
Assertion
Ref Expression
df-le

Detailed syntax breakdown of Definition df-le
StepHypRef Expression
1 cle 9172 . 2
2 cxr 9170 . . . 4
32, 2cxp 4917 . . 3
4 clt 9171 . . . 4
54ccnv 4918 . . 3
63, 5cdif 3306 . 2
71, 6wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  lerelxr  9192  xrlenlt  9194  leiso  11759  gtiso  24136
  Copyright terms: Public domain W3C validator