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	⊢ ≤ = ( ( ℝ* × ℝ* ) ∖ ◡ < )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cle	⊢ ≤
1		cxr	⊢ ℝ*
2	1 1	cxp	⊢ ( ℝ* × ℝ* )
3		clt	⊢ <
4	3	ccnv	⊢ ◡ <
5	2 4	cdif	⊢ ( ( ℝ* × ℝ* ) ∖ ◡ < )
6	0 5	wceq	⊢ ≤ = ( ( ℝ* × ℝ* ) ∖ ◡ < )