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 } ) )

Metamath Proof Explorer

Theorem eff1olem

Proof