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	$⊢ D = ℂ ∖ (−∞, 0]$
	Assertion	logf1o2	$⊢ ({log ↾}_{D}) : D \underset{1-1 onto}{⟶} ℑ^{-1} [(- π, π)]$

Proof

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

Metamath Proof Explorer

Theorem logf1o2

Proof