Theorem cnn0opn

Description: The set of nonzero complex numbers is open with respect to the standard topology on complex numbers. (Contributed by SN, 7-Oct-2025)

	Ref	Expression
Assertion	cnn0opn	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	cnfldhaus	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}$$
3		0cn	$$⊢0\in ℂ$$
4		unicntop	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
5	4	sncld	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}\wedge 0\in ℂ\right)\to \left\{0\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
6	2 3 5	mp2an	$$⊢\left\{0\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
7	4	cldopn	$$⊢\left\{0\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
8	6 7	ax-mp	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$