Metamath Proof Explorer

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 ℂ ∖ 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 -1 ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld
14 4 12 13 mp2an ⊢ cos -1 ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld