Metamath Proof Explorer

Theorem efopnlem2

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

Ref Expression
Hypothesis efopn.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion efopnlem2 ( ( 𝑅 ∈ ℝ+ ∧ 𝑅 < π ) → ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ∈ 𝐽 )

Proof

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