Metamath Proof Explorer

Theorem logdmopn

Description: The "continuous domain" of log is an open set. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypothesis logcn.d ⊢ D = ℂ ∖ −∞ 0
Assertion logdmopn ⊢ D ∈ TopOpen ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 logcn.d ⊢ D = ℂ ∖ −∞ 0
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 2 recld2 ⊢ ℝ ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
4 0re ⊢ 0 ∈ ℝ
5 iocmnfcld ⊢ 0 ∈ ℝ → −∞ 0 ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
6 4 5 ax-mp ⊢ −∞ 0 ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
7 tgioo4 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
8 7 fveq2i ⊢ Clsd ⁡ topGen ⁡ ran ⁡ . = Clsd ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
9 6 8 eleqtri ⊢ −∞ 0 ∈ Clsd ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
10 restcldr ⊢ ℝ ∈ Clsd ⁡ TopOpen ⁡ ℂ fld ∧ −∞ 0 ∈ Clsd ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ → −∞ 0 ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
11 3 9 10 mp2an ⊢ −∞ 0 ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
12 unicntop ⊢ ℂ = ⋃ TopOpen ⁡ ℂ fld
13 12 cldopn ⊢ −∞ 0 ∈ Clsd ⁡ TopOpen ⁡ ℂ fld → ℂ ∖ −∞ 0 ∈ TopOpen ⁡ ℂ fld
14 11 13 ax-mp ⊢ ℂ ∖ −∞ 0 ∈ TopOpen ⁡ ℂ fld
15 1 14 eqeltri ⊢ D ∈ TopOpen ⁡ ℂ fld