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

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