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 “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		coscn	⊢ cos ∈ ( ℂ –cn→ ℂ )
2		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3	2	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
4	1 3	eleqtri	⊢ cos ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
5	2	cnfldhaus	⊢ ( TopOpen ‘ ℂfld ) ∈ Haus
6		0cn	⊢ 0 ∈ ℂ
7	2	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
8	7	toponunii	⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
9	8	sncld	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Haus ∧ 0 ∈ ℂ ) → { 0 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
10	5 6 9	mp2an	⊢ { 0 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) )
11	8	cldopn	⊢ ( { 0 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) → ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld ) )
12	10 11	ax-mp	⊢ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld )
13		cnima	⊢ ( ( cos ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld ) ) → ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld ) )
14	4 12 13	mp2an	⊢ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld )