Metamath Proof Explorer

Theorem eff1olem

Description: The exponential function maps the set S , of complex numbers with imaginary part in a real interval of length 2 x. _pi , one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008) (Proof shortened by Mario Carneiro, 13-May-2014)

Ref Expression
Hypotheses eff1olem.1 ⊢ 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) )
eff1olem.2 ⊢ 𝑆 = ( ◡ ℑ “ 𝐷 )
eff1olem.3 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
eff1olem.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )
eff1olem.5 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐷 ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
Assertion eff1olem ( 𝜑 → ( exp ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ℂ ∖ { 0 } ) )

Proof

Step Hyp Ref Expression
1 eff1olem.1 ⊢ 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) )
2 eff1olem.2 ⊢ 𝑆 = ( ◡ ℑ “ 𝐷 )
3 eff1olem.3 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
4 eff1olem.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )
5 eff1olem.5 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐷 ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
6 cnvimass ⊢ ( ◡ ℑ “ 𝐷 ) ⊆ dom ℑ
7 imf ⊢ ℑ : ℂ ⟶ ℝ
8 7 fdmi ⊢ dom ℑ = ℂ
9 8 eqcomi ⊢ ℂ = dom ℑ
10 6 2 9 3sstr4i ⊢ 𝑆 ⊆ ℂ
11 eff2 ⊢ exp : ℂ ⟶ ( ℂ ∖ { 0 } )
12 11 a1i ⊢ ( 𝑆 ⊆ ℂ → exp : ℂ ⟶ ( ℂ ∖ { 0 } ) )
13 12 feqmptd ⊢ ( 𝑆 ⊆ ℂ → exp = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) )
14 13 reseq1d ⊢ ( 𝑆 ⊆ ℂ → ( exp ↾ 𝑆 ) = ( ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ↾ 𝑆 ) )
15 resmpt ⊢ ( 𝑆 ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ↾ 𝑆 ) = ( 𝑦 ∈ 𝑆 ↦ ( exp ‘ 𝑦 ) ) )
16 14 15 eqtrd ⊢ ( 𝑆 ⊆ ℂ → ( exp ↾ 𝑆 ) = ( 𝑦 ∈ 𝑆 ↦ ( exp ‘ 𝑦 ) ) )
17 10 16 ax-mp ⊢ ( exp ↾ 𝑆 ) = ( 𝑦 ∈ 𝑆 ↦ ( exp ‘ 𝑦 ) )
18 10 sseli ⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ )
19 11 ffvelcdmi ⊢ ( 𝑦 ∈ ℂ → ( exp ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
20 18 19 syl ⊢ ( 𝑦 ∈ 𝑆 → ( exp ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( exp ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
22 eldifsn ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
23 22 bilani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
24 23 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
25 23 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ≠ 0 )
26 24 25 absrpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ 𝑥 ) ∈ ℝ+ )
27 reeff1o ⊢ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+
28 f1ocnv ⊢ ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ → ◡ ( exp ↾ ℝ ) : ℝ+ –1-1-onto→ ℝ )
29 f1of ⊢ ( ◡ ( exp ↾ ℝ ) : ℝ+ –1-1-onto→ ℝ → ◡ ( exp ↾ ℝ ) : ℝ+ ⟶ ℝ )
30 27 28 29 mp2b ⊢ ◡ ( exp ↾ ℝ ) : ℝ+ ⟶ ℝ
31 30 ffvelcdmi ⊢ ( ( abs ‘ 𝑥 ) ∈ ℝ+ → ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ∈ ℝ )
32 26 31 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ∈ ℝ )
33 32 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ∈ ℂ )
34 ax-icn ⊢ i ∈ ℂ
35 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝐷 ⊆ ℝ )
36 eqid ⊢ ( ◡ abs “ { 1 } ) = ( ◡ abs “ { 1 } )
37 eqid ⊢ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) = ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) )
38 1 36 3 4 5 37 efif1olem4 ⊢ ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ ( ◡ abs “ { 1 } ) )
39 f1ocnv ⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( ◡ abs “ { 1 } ) → ◡ 𝐹 : ( ◡ abs “ { 1 } ) –1-1-onto→ 𝐷 )
40 f1of ⊢ ( ◡ 𝐹 : ( ◡ abs “ { 1 } ) –1-1-onto→ 𝐷 → ◡ 𝐹 : ( ◡ abs “ { 1 } ) ⟶ 𝐷 )
41 38 39 40 3syl ⊢ ( 𝜑 → ◡ 𝐹 : ( ◡ abs “ { 1 } ) ⟶ 𝐷 )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ◡ 𝐹 : ( ◡ abs “ { 1 } ) ⟶ 𝐷 )
43 24 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
44 43 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ 𝑥 ) ∈ ℂ )
45 24 25 absne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ 𝑥 ) ≠ 0 )
46 24 44 45 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 / ( abs ‘ 𝑥 ) ) ∈ ℂ )
47 24 44 45 absdivd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) = ( ( abs ‘ 𝑥 ) / ( abs ‘ ( abs ‘ 𝑥 ) ) ) )
48 absidm ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ ( abs ‘ 𝑥 ) ) = ( abs ‘ 𝑥 ) )
49 24 48 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ ( abs ‘ 𝑥 ) ) = ( abs ‘ 𝑥 ) )
50 49 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( abs ‘ 𝑥 ) / ( abs ‘ ( abs ‘ 𝑥 ) ) ) = ( ( abs ‘ 𝑥 ) / ( abs ‘ 𝑥 ) ) )
51 44 45 dividd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( abs ‘ 𝑥 ) / ( abs ‘ 𝑥 ) ) = 1 )
52 47 50 51 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) = 1 )
53 absf ⊢ abs : ℂ ⟶ ℝ
54 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
55 fniniseg ⊢ ( abs Fn ℂ → ( ( 𝑥 / ( abs ‘ 𝑥 ) ) ∈ ( ◡ abs “ { 1 } ) ↔ ( ( 𝑥 / ( abs ‘ 𝑥 ) ) ∈ ℂ ∧ ( abs ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) = 1 ) ) )
56 53 54 55 mp2b ⊢ ( ( 𝑥 / ( abs ‘ 𝑥 ) ) ∈ ( ◡ abs “ { 1 } ) ↔ ( ( 𝑥 / ( abs ‘ 𝑥 ) ) ∈ ℂ ∧ ( abs ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) = 1 ) )
57 46 52 56 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 / ( abs ‘ 𝑥 ) ) ∈ ( ◡ abs “ { 1 } ) )
58 42 57 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ∈ 𝐷 )
59 35 58 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ∈ ℝ )
60 59 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ∈ ℂ )
61 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ∈ ℂ ) → ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ∈ ℂ )
62 34 60 61 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ∈ ℂ )
63 33 62 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ∈ ℂ )
64 32 59 crimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ℑ ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) = ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) )
65 64 58 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ℑ ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) ∈ 𝐷 )
66 ffn ⊢ ( ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ )
67 elpreima ⊢ ( ℑ Fn ℂ → ( ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ∈ ( ◡ ℑ “ 𝐷 ) ↔ ( ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ∈ ℂ ∧ ( ℑ ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) ∈ 𝐷 ) ) )
68 7 66 67 mp2b ⊢ ( ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ∈ ( ◡ ℑ “ 𝐷 ) ↔ ( ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ∈ ℂ ∧ ( ℑ ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) ∈ 𝐷 ) )
69 63 65 68 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ∈ ( ◡ ℑ “ 𝐷 ) )
70 69 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ∈ 𝑆 )
71 efadd ⊢ ( ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ∈ ℂ ∧ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ∈ ℂ ) → ( exp ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) = ( ( exp ‘ ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ) · ( exp ‘ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) )
72 33 62 71 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) = ( ( exp ‘ ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ) · ( exp ‘ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) )
73 32 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ) = ( exp ‘ ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ) )
74 f1ocnvfv2 ⊢ ( ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ∧ ( abs ‘ 𝑥 ) ∈ ℝ+ ) → ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ) = ( abs ‘ 𝑥 ) )
75 27 26 74 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ) = ( abs ‘ 𝑥 ) )
76 73 75 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ) = ( abs ‘ 𝑥 ) )
77 oveq2 ⊢ ( 𝑧 = ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) → ( i · 𝑧 ) = ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) )
78 77 fveq2d ⊢ ( 𝑧 = ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) → ( exp ‘ ( i · 𝑧 ) ) = ( exp ‘ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) )
79 oveq2 ⊢ ( 𝑤 = 𝑧 → ( i · 𝑤 ) = ( i · 𝑧 ) )
80 79 fveq2d ⊢ ( 𝑤 = 𝑧 → ( exp ‘ ( i · 𝑤 ) ) = ( exp ‘ ( i · 𝑧 ) ) )
81 80 cbvmptv ⊢ ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) ) = ( 𝑧 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑧 ) ) )
82 1 81 eqtri ⊢ 𝐹 = ( 𝑧 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑧 ) ) )
83 fvex ⊢ ( exp ‘ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ∈ V
84 78 82 83 fvmpt ⊢ ( ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ∈ 𝐷 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) = ( exp ‘ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) )
85 58 84 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) = ( exp ‘ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) )
86 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝐹 : 𝐷 –1-1-onto→ ( ◡ abs “ { 1 } ) )
87 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐷 –1-1-onto→ ( ◡ abs “ { 1 } ) ∧ ( 𝑥 / ( abs ‘ 𝑥 ) ) ∈ ( ◡ abs “ { 1 } ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) = ( 𝑥 / ( abs ‘ 𝑥 ) ) )
88 86 57 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) = ( 𝑥 / ( abs ‘ 𝑥 ) ) )
89 85 88 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) = ( 𝑥 / ( abs ‘ 𝑥 ) ) )
90 76 89 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( exp ‘ ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) ) · ( exp ‘ ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) = ( ( abs ‘ 𝑥 ) · ( 𝑥 / ( abs ‘ 𝑥 ) ) ) )
91 24 44 45 divcan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( abs ‘ 𝑥 ) · ( 𝑥 / ( abs ‘ 𝑥 ) ) ) = 𝑥 )
92 72 90 91 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 = ( exp ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) )
93 92 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ) → 𝑥 = ( exp ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) )
94 fveq2 ⊢ ( 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) → ( exp ‘ 𝑦 ) = ( exp ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) )
95 94 eqeq2d ⊢ ( 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) → ( 𝑥 = ( exp ‘ 𝑦 ) ↔ 𝑥 = ( exp ‘ ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) ) )
96 93 95 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ) → ( 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) → 𝑥 = ( exp ‘ 𝑦 ) ) )
97 18 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ℂ )
98 97 replimd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 = ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) )
99 absef ⊢ ( 𝑦 ∈ ℂ → ( abs ‘ ( exp ‘ 𝑦 ) ) = ( exp ‘ ( ℜ ‘ 𝑦 ) ) )
100 97 99 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( exp ‘ 𝑦 ) ) = ( exp ‘ ( ℜ ‘ 𝑦 ) ) )
101 97 recld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ℜ ‘ 𝑦 ) ∈ ℝ )
102 101 fvresd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( exp ↾ ℝ ) ‘ ( ℜ ‘ 𝑦 ) ) = ( exp ‘ ( ℜ ‘ 𝑦 ) ) )
103 100 102 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( exp ‘ 𝑦 ) ) = ( ( exp ↾ ℝ ) ‘ ( ℜ ‘ 𝑦 ) ) )
104 103 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ ( exp ‘ 𝑦 ) ) ) = ( ◡ ( exp ↾ ℝ ) ‘ ( ( exp ↾ ℝ ) ‘ ( ℜ ‘ 𝑦 ) ) ) )
105 f1ocnvfv1 ⊢ ( ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ∧ ( ℜ ‘ 𝑦 ) ∈ ℝ ) → ( ◡ ( exp ↾ ℝ ) ‘ ( ( exp ↾ ℝ ) ‘ ( ℜ ‘ 𝑦 ) ) ) = ( ℜ ‘ 𝑦 ) )
106 27 101 105 sylancr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ◡ ( exp ↾ ℝ ) ‘ ( ( exp ↾ ℝ ) ‘ ( ℜ ‘ 𝑦 ) ) ) = ( ℜ ‘ 𝑦 ) )
107 104 106 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ ( exp ‘ 𝑦 ) ) ) = ( ℜ ‘ 𝑦 ) )
108 97 imcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ℑ ‘ 𝑦 ) ∈ ℝ )
109 108 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ℑ ‘ 𝑦 ) ∈ ℂ )
110 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝑦 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝑦 ) ) ∈ ℂ )
111 34 109 110 sylancr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( i · ( ℑ ‘ 𝑦 ) ) ∈ ℂ )
112 efcl ⊢ ( ( i · ( ℑ ‘ 𝑦 ) ) ∈ ℂ → ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) ∈ ℂ )
113 111 112 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) ∈ ℂ )
114 101 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ℜ ‘ 𝑦 ) ∈ ℂ )
115 efcl ⊢ ( ( ℜ ‘ 𝑦 ) ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝑦 ) ) ∈ ℂ )
116 114 115 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( exp ‘ ( ℜ ‘ 𝑦 ) ) ∈ ℂ )
117 efne0 ⊢ ( ( ℜ ‘ 𝑦 ) ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝑦 ) ) ≠ 0 )
118 114 117 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( exp ‘ ( ℜ ‘ 𝑦 ) ) ≠ 0 )
119 113 116 118 divcan3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( ( exp ‘ ( ℜ ‘ 𝑦 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) ) / ( exp ‘ ( ℜ ‘ 𝑦 ) ) ) = ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) )
120 98 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( exp ‘ 𝑦 ) = ( exp ‘ ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) ) )
121 efadd ⊢ ( ( ( ℜ ‘ 𝑦 ) ∈ ℂ ∧ ( i · ( ℑ ‘ 𝑦 ) ) ∈ ℂ ) → ( exp ‘ ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) ) = ( ( exp ‘ ( ℜ ‘ 𝑦 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) ) )
122 114 111 121 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( exp ‘ ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) ) = ( ( exp ‘ ( ℜ ‘ 𝑦 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) ) )
123 120 122 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( exp ‘ 𝑦 ) = ( ( exp ‘ ( ℜ ‘ 𝑦 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) ) )
124 123 100 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) = ( ( ( exp ‘ ( ℜ ‘ 𝑦 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) ) / ( exp ‘ ( ℜ ‘ 𝑦 ) ) ) )
125 elpreima ⊢ ( ℑ Fn ℂ → ( 𝑦 ∈ ( ◡ ℑ “ 𝐷 ) ↔ ( 𝑦 ∈ ℂ ∧ ( ℑ ‘ 𝑦 ) ∈ 𝐷 ) ) )
126 7 66 125 mp2b ⊢ ( 𝑦 ∈ ( ◡ ℑ “ 𝐷 ) ↔ ( 𝑦 ∈ ℂ ∧ ( ℑ ‘ 𝑦 ) ∈ 𝐷 ) )
127 126 simprbi ⊢ ( 𝑦 ∈ ( ◡ ℑ “ 𝐷 ) → ( ℑ ‘ 𝑦 ) ∈ 𝐷 )
128 127 2 eleq2s ⊢ ( 𝑦 ∈ 𝑆 → ( ℑ ‘ 𝑦 ) ∈ 𝐷 )
129 128 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ℑ ‘ 𝑦 ) ∈ 𝐷 )
130 oveq2 ⊢ ( 𝑤 = ( ℑ ‘ 𝑦 ) → ( i · 𝑤 ) = ( i · ( ℑ ‘ 𝑦 ) ) )
131 130 fveq2d ⊢ ( 𝑤 = ( ℑ ‘ 𝑦 ) → ( exp ‘ ( i · 𝑤 ) ) = ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) )
132 fvex ⊢ ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) ∈ V
133 131 1 132 fvmpt ⊢ ( ( ℑ ‘ 𝑦 ) ∈ 𝐷 → ( 𝐹 ‘ ( ℑ ‘ 𝑦 ) ) = ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) )
134 129 133 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ ( ℑ ‘ 𝑦 ) ) = ( exp ‘ ( i · ( ℑ ‘ 𝑦 ) ) ) )
135 119 124 134 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) = ( 𝐹 ‘ ( ℑ ‘ 𝑦 ) ) )
136 135 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) = ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( ℑ ‘ 𝑦 ) ) ) )
137 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝐷 –1-1-onto→ ( ◡ abs “ { 1 } ) ∧ ( ℑ ‘ 𝑦 ) ∈ 𝐷 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( ℑ ‘ 𝑦 ) ) ) = ( ℑ ‘ 𝑦 ) )
138 38 128 137 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( ℑ ‘ 𝑦 ) ) ) = ( ℑ ‘ 𝑦 ) )
139 136 138 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) = ( ℑ ‘ 𝑦 ) )
140 139 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( i · ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) ) = ( i · ( ℑ ‘ 𝑦 ) ) )
141 107 140 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ ( exp ‘ 𝑦 ) ) ) + ( i · ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) ) ) = ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) )
142 98 141 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ ( exp ‘ 𝑦 ) ) ) + ( i · ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) ) ) )
143 fveq2 ⊢ ( 𝑥 = ( exp ‘ 𝑦 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( exp ‘ 𝑦 ) ) )
144 143 fveq2d ⊢ ( 𝑥 = ( exp ‘ 𝑦 ) → ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) = ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ ( exp ‘ 𝑦 ) ) ) )
145 id ⊢ ( 𝑥 = ( exp ‘ 𝑦 ) → 𝑥 = ( exp ‘ 𝑦 ) )
146 145 143 oveq12d ⊢ ( 𝑥 = ( exp ‘ 𝑦 ) → ( 𝑥 / ( abs ‘ 𝑥 ) ) = ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) )
147 146 fveq2d ⊢ ( 𝑥 = ( exp ‘ 𝑦 ) → ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) = ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) )
148 147 oveq2d ⊢ ( 𝑥 = ( exp ‘ 𝑦 ) → ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) = ( i · ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) ) )
149 144 148 oveq12d ⊢ ( 𝑥 = ( exp ‘ 𝑦 ) → ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ ( exp ‘ 𝑦 ) ) ) + ( i · ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) ) ) )
150 149 eqeq2d ⊢ ( 𝑥 = ( exp ‘ 𝑦 ) → ( 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ↔ 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ ( exp ‘ 𝑦 ) ) ) + ( i · ( ◡ 𝐹 ‘ ( ( exp ‘ 𝑦 ) / ( abs ‘ ( exp ‘ 𝑦 ) ) ) ) ) ) ) )
151 142 150 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 = ( exp ‘ 𝑦 ) → 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) )
152 151 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ) → ( 𝑥 = ( exp ‘ 𝑦 ) → 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ) )
153 96 152 impbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ) → ( 𝑦 = ( ( ◡ ( exp ↾ ℝ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ◡ 𝐹 ‘ ( 𝑥 / ( abs ‘ 𝑥 ) ) ) ) ) ↔ 𝑥 = ( exp ‘ 𝑦 ) ) )
154 17 21 70 153 f1o2d ⊢ ( 𝜑 → ( exp ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ℂ ∖ { 0 } ) )