df-le - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > df-le		GIF version

Definition df-le 7935

Description: Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.)

**Assertion**
Ref	Expression
df-le	⊢ ≤ = ((ℝ^* × ℝ^*) ∖ ^◡ < )

**Detailed syntax breakdown of Definition df-le**
Step	Hyp	Ref	Expression
1		cle 7930	. 2 class ≤
2		cxr 7928	. . . 4 class ℝ^*
3	2, 2	cxp 4601	. . 3 class (ℝ^* × ℝ^*)
4		clt 7929	. . . 4 class <
5	4	ccnv 4602	. . 3 class ^◡ <
6	3, 5	cdif 3112	. 2 class ((ℝ^* × ℝ^*) ∖ ^◡ < )
7	1, 6	wceq 1343	1 wff ≤ = ((ℝ^* × ℝ^*) ∖ ^◡ < )

Colors of variables: wff set class

This definition is referenced by: lerelxr 7957 xrlenlt 7959