Theorem dvtanlem

Description: Lemma for dvtan - the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018) (Proof shortened by OpenAI, 3-Jul-2020)

	Ref	Expression
Assertion	dvtanlem	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		coscn	$$⊢\cos :ℂ\underset{cn}{⟶}ℂ$$
2		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3	2	cncfcn1	$$⊢ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	1 3	eleqtri	$$⊢\cos \in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
5		cnn0opn	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6		cnima	$$⊢\left(\cos \in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
7	4 5 6	mp2an	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$