Definition df-le 11298

Description: Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 11344 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

Step	Hyp	Ref	Expression
1		cle 11293	. 2 class ≤
2		cxr 11291	. . . 4 class ℝ*
3	2, 2	cxp 5686	. . 3 class (ℝ* × ℝ*)
4		clt 11292	. . . 4 class <
5	4	ccnv 5687	. . 3 class ◡ <
6	3, 5	cdif 3959	. 2 class ((ℝ* × ℝ*) ∖ ◡ < )
7	1, 6	wceq 1536	1 wff ≤ = ((ℝ* × ℝ*) ∖ ◡ < )

This definition is referenced by:  lerelxr  11321  xrlenlt  11323  leiso  14494  gtiso  32715