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	$$⊢\le =\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cle	$$class\le$$
1		cxr	$$class{ℝ}^{*}$$
2	1 1	cxp	$$class\left({ℝ}^{*}\times {ℝ}^{*}\right)$$
3		clt	$$class<$$
4	3	ccnv	$$class{<}^{-1}$$
5	2 4	cdif	$$class\left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}\right)$$
6	0 5	wceq	$$wff\le =\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}$$