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

Metamath Proof Explorer

Theorem eff1olem

Proof