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

Definition df-le 9303
Description: Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9340 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 9298 . 2
2 cxr 9296 . . . 4
32, 2cxp 4860 . . 3
4 clt 9297 . . . 4
54ccnv 4861 . . 3
63, 5cdif 3362 . 2
71, 6wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  lerelxr  9319  xrlenlt  9321  leiso  12059  gtiso  25126
  Copyright terms: Public domain W3C validator