Metamath Proof Explorer

Theorem efopnlem2

Description: Lemma for efopn . (Contributed by Mario Carneiro, 2-May-2015)

Ref Expression
Hypothesis efopn.j ⊢J=TopOpen⁡ℂfld
Assertion efopnlem2 ⊢R∈ℝ+∧R<π→exp0ball⁡abs∘−R∈J

Proof

Step Hyp Ref Expression
1 efopn.j ⊢J=TopOpen⁡ℂfld
2 logf1o ⊢log:ℂ∖0⟶1-1 ontoran⁡log
3 f1orn ⊢log:ℂ∖0⟶1-1 ontoran⁡log↔logFnℂ∖0∧Fun⁡log-1
4 3 simprbi ⊢log:ℂ∖0⟶1-1 ontoran⁡log→Fun⁡log-1
5 funcnvres ⊢Fun⁡log-1→log↾ℂ∖−∞0-1=log-1↾logℂ∖−∞0
6 2 4 5 mp2b ⊢log↾ℂ∖−∞0-1=log-1↾logℂ∖−∞0
7 df-log ⊢log=exp↾ℑ-1−ππ-1
8 7 cnveqi ⊢log-1=exp↾ℑ-1−ππ-1-1
9 relres ⊢Rel⁡exp↾ℑ-1−ππ
10 dfrel2 ⊢Rel⁡exp↾ℑ-1−ππ↔exp↾ℑ-1−ππ-1-1=exp↾ℑ-1−ππ
11 9 10 mpbi ⊢exp↾ℑ-1−ππ-1-1=exp↾ℑ-1−ππ
12 8 11 eqtri ⊢log-1=exp↾ℑ-1−ππ
13 12 reseq1i ⊢log-1↾logℂ∖−∞0=exp↾ℑ-1−ππ↾logℂ∖−∞0
14 imassrn ⊢logℂ∖−∞0⊆ran⁡log
15 logrn ⊢ran⁡log=ℑ-1−ππ
16 14 15 sseqtri ⊢logℂ∖−∞0⊆ℑ-1−ππ
17 resabs1 ⊢logℂ∖−∞0⊆ℑ-1−ππ→exp↾ℑ-1−ππ↾logℂ∖−∞0=exp↾logℂ∖−∞0
18 16 17 ax-mp ⊢exp↾ℑ-1−ππ↾logℂ∖−∞0=exp↾logℂ∖−∞0
19 6 13 18 3eqtri ⊢log↾ℂ∖−∞0-1=exp↾logℂ∖−∞0
20 19 imaeq1i ⊢log↾ℂ∖−∞0-10ball⁡abs∘−R=exp↾logℂ∖−∞00ball⁡abs∘−R
21 cnxmet ⊢abs∘−∈∞Met⁡ℂ
22 0cnd ⊢R∈ℝ+∧R<π→0∈ℂ
23 rpxr ⊢R∈ℝ+→R∈ℝ*
24 23 adantr ⊢R∈ℝ+∧R<π→R∈ℝ*
25 blssm ⊢abs∘−∈∞Met⁡ℂ∧0∈ℂ∧R∈ℝ*→0ball⁡abs∘−R⊆ℂ
26 21 22 24 25 mp3an2i ⊢R∈ℝ+∧R<π→0ball⁡abs∘−R⊆ℂ
27 26 sselda ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→x∈ℂ
28 27 imcld ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→ℑ⁡x∈ℝ
29 efopnlem1 ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→ℑ⁡x<π
30 pire ⊢π∈ℝ
31 abslt ⊢ℑ⁡x∈ℝ∧π∈ℝ→ℑ⁡x<π↔−π<ℑ⁡x∧ℑ⁡x<π
32 28 30 31 sylancl ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→ℑ⁡x<π↔−π<ℑ⁡x∧ℑ⁡x<π
33 29 32 mpbid ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→−π<ℑ⁡x∧ℑ⁡x<π
34 33 simpld ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→−π<ℑ⁡x
35 33 simprd ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→ℑ⁡x<π
36 30 renegcli ⊢−π∈ℝ
37 36 rexri ⊢−π∈ℝ*
38 30 rexri ⊢π∈ℝ*
39 elioo2 ⊢−π∈ℝ*∧π∈ℝ*→ℑ⁡x∈−ππ↔ℑ⁡x∈ℝ∧−π<ℑ⁡x∧ℑ⁡x<π
40 37 38 39 mp2an ⊢ℑ⁡x∈−ππ↔ℑ⁡x∈ℝ∧−π<ℑ⁡x∧ℑ⁡x<π
41 28 34 35 40 syl3anbrc ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→ℑ⁡x∈−ππ
42 imf ⊢ℑ:ℂ⟶ℝ
43 ffn ⊢ℑ:ℂ⟶ℝ→ℑFnℂ
44 elpreima ⊢ℑFnℂ→x∈ℑ-1−ππ↔x∈ℂ∧ℑ⁡x∈−ππ
45 42 43 44 mp2b ⊢x∈ℑ-1−ππ↔x∈ℂ∧ℑ⁡x∈−ππ
46 27 41 45 sylanbrc ⊢R∈ℝ+∧R<π∧x∈0ball⁡abs∘−R→x∈ℑ-1−ππ
47 46 ex ⊢R∈ℝ+∧R<π→x∈0ball⁡abs∘−R→x∈ℑ-1−ππ
48 47 ssrdv ⊢R∈ℝ+∧R<π→0ball⁡abs∘−R⊆ℑ-1−ππ
49 df-ima ⊢logℂ∖−∞0=ran⁡log↾ℂ∖−∞0
50 eqid ⊢ℂ∖−∞0=ℂ∖−∞0
51 50 logf1o2 ⊢log↾ℂ∖−∞0:ℂ∖−∞0⟶1-1 ontoℑ-1−ππ
52 f1ofo ⊢log↾ℂ∖−∞0:ℂ∖−∞0⟶1-1 ontoℑ-1−ππ→log↾ℂ∖−∞0:ℂ∖−∞0⟶ontoℑ-1−ππ
53 forn ⊢log↾ℂ∖−∞0:ℂ∖−∞0⟶ontoℑ-1−ππ→ran⁡log↾ℂ∖−∞0=ℑ-1−ππ
54 51 52 53 mp2b ⊢ran⁡log↾ℂ∖−∞0=ℑ-1−ππ
55 49 54 eqtri ⊢logℂ∖−∞0=ℑ-1−ππ
56 48 55 sseqtrrdi ⊢R∈ℝ+∧R<π→0ball⁡abs∘−R⊆logℂ∖−∞0
57 resima2 ⊢0ball⁡abs∘−R⊆logℂ∖−∞0→exp↾logℂ∖−∞00ball⁡abs∘−R=exp0ball⁡abs∘−R
58 56 57 syl ⊢R∈ℝ+∧R<π→exp↾logℂ∖−∞00ball⁡abs∘−R=exp0ball⁡abs∘−R
59 20 58 eqtrid ⊢R∈ℝ+∧R<π→log↾ℂ∖−∞0-10ball⁡abs∘−R=exp0ball⁡abs∘−R
60 50 logcn ⊢log↾ℂ∖−∞0:ℂ∖−∞0⟶cnℂ
61 difss ⊢ℂ∖−∞0⊆ℂ
62 ssid ⊢ℂ⊆ℂ
63 eqid ⊢J↾𝑡ℂ∖−∞0=J↾𝑡ℂ∖−∞0
64 1 cnfldtopon ⊢J∈TopOn⁡ℂ
65 64 toponrestid ⊢J=J↾𝑡ℂ
66 1 63 65 cncfcn ⊢ℂ∖−∞0⊆ℂ∧ℂ⊆ℂ→ℂ∖−∞0⟶cnℂ=J↾𝑡ℂ∖−∞0CnJ
67 61 62 66 mp2an ⊢ℂ∖−∞0⟶cnℂ=J↾𝑡ℂ∖−∞0CnJ
68 60 67 eleqtri ⊢log↾ℂ∖−∞0∈J↾𝑡ℂ∖−∞0CnJ
69 1 cnfldtopn ⊢J=MetOpen⁡abs∘−
70 69 blopn ⊢abs∘−∈∞Met⁡ℂ∧0∈ℂ∧R∈ℝ*→0ball⁡abs∘−R∈J
71 21 22 24 70 mp3an2i ⊢R∈ℝ+∧R<π→0ball⁡abs∘−R∈J
72 cnima ⊢log↾ℂ∖−∞0∈J↾𝑡ℂ∖−∞0CnJ∧0ball⁡abs∘−R∈J→log↾ℂ∖−∞0-10ball⁡abs∘−R∈J↾𝑡ℂ∖−∞0
73 68 71 72 sylancr ⊢R∈ℝ+∧R<π→log↾ℂ∖−∞0-10ball⁡abs∘−R∈J↾𝑡ℂ∖−∞0
74 59 73 eqeltrrd ⊢R∈ℝ+∧R<π→exp0ball⁡abs∘−R∈J↾𝑡ℂ∖−∞0
75 1 cnfldtop ⊢J∈Top
76 50 logdmopn ⊢ℂ∖−∞0∈TopOpen⁡ℂfld
77 76 1 eleqtrri ⊢ℂ∖−∞0∈J
78 restopn2 ⊢J∈Top∧ℂ∖−∞0∈J→exp0ball⁡abs∘−R∈J↾𝑡ℂ∖−∞0↔exp0ball⁡abs∘−R∈J∧exp0ball⁡abs∘−R⊆ℂ∖−∞0
79 75 77 78 mp2an ⊢exp0ball⁡abs∘−R∈J↾𝑡ℂ∖−∞0↔exp0ball⁡abs∘−R∈J∧exp0ball⁡abs∘−R⊆ℂ∖−∞0
80 74 79 sylib ⊢R∈ℝ+∧R<π→exp0ball⁡abs∘−R∈J∧exp0ball⁡abs∘−R⊆ℂ∖−∞0
81 80 simpld ⊢R∈ℝ+∧R<π→exp0ball⁡abs∘−R∈J