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

Metamath Proof Explorer

Theorem 0ncn

Description: The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by NM, 2-May-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	0ncn	$⊢ \neg \emptyset \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		0nelxp	$⊢ \neg \emptyset \in (𝑹 \times 𝑹)$
2		df-c	$⊢ ℂ = 𝑹 \times 𝑹$
3	2	eleq2i	$⊢ \emptyset \in ℂ \leftrightarrow \emptyset \in (𝑹 \times 𝑹)$
4	1 3	mtbir	$⊢ \neg \emptyset \in ℂ$