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 \varnothing \in ℂ$$

Proof

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