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 ∘ − ) ) 𝑅 ) ) ∈ 𝐽 )