Theorem logf1o2

Description: The logarithm maps its continuous domain bijectively onto the set of numbers with imaginary part -upi < Im ( z ) < pi . The negative reals are mapped to the numbers with imaginary part equal to _pi . (Contributed by Mario Carneiro, 2-May-2015)

	Ref	Expression
Hypothesis	logcn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion	logf1o2	⊢ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( ◡ ℑ “ ( - π (,) π ) )

Proof

Step	Hyp	Ref	Expression
1		logcn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2		logf1o	⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
3		f1of1	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) –1-1→ ran log )
4	2 3	ax-mp	⊢ log : ( ℂ ∖ { 0 } ) –1-1→ ran log
5	1	logdmss	⊢ 𝐷 ⊆ ( ℂ ∖ { 0 } )
6		f1ores	⊢ ( ( log : ( ℂ ∖ { 0 } ) –1-1→ ran log ∧ 𝐷 ⊆ ( ℂ ∖ { 0 } ) ) → ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) )
7	4 5 6	mp2an	⊢ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 )
8		f1ofun	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → Fun log )
9	2 8	ax-mp	⊢ Fun log
10		f1of	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
11	2 10	ax-mp	⊢ log : ( ℂ ∖ { 0 } ) ⟶ ran log
12	11	fdmi	⊢ dom log = ( ℂ ∖ { 0 } )
13	5 12	sseqtrri	⊢ 𝐷 ⊆ dom log
14		funimass4	⊢ ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥 ∈ 𝐷 ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ) )
15	9 13 14	mp2an	⊢ ( ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥 ∈ 𝐷 ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) )
16	1	ellogdm	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
17	16	simplbi	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
18	1	logdmn0	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
19	17 18	logcld	⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ℂ )
20	19	imcld	⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ )
21	17 18	logimcld	⊢ ( 𝑥 ∈ 𝐷 → ( - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π ) )
22	21	simpld	⊢ ( 𝑥 ∈ 𝐷 → - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) )
23		pire	⊢ π ∈ ℝ
24	23	a1i	⊢ ( 𝑥 ∈ 𝐷 → π ∈ ℝ )
25	21	simprd	⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π )
26	1	logdmnrp	⊢ ( 𝑥 ∈ 𝐷 → ¬ - 𝑥 ∈ ℝ+ )
27		lognegb	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) )
28	17 18 27	syl2anc	⊢ ( 𝑥 ∈ 𝐷 → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) )
29	28	necon3bbid	⊢ ( 𝑥 ∈ 𝐷 → ( ¬ - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π ) )
30	26 29	mpbid	⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π )
31	30	necomd	⊢ ( 𝑥 ∈ 𝐷 → π ≠ ( ℑ ‘ ( log ‘ 𝑥 ) ) )
32	20 24 25 31	leneltd	⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) < π )
33	23	renegcli	⊢ - π ∈ ℝ
34	33	rexri	⊢ - π ∈ ℝ*
35	23	rexri	⊢ π ∈ ℝ*
36		elioo2	⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) ) )
37	34 35 36	mp2an	⊢ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) )
38	20 22 32 37	syl3anbrc	⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) )
39		imf	⊢ ℑ : ℂ ⟶ ℝ
40		ffn	⊢ ( ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ )
41		elpreima	⊢ ( ℑ Fn ℂ → ( ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) ) )
42	39 40 41	mp2b	⊢ ( ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) )
43	19 38 42	sylanbrc	⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) )
44	15 43	mprgbir	⊢ ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) )
45		elpreima	⊢ ( ℑ Fn ℂ → ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ) )
46	39 40 45	mp2b	⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) )
47		simpl	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ℂ )
48		eliooord	⊢ ( ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) )
49	48	adantl	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) )
50	49	simpld	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → - π < ( ℑ ‘ 𝑥 ) )
51	49	simprd	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) < π )
52		imcl	⊢ ( 𝑥 ∈ ℂ → ( ℑ ‘ 𝑥 ) ∈ ℝ )
53	52	adantr	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ∈ ℝ )
54		ltle	⊢ ( ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) < π → ( ℑ ‘ 𝑥 ) ≤ π ) )
55	53 23 54	sylancl	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ( ℑ ‘ 𝑥 ) < π → ( ℑ ‘ 𝑥 ) ≤ π ) )
56	51 55	mpd	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ≤ π )
57		ellogrn	⊢ ( 𝑥 ∈ ran log ↔ ( 𝑥 ∈ ℂ ∧ - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) ≤ π ) )
58	47 50 56 57	syl3anbrc	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ran log )
59		logef	⊢ ( 𝑥 ∈ ran log → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 )
60	58 59	syl	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 )
61		efcl	⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
62	61	adantr	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ℂ )
63	53	adantr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℝ )
64	63	recnd	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℂ )
65		picn	⊢ π ∈ ℂ
66	65	a1i	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ∈ ℂ )
67		pipos	⊢ 0 < π
68	23 67	gt0ne0ii	⊢ π ≠ 0
69	68	a1i	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ≠ 0 )
70	51	adantr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) < π )
71	65	mulridi	⊢ ( π · 1 ) = π
72	70 71	breqtrrdi	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) < ( π · 1 ) )
73		1re	⊢ 1 ∈ ℝ
74	73	a1i	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 1 ∈ ℝ )
75	23	a1i	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ∈ ℝ )
76	67	a1i	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 0 < π )
77		ltdivmul	⊢ ( ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( π ∈ ℝ ∧ 0 < π ) ) → ( ( ( ℑ ‘ 𝑥 ) / π ) < 1 ↔ ( ℑ ‘ 𝑥 ) < ( π · 1 ) ) )
78	63 74 75 76 77	syl112anc	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) < 1 ↔ ( ℑ ‘ 𝑥 ) < ( π · 1 ) ) )
79	72 78	mpbird	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) < 1 )
80		1e0p1	⊢ 1 = ( 0 + 1 )
81	79 80	breqtrdi	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) )
82	63	recoscld	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( cos ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ )
83	63	resincld	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ )
84	82 83	crimd	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) = ( sin ‘ ( ℑ ‘ 𝑥 ) ) )
85		efeul	⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) = ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) )
86	85	ad2antrr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) = ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) )
87	86	oveq1d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) )
88	82	recnd	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( cos ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ )
89		ax-icn	⊢ i ∈ ℂ
90	83	recnd	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ )
91		mulcl	⊢ ( ( i ∈ ℂ ∧ ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ ) → ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ∈ ℂ )
92	89 90 91	sylancr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ∈ ℂ )
93	88 92	addcld	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ∈ ℂ )
94		recl	⊢ ( 𝑥 ∈ ℂ → ( ℜ ‘ 𝑥 ) ∈ ℝ )
95	94	ad2antrr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℜ ‘ 𝑥 ) ∈ ℝ )
96	95	recnd	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℜ ‘ 𝑥 ) ∈ ℂ )
97		efcl	⊢ ( ( ℜ ‘ 𝑥 ) ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℂ )
98	96 97	syl	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℂ )
99		efne0	⊢ ( ( ℜ ‘ 𝑥 ) ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ≠ 0 )
100	96 99	syl	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ≠ 0 )
101	93 98 100	divcan3d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) )
102	87 101	eqtrd	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) )
103		simpr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) ∈ ℝ )
104	95	reefcld	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℝ )
105	103 104 100	redivcld	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) ∈ ℝ )
106	102 105	eqeltrrd	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ∈ ℝ )
107	106	reim0d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) = 0 )
108	84 107	eqtr3d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 )
109		sineq0	⊢ ( ( ℑ ‘ 𝑥 ) ∈ ℂ → ( ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) )
110	64 109	syl	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) )
111	108 110	mpbid	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ )
112		0z	⊢ 0 ∈ ℤ
113		zleltp1	⊢ ( ( ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) ) )
114	111 112 113	sylancl	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) ) )
115	81 114	mpbird	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 )
116		df-neg	⊢ - 1 = ( 0 − 1 )
117	65	mulm1i	⊢ ( - 1 · π ) = - π
118	50	adantr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - π < ( ℑ ‘ 𝑥 ) )
119	117 118	eqbrtrid	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( - 1 · π ) < ( ℑ ‘ 𝑥 ) )
120	73	renegcli	⊢ - 1 ∈ ℝ
121	120	a1i	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - 1 ∈ ℝ )
122		ltmuldiv	⊢ ( ( - 1 ∈ ℝ ∧ ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ ( π ∈ ℝ ∧ 0 < π ) ) → ( ( - 1 · π ) < ( ℑ ‘ 𝑥 ) ↔ - 1 < ( ( ℑ ‘ 𝑥 ) / π ) ) )
123	121 63 75 76 122	syl112anc	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( - 1 · π ) < ( ℑ ‘ 𝑥 ) ↔ - 1 < ( ( ℑ ‘ 𝑥 ) / π ) ) )
124	119 123	mpbid	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - 1 < ( ( ℑ ‘ 𝑥 ) / π ) )
125	116 124	eqbrtrrid	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) )
126		zlem1lt	⊢ ( ( 0 ∈ ℤ ∧ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) → ( 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ↔ ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) ) )
127	112 111 126	sylancr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ↔ ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) ) )
128	125 127	mpbird	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) )
129	63 75 69	redivcld	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℝ )
130		0re	⊢ 0 ∈ ℝ
131		letri3	⊢ ( ( ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) = 0 ↔ ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ∧ 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ) ) )
132	129 130 131	sylancl	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) = 0 ↔ ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ∧ 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ) ) )
133	115 128 132	mpbir2and	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) = 0 )
134	64 66 69 133	diveq0d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) = 0 )
135		reim0b	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) )
136	135	ad2antrr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) )
137	134 136	mpbird	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 𝑥 ∈ ℝ )
138	137	rpefcld	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) ∈ ℝ+ )
139	138	ex	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ( exp ‘ 𝑥 ) ∈ ℝ → ( exp ‘ 𝑥 ) ∈ ℝ+ ) )
140	1	ellogdm	⊢ ( ( exp ‘ 𝑥 ) ∈ 𝐷 ↔ ( ( exp ‘ 𝑥 ) ∈ ℂ ∧ ( ( exp ‘ 𝑥 ) ∈ ℝ → ( exp ‘ 𝑥 ) ∈ ℝ+ ) ) )
141	62 139 140	sylanbrc	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ 𝐷 )
142		funfvima2	⊢ ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) )
143	9 13 142	mp2an	⊢ ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) )
144	141 143	syl	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) )
145	60 144	eqeltrrd	⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) )
146	46 145	sylbi	⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) )
147	146	ssriv	⊢ ( ◡ ℑ “ ( - π (,) π ) ) ⊆ ( log “ 𝐷 )
148	44 147	eqssi	⊢ ( log “ 𝐷 ) = ( ◡ ℑ “ ( - π (,) π ) )
149		f1oeq3	⊢ ( ( log “ 𝐷 ) = ( ◡ ℑ “ ( - π (,) π ) ) → ( ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) ↔ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( ◡ ℑ “ ( - π (,) π ) ) ) )
150	148 149	ax-mp	⊢ ( ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) ↔ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( ◡ ℑ “ ( - π (,) π ) ) )
151	7 150	mpbi	⊢ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( ◡ ℑ “ ( - π (,) π ) )