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 < π → exp 0 ball ⁡ abs ∘ − R ∈ J

Proof

Step Hyp Ref Expression
1 efopn.j ⊢ J = TopOpen ⁡ ℂ fld
2 logf1o ⊢ log : ℂ ∖ 0 ⟶ 1-1 onto ran ⁡ log
3 f1orn ⊢ log : ℂ ∖ 0 ⟶ 1-1 onto ran ⁡ log ↔ log Fn ℂ ∖ 0 ∧ Fun ⁡ log -1
4 3 simprbi ⊢ log : ℂ ∖ 0 ⟶ 1-1 onto ran ⁡ 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 -1 0 ball ⁡ abs ∘ − R = exp ↾ log ℂ ∖ −∞ 0 0 ball ⁡ 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 ∈ ℝ * → 0 ball ⁡ abs ∘ − R ⊆ ℂ
26 21 22 24 25 mp3an2i ⊢ R ∈ ℝ + ∧ R < π → 0 ball ⁡ abs ∘ − R ⊆ ℂ
27 26 sselda ⊢ R ∈ ℝ + ∧ R < π ∧ x ∈ 0 ball ⁡ abs ∘ − R → x ∈ ℂ
28 27 imcld ⊢ R ∈ ℝ + ∧ R < π ∧ x ∈ 0 ball ⁡ abs ∘ − R → ℑ ⁡ x ∈ ℝ
29 efopnlem1 ⊢ R ∈ ℝ + ∧ R < π ∧ x ∈ 0 ball ⁡ abs ∘ − R → ℑ ⁡ x < π
30 pire ⊢ π ∈ ℝ
31 abslt ⊢ ℑ ⁡ x ∈ ℝ ∧ π ∈ ℝ → ℑ ⁡ x < π ↔ − π < ℑ ⁡ x ∧ ℑ ⁡ x < π
32 28 30 31 sylancl ⊢ R ∈ ℝ + ∧ R < π ∧ x ∈ 0 ball ⁡ abs ∘ − R → ℑ ⁡ x < π ↔ − π < ℑ ⁡ x ∧ ℑ ⁡ x < π
33 29 32 mpbid ⊢ R ∈ ℝ + ∧ R < π ∧ x ∈ 0 ball ⁡ abs ∘ − R → − π < ℑ ⁡ x ∧ ℑ ⁡ x < π
34 33 simpld ⊢ R ∈ ℝ + ∧ R < π ∧ x ∈ 0 ball ⁡ abs ∘ − R → − π < ℑ ⁡ x
35 33 simprd ⊢ R ∈ ℝ + ∧ R < π ∧ x ∈ 0 ball ⁡ 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 ∈ 0 ball ⁡ 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 ∈ 0 ball ⁡ abs ∘ − R → x ∈ ℑ -1 − π π
47 46 ex ⊢ R ∈ ℝ + ∧ R < π → x ∈ 0 ball ⁡ abs ∘ − R → x ∈ ℑ -1 − π π
48 47 ssrdv ⊢ R ∈ ℝ + ∧ R < π → 0 ball ⁡ 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 < π → 0 ball ⁡ abs ∘ − R ⊆ log ℂ ∖ −∞ 0
57 resima2 ⊢ 0 ball ⁡ abs ∘ − R ⊆ log ℂ ∖ −∞ 0 → exp ↾ log ℂ ∖ −∞ 0 0 ball ⁡ abs ∘ − R = exp 0 ball ⁡ abs ∘ − R
58 56 57 syl ⊢ R ∈ ℝ + ∧ R < π → exp ↾ log ℂ ∖ −∞ 0 0 ball ⁡ abs ∘ − R = exp 0 ball ⁡ abs ∘ − R
59 20 58 syl5eq ⊢ R ∈ ℝ + ∧ R < π → log ↾ ℂ ∖ −∞ 0 -1 0 ball ⁡ abs ∘ − R = exp 0 ball ⁡ 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 ↾ 𝑡 ℂ ∖ −∞ 0 Cn J
67 61 62 66 mp2an ⊢ ℂ ∖ −∞ 0 ⟶cn ℂ = J ↾ 𝑡 ℂ ∖ −∞ 0 Cn J
68 60 67 eleqtri ⊢ log ↾ ℂ ∖ −∞ 0 ∈ J ↾ 𝑡 ℂ ∖ −∞ 0 Cn J
69 1 cnfldtopn ⊢ J = MetOpen ⁡ abs ∘ −
70 69 blopn ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ 0 ∈ ℂ ∧ R ∈ ℝ * → 0 ball ⁡ abs ∘ − R ∈ J
71 21 22 24 70 mp3an2i ⊢ R ∈ ℝ + ∧ R < π → 0 ball ⁡ abs ∘ − R ∈ J
72 cnima ⊢ log ↾ ℂ ∖ −∞ 0 ∈ J ↾ 𝑡 ℂ ∖ −∞ 0 Cn J ∧ 0 ball ⁡ abs ∘ − R ∈ J → log ↾ ℂ ∖ −∞ 0 -1 0 ball ⁡ abs ∘ − R ∈ J ↾ 𝑡 ℂ ∖ −∞ 0
73 68 71 72 sylancr ⊢ R ∈ ℝ + ∧ R < π → log ↾ ℂ ∖ −∞ 0 -1 0 ball ⁡ abs ∘ − R ∈ J ↾ 𝑡 ℂ ∖ −∞ 0
74 59 73 eqeltrrd ⊢ R ∈ ℝ + ∧ R < π → exp 0 ball ⁡ 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 → exp 0 ball ⁡ abs ∘ − R ∈ J ↾ 𝑡 ℂ ∖ −∞ 0 ↔ exp 0 ball ⁡ abs ∘ − R ∈ J ∧ exp 0 ball ⁡ abs ∘ − R ⊆ ℂ ∖ −∞ 0
79 75 77 78 mp2an ⊢ exp 0 ball ⁡ abs ∘ − R ∈ J ↾ 𝑡 ℂ ∖ −∞ 0 ↔ exp 0 ball ⁡ abs ∘ − R ∈ J ∧ exp 0 ball ⁡ abs ∘ − R ⊆ ℂ ∖ −∞ 0
80 74 79 sylib ⊢ R ∈ ℝ + ∧ R < π → exp 0 ball ⁡ abs ∘ − R ∈ J ∧ exp 0 ball ⁡ abs ∘ − R ⊆ ℂ ∖ −∞ 0
81 80 simpld ⊢ R ∈ ℝ + ∧ R < π → exp 0 ball ⁡ abs ∘ − R ∈ J