dvloglem

		Ref	Expression
	Hypothesis	logcn.d	$⊢ D = ℂ ∖ (−∞, 0]$
	Assertion	dvloglem	$⊢ log [D] \in TopOpen (ℂ_{fld})$

Proof

Step	Hyp	Ref	Expression
1		logcn.d	$⊢ D = ℂ ∖ (−∞, 0]$
2		logf1o	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log$
3		f1ofun	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log \to Fun log$
4	2 3	ax-mp	$⊢ Fun log$
5	1	logdmss	$⊢ D \subseteq ℂ ∖ \{0\}$
6		f1odm	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log \to dom log = ℂ ∖ \{0\}$
7	2 6	ax-mp	$⊢ dom log = ℂ ∖ \{0\}$
8	5 7	sseqtrri	$⊢ D \subseteq dom log$
9		funimass4	$⊢ (Fun log \land D \subseteq dom log) \to (log [D] \subseteq ℑ^{-1} [(- π, π)] \leftrightarrow \forall x \in D \log x \in ℑ^{-1} [(- π, π)])$
10	4 8 9	mp2an	$⊢ log [D] \subseteq ℑ^{-1} [(- π, π)] \leftrightarrow \forall x \in D \log x \in ℑ^{-1} [(- π, π)]$
11	1	ellogdm	$⊢ x \in D \leftrightarrow (x \in ℂ \land (x \in ℝ \to x \in ℝ^{+}))$
12	11	simplbi	$⊢ x \in D \to x \in ℂ$
13	1	logdmn0	$⊢ x \in D \to x \neq 0$
14	12 13	logcld	$⊢ x \in D \to \log x \in ℂ$
15	14	imcld	$⊢ x \in D \to ℑ (\log x) \in ℝ$
16	12 13	logimcld	$⊢ x \in D \to (- π < ℑ (\log x) \land ℑ (\log x) \leq π)$
17	16	simpld	$⊢ x \in D \to - π < ℑ (\log x)$
18		pire	$⊢ π \in ℝ$
19	18	a1i	$⊢ x \in D \to π \in ℝ$
20	16	simprd	$⊢ x \in D \to ℑ (\log x) \leq π$
21	1	logdmnrp	$⊢ x \in D \to \neg - x \in ℝ^{+}$
22		lognegb	$⊢ (x \in ℂ \land x \neq 0) \to (- x \in ℝ^{+} \leftrightarrow ℑ (\log x) = π)$
23	12 13 22	syl2anc	$⊢ x \in D \to (- x \in ℝ^{+} \leftrightarrow ℑ (\log x) = π)$
24	23	necon3bbid	$⊢ x \in D \to (\neg - x \in ℝ^{+} \leftrightarrow ℑ (\log x) \neq π)$
25	21 24	mpbid	$⊢ x \in D \to ℑ (\log x) \neq π$
26	25	necomd	$⊢ x \in D \to π \neq ℑ (\log x)$
27	15 19 20 26	leneltd	$⊢ x \in D \to ℑ (\log x) < π$
28	18	renegcli	$⊢ - π \in ℝ$
29	28	rexri	$⊢ - π \in ℝ^{*}$
30	18	rexri	$⊢ π \in ℝ^{*}$
31		elioo2	$⊢ (- π \in ℝ^{} \land π \in ℝ^{}) \to (ℑ (\log x) \in (- π, π) \leftrightarrow (ℑ (\log x) \in ℝ \land - π < ℑ (\log x) \land ℑ (\log x) < π))$
32	29 30 31	mp2an	$⊢ ℑ (\log x) \in (- π, π) \leftrightarrow (ℑ (\log x) \in ℝ \land - π < ℑ (\log x) \land ℑ (\log x) < π)$
33	15 17 27 32	syl3anbrc	$⊢ x \in D \to ℑ (\log x) \in (- π, π)$
34		imf	$⊢ ℑ : ℂ ⟶ ℝ$
35		ffn	$⊢ ℑ : ℂ ⟶ ℝ \to ℑ Fn ℂ$
36		elpreima	$⊢ ℑ Fn ℂ \to (\log x \in ℑ^{-1} [(- π, π)] \leftrightarrow (\log x \in ℂ \land ℑ (\log x) \in (- π, π)))$
37	34 35 36	mp2b	$⊢ \log x \in ℑ^{-1} [(- π, π)] \leftrightarrow (\log x \in ℂ \land ℑ (\log x) \in (- π, π))$
38	14 33 37	sylanbrc	$⊢ x \in D \to \log x \in ℑ^{-1} [(- π, π)]$
39	10 38	mprgbir	$⊢ log [D] \subseteq ℑ^{-1} [(- π, π)]$
40		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
41		df-ioc	$⊢ (.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z \leq y)\})$
42		idd	$⊢ (- π \in ℝ^{} \land w \in ℝ^{}) \to (- π < w \to - π < w)$
43		xrltle	$⊢ (w \in ℝ^{} \land π \in ℝ^{}) \to (w < π \to w \leq π)$
44	40 41 42 43	ixxssixx	$⊢ (- π, π) \subseteq (- π, π]$
45		imass2	$⊢ (- π, π) \subseteq (- π, π] \to ℑ^{-1} [(- π, π)] \subseteq ℑ^{-1} [(- π, π]]$
46	44 45	ax-mp	$⊢ ℑ^{-1} [(- π, π)] \subseteq ℑ^{-1} [(- π, π]]$
47		logrn	$⊢ ran log = ℑ^{-1} [(- π, π]]$
48	46 47	sseqtrri	$⊢ ℑ^{-1} [(- π, π)] \subseteq ran log$
49	48	sseli	$⊢ x \in ℑ^{-1} [(- π, π)] \to x \in ran log$
50		logef	$⊢ x \in ran log \to \log e^{x} = x$
51	49 50	syl	$⊢ x \in ℑ^{-1} [(- π, π)] \to \log e^{x} = x$
52		elpreima	$⊢ ℑ Fn ℂ \to (x \in ℑ^{-1} [(- π, π)] \leftrightarrow (x \in ℂ \land ℑ (x) \in (- π, π)))$
53	34 35 52	mp2b	$⊢ x \in ℑ^{-1} [(- π, π)] \leftrightarrow (x \in ℂ \land ℑ (x) \in (- π, π))$
54		efcl	$⊢ x \in ℂ \to e^{x} \in ℂ$
55	54	adantr	$⊢ (x \in ℂ \land ℑ (x) \in (- π, π)) \to e^{x} \in ℂ$
56	53 55	sylbi	$⊢ x \in ℑ^{-1} [(- π, π)] \to e^{x} \in ℂ$
57	53	simplbi	$⊢ x \in ℑ^{-1} [(- π, π)] \to x \in ℂ$
58	57	imcld	$⊢ x \in ℑ^{-1} [(- π, π)] \to ℑ (x) \in ℝ$
59		eliooord	$⊢ ℑ (x) \in (- π, π) \to (- π < ℑ (x) \land ℑ (x) < π)$
60	53 59	simplbiim	$⊢ x \in ℑ^{-1} [(- π, π)] \to (- π < ℑ (x) \land ℑ (x) < π)$
61	60	simprd	$⊢ x \in ℑ^{-1} [(- π, π)] \to ℑ (x) < π$
62	58 61	ltned	$⊢ x \in ℑ^{-1} [(- π, π)] \to ℑ (x) \neq π$
63	51	adantr	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to \log e^{x} = x$
64	63	fveq2d	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to ℑ (\log e^{x}) = ℑ (x)$
65		simpr	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to e^{x} \in (−∞, 0]$
66		mnfxr	$⊢ −∞ \in ℝ^{*}$
67		0re	$⊢ 0 \in ℝ$
68		elioc2	$⊢ (−∞ \in ℝ^{*} \land 0 \in ℝ) \to (e^{x} \in (−∞, 0] \leftrightarrow (e^{x} \in ℝ \land −∞ < e^{x} \land e^{x} \leq 0))$
69	66 67 68	mp2an	$⊢ e^{x} \in (−∞, 0] \leftrightarrow (e^{x} \in ℝ \land −∞ < e^{x} \land e^{x} \leq 0)$
70	65 69	sylib	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to (e^{x} \in ℝ \land −∞ < e^{x} \land e^{x} \leq 0)$
71	70	simp1d	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to e^{x} \in ℝ$
72		0red	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to 0 \in ℝ$
73	70	simp3d	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to e^{x} \leq 0$
74		efne0	$⊢ x \in ℂ \to e^{x} \neq 0$
75	57 74	syl	$⊢ x \in ℑ^{-1} [(- π, π)] \to e^{x} \neq 0$
76	75	adantr	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to e^{x} \neq 0$
77	76	necomd	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to 0 \neq e^{x}$
78	71 72 73 77	leneltd	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to e^{x} < 0$
79	71 78	negelrpd	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to - e^{x} \in ℝ^{+}$
80		lognegb	$⊢ (e^{x} \in ℂ \land e^{x} \neq 0) \to (- e^{x} \in ℝ^{+} \leftrightarrow ℑ (\log e^{x}) = π)$
81	56 75 80	syl2anc	$⊢ x \in ℑ^{-1} [(- π, π)] \to (- e^{x} \in ℝ^{+} \leftrightarrow ℑ (\log e^{x}) = π)$
82	81	adantr	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to (- e^{x} \in ℝ^{+} \leftrightarrow ℑ (\log e^{x}) = π)$
83	79 82	mpbid	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to ℑ (\log e^{x}) = π$
84	64 83	eqtr3d	$⊢ (x \in ℑ^{-1} [(- π, π)] \land e^{x} \in (−∞, 0]) \to ℑ (x) = π$
85	84	ex	$⊢ x \in ℑ^{-1} [(- π, π)] \to (e^{x} \in (−∞, 0] \to ℑ (x) = π)$
86	85	necon3ad	$⊢ x \in ℑ^{-1} [(- π, π)] \to (ℑ (x) \neq π \to \neg e^{x} \in (−∞, 0])$
87	62 86	mpd	$⊢ x \in ℑ^{-1} [(- π, π)] \to \neg e^{x} \in (−∞, 0]$
88	56 87	eldifd	$⊢ x \in ℑ^{-1} [(- π, π)] \to e^{x} \in (ℂ ∖ (−∞, 0])$
89	88 1	eleqtrrdi	$⊢ x \in ℑ^{-1} [(- π, π)] \to e^{x} \in D$
90		funfvima2	$⊢ (Fun log \land D \subseteq dom log) \to (e^{x} \in D \to \log e^{x} \in log [D])$
91	4 8 90	mp2an	$⊢ e^{x} \in D \to \log e^{x} \in log [D]$
92	89 91	syl	$⊢ x \in ℑ^{-1} [(- π, π)] \to \log e^{x} \in log [D]$
93	51 92	eqeltrrd	$⊢ x \in ℑ^{-1} [(- π, π)] \to x \in log [D]$
94	93	ssriv	$⊢ ℑ^{-1} [(- π, π)] \subseteq log [D]$
95	39 94	eqssi	$⊢ log [D] = ℑ^{-1} [(- π, π)]$
96		imcncf	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ$
97		ssid	$⊢ ℂ \subseteq ℂ$
98		ax-resscn	$⊢ ℝ \subseteq ℂ$
99		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
100	99	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
101	100	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
102		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
103	99 101 102	cncfcn	$⊢ (ℂ \subseteq ℂ \land ℝ \subseteq ℂ) \to ℂ \underset{cn}{⟶} ℝ = TopOpen (ℂ_{fld}) Cn topGen (ran (.))$
104	97 98 103	mp2an	$⊢ ℂ \underset{cn}{⟶} ℝ = TopOpen (ℂ_{fld}) Cn topGen (ran (.))$
105	96 104	eleqtri	$⊢ ℑ \in (TopOpen (ℂ_{fld}) Cn topGen (ran (.)))$
106		iooretop	$⊢ (- π, π) \in topGen (ran (.))$
107		cnima	$⊢ (ℑ \in (TopOpen (ℂ_{fld}) Cn topGen (ran (.))) \land (- π, π) \in topGen (ran (.))) \to ℑ^{-1} [(- π, π)] \in TopOpen (ℂ_{fld})$
108	105 106 107	mp2an	$⊢ ℑ^{-1} [(- π, π)] \in TopOpen (ℂ_{fld})$
109	95 108	eqeltri	$⊢ log [D] \in TopOpen (ℂ_{fld})$

Metamath Proof Explorer

Theorem dvloglem

Proof