This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \leq = (ℝ^{} \times ℝ^{}) ∖ <^{-1}$

Detailed syntax breakdown

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