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