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		cnn0opn	⊢ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld )
6		cnima	⊢ ( ( cos ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld ) ) → ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld ) )
7	4 5 6	mp2an	⊢ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld )