Theorem logcn

Description: The logarithm function is continuous away from the branch cut at negative reals. (Contributed by Mario Carneiro, 25-Feb-2015)

	Ref	Expression
Hypothesis	logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
Assertion	logcn	$$⊢\left({log\upharpoonright }_D\right):D\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2		logf1o	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log$$
3		f1of	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log\to log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
4	2 3	ax-mp	$$⊢log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
5	1	logdmss	$$⊢D\subseteq ℂ\setminus \left\{0\right\}$$
6		fssres	$$⊢\left(log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log\wedge D\subseteq ℂ\setminus \left\{0\right\}\right)\to \left({log\upharpoonright }_D\right):D⟶\mathrm{ran}log$$
7	4 5 6	mp2an	$$⊢\left({log\upharpoonright }_D\right):D⟶\mathrm{ran}log$$
8		ffn	$$⊢\left({log\upharpoonright }_D\right):D⟶\mathrm{ran}log\to \left({log\upharpoonright }_D\right)FnD$$
9	7 8	ax-mp	$$⊢\left({log\upharpoonright }_D\right)FnD$$
10		dffn5	$$⊢\left({log\upharpoonright }_D\right)FnD\leftrightarrow {log\upharpoonright }_D=\left(x\in D⟼\left({log\upharpoonright }_D\right)\left(x\right)\right)$$
11	9 10	mpbi	$$⊢{log\upharpoonright }_D=\left(x\in D⟼\left({log\upharpoonright }_D\right)\left(x\right)\right)$$
12		fvres	$$⊢x\in D\to \left({log\upharpoonright }_D\right)\left(x\right)=\log x$$
13	1	ellogdm	$$⊢x\in D\leftrightarrow \left(x\in ℂ\wedge \left(x\in ℝ\to x\in {ℝ}^{+}\right)\right)$$
14	13	simplbi	$$⊢x\in D\to x\in ℂ$$
15	1	logdmn0	$$⊢x\in D\to x\ne 0$$
16	14 15	logcld	$$⊢x\in D\to \log x\in ℂ$$
17	16	replimd	$$⊢x\in D\to \log x=\Re \left(\log x\right)+\mathrm{i}\Im \left(\log x\right)$$
18		relog	$$⊢\left(x\in ℂ\wedge x\ne 0\right)\to \Re \left(\log x\right)=\log \left|x\right|$$
19	14 15 18	syl2anc	$$⊢x\in D\to \Re \left(\log x\right)=\log \left|x\right|$$
20	14 15	absrpcld	$$⊢x\in D\to \left|x\right|\in {ℝ}^{+}$$
21	20	fvresd	$$⊢x\in D\to \left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)=\log \left|x\right|$$
22	19 21	eqtr4d	$$⊢x\in D\to \Re \left(\log x\right)=\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)$$
23	22	oveq1d	$$⊢x\in D\to \Re \left(\log x\right)+\mathrm{i}\Im \left(\log x\right)=\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)+\mathrm{i}\Im \left(\log x\right)$$
24	12 17 23	3eqtrd	$$⊢x\in D\to \left({log\upharpoonright }_D\right)\left(x\right)=\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)+\mathrm{i}\Im \left(\log x\right)$$
25	24	mpteq2ia	$$⊢\left(x\in D⟼\left({log\upharpoonright }_D\right)\left(x\right)\right)=\left(x\in D⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)+\mathrm{i}\Im \left(\log x\right)\right)$$
26	11 25	eqtri	$$⊢{log\upharpoonright }_D=\left(x\in D⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)+\mathrm{i}\Im \left(\log x\right)\right)$$
27		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
28	27	addcn	$$⊢+\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
29	28	a1i	$$⊢\top \to +\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
30	27	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
31	14	ssriv	$$⊢D\subseteq ℂ$$
32		resttopon	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge D\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\in \mathrm{TopOn}\left(D\right)$$
33	30 31 32	mp2an	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\in \mathrm{TopOn}\left(D\right)$$
34	33	a1i	$$⊢\top \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\in \mathrm{TopOn}\left(D\right)$$
35		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
36		fssres	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge D\subseteq ℂ\right)\to \left({\mathrm{abs}\upharpoonright }_D\right):D⟶ℝ$$
37	35 31 36	mp2an	$$⊢\left({\mathrm{abs}\upharpoonright }_D\right):D⟶ℝ$$
38	37	a1i	$$⊢\top \to \left({\mathrm{abs}\upharpoonright }_D\right):D⟶ℝ$$
39	38	feqmptd	$$⊢\top \to {\mathrm{abs}\upharpoonright }_D=\left(x\in D⟼\left({\mathrm{abs}\upharpoonright }_D\right)\left(x\right)\right)$$
40		fvres	$$⊢x\in D\to \left({\mathrm{abs}\upharpoonright }_D\right)\left(x\right)=\left|x\right|$$
41	40	mpteq2ia	$$⊢\left(x\in D⟼\left({\mathrm{abs}\upharpoonright }_D\right)\left(x\right)\right)=\left(x\in D⟼\left|x\right|\right)$$
42	39 41	syl6eq	$$⊢\top \to {\mathrm{abs}\upharpoonright }_D=\left(x\in D⟼\left|x\right|\right)$$
43		ffn	$$⊢\left({\mathrm{abs}\upharpoonright }_D\right):D⟶ℝ\to \left({\mathrm{abs}\upharpoonright }_D\right)FnD$$
44	37 43	ax-mp	$$⊢\left({\mathrm{abs}\upharpoonright }_D\right)FnD$$
45	40 20	eqeltrd	$$⊢x\in D\to \left({\mathrm{abs}\upharpoonright }_D\right)\left(x\right)\in {ℝ}^{+}$$
46	45	rgen	$$⊢\forall x\in D\left({\mathrm{abs}\upharpoonright }_D\right)\left(x\right)\in {ℝ}^{+}$$
47		ffnfv	$$⊢\left({\mathrm{abs}\upharpoonright }_D\right):D⟶{ℝ}^{+}\leftrightarrow \left(\left({\mathrm{abs}\upharpoonright }_D\right)FnD\wedge \forall x\in D\left({\mathrm{abs}\upharpoonright }_D\right)\left(x\right)\in {ℝ}^{+}\right)$$
48	44 46 47	mpbir2an	$$⊢\left({\mathrm{abs}\upharpoonright }_D\right):D⟶{ℝ}^{+}$$
49		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
50		ax-resscn	$$⊢ℝ\subseteq ℂ$$
51	49 50	sstri	$$⊢{ℝ}^{+}\subseteq ℂ$$
52		abscncf	$$⊢\mathrm{abs}:ℂ\underset{cn}{⟶}ℝ$$
53		rescncf	$$⊢D\subseteq ℂ\to \left(\mathrm{abs}:ℂ\underset{cn}{⟶}ℝ\to \left({\mathrm{abs}\upharpoonright }_D\right):D\underset{cn}{⟶}ℝ\right)$$
54	31 52 53	mp2	$$⊢\left({\mathrm{abs}\upharpoonright }_D\right):D\underset{cn}{⟶}ℝ$$
55		cncffvrn	$$⊢\left({ℝ}^{+}\subseteq ℂ\wedge \left({\mathrm{abs}\upharpoonright }_D\right):D\underset{cn}{⟶}ℝ\right)\to \left(\left({\mathrm{abs}\upharpoonright }_D\right):D\underset{cn}{⟶}{ℝ}^{+}\leftrightarrow \left({\mathrm{abs}\upharpoonright }_D\right):D⟶{ℝ}^{+}\right)$$
56	51 54 55	mp2an	$$⊢\left({\mathrm{abs}\upharpoonright }_D\right):D\underset{cn}{⟶}{ℝ}^{+}\leftrightarrow \left({\mathrm{abs}\upharpoonright }_D\right):D⟶{ℝ}^{+}$$
57	48 56	mpbir	$$⊢\left({\mathrm{abs}\upharpoonright }_D\right):D\underset{cn}{⟶}{ℝ}^{+}$$
58	42 57	syl6eqelr	$$⊢\top \to \left(x\in D⟼\left|x\right|\right):D\underset{cn}{⟶}{ℝ}^{+}$$
59		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D$$
60		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^{+}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^{+}$$
61	27 59 60	cncfcn	$$⊢\left(D\subseteq ℂ\wedge {ℝ}^{+}\subseteq ℂ\right)\to D\underset{cn}{⟶}{ℝ}^{+}=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^{+}\right)$$
62	31 51 61	mp2an	$$⊢D\underset{cn}{⟶}{ℝ}^{+}=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^{+}\right)$$
63	58 62	eleqtrdi	$$⊢\top \to \left(x\in D⟼\left|x\right|\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^{+}\right)\right)$$
64		ssid	$$⊢ℂ\subseteq ℂ$$
65		cncfss	$$⊢\left(ℝ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to {ℝ}^{+}\underset{cn}{⟶}ℝ\subseteq {ℝ}^{+}\underset{cn}{⟶}ℂ$$
66	50 64 65	mp2an	$$⊢{ℝ}^{+}\underset{cn}{⟶}ℝ\subseteq {ℝ}^{+}\underset{cn}{⟶}ℂ$$
67		relogcn	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ$$
68	66 67	sselii	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℂ$$
69	68	a1i	$$⊢\top \to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℂ$$
70	30	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
71	27 60 70	cncfcn	$$⊢\left({ℝ}^{+}\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to {ℝ}^{+}\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^{+}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
72	51 64 71	mp2an	$$⊢{ℝ}^{+}\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^{+}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
73	69 72	eleqtrdi	$$⊢\top \to {log\upharpoonright }_{{ℝ}^{+}}\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}{ℝ}^{+}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
74	34 63 73	cnmpt11f	$$⊢\top \to \left(x\in D⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
75	27 59 70	cncfcn	$$⊢\left(D\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to D\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
76	31 64 75	mp2an	$$⊢D\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
77	74 76	eleqtrrdi	$$⊢\top \to \left(x\in D⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)\right):D\underset{cn}{⟶}ℂ$$
78	16	imcld	$$⊢x\in D\to \Im \left(\log x\right)\in ℝ$$
79	78	recnd	$$⊢x\in D\to \Im \left(\log x\right)\in ℂ$$
80	79	adantl	$$⊢\left(\top \wedge x\in D\right)\to \Im \left(\log x\right)\in ℂ$$
81		eqidd	$$⊢\top \to \left(x\in D⟼\Im \left(\log x\right)\right)=\left(x\in D⟼\Im \left(\log x\right)\right)$$
82		eqidd	$$⊢\top \to \left(y\in ℂ⟼\mathrm{i}y\right)=\left(y\in ℂ⟼\mathrm{i}y\right)$$
83		oveq2	$$⊢y=\Im \left(\log x\right)\to \mathrm{i}y=\mathrm{i}\Im \left(\log x\right)$$
84	80 81 82 83	fmptco	$$⊢\top \to \left(y\in ℂ⟼\mathrm{i}y\right)\circ \left(x\in D⟼\Im \left(\log x\right)\right)=\left(x\in D⟼\mathrm{i}\Im \left(\log x\right)\right)$$
85		cncfss	$$⊢\left(ℝ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to D\underset{cn}{⟶}ℝ\subseteq D\underset{cn}{⟶}ℂ$$
86	50 64 85	mp2an	$$⊢D\underset{cn}{⟶}ℝ\subseteq D\underset{cn}{⟶}ℂ$$
87	1	logcnlem5	$$⊢\left(x\in D⟼\Im \left(\log x\right)\right):D\underset{cn}{⟶}ℝ$$
88	86 87	sselii	$$⊢\left(x\in D⟼\Im \left(\log x\right)\right):D\underset{cn}{⟶}ℂ$$
89	88	a1i	$$⊢\top \to \left(x\in D⟼\Im \left(\log x\right)\right):D\underset{cn}{⟶}ℂ$$
90		ax-icn	$$⊢\mathrm{i}\in ℂ$$
91		eqid	$$⊢\left(y\in ℂ⟼\mathrm{i}y\right)=\left(y\in ℂ⟼\mathrm{i}y\right)$$
92	91	mulc1cncf	$$⊢\mathrm{i}\in ℂ\to \left(y\in ℂ⟼\mathrm{i}y\right):ℂ\underset{cn}{⟶}ℂ$$
93	90 92	mp1i	$$⊢\top \to \left(y\in ℂ⟼\mathrm{i}y\right):ℂ\underset{cn}{⟶}ℂ$$
94	89 93	cncfco	$$⊢\top \to \left(\left(y\in ℂ⟼\mathrm{i}y\right)\circ \left(x\in D⟼\Im \left(\log x\right)\right)\right):D\underset{cn}{⟶}ℂ$$
95	84 94	eqeltrrd	$$⊢\top \to \left(x\in D⟼\mathrm{i}\Im \left(\log x\right)\right):D\underset{cn}{⟶}ℂ$$
96	27 29 77 95	cncfmpt2f	$$⊢\top \to \left(x\in D⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)+\mathrm{i}\Im \left(\log x\right)\right):D\underset{cn}{⟶}ℂ$$
97	96	mptru	$$⊢\left(x\in D⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(\left|x\right|\right)+\mathrm{i}\Im \left(\log x\right)\right):D\underset{cn}{⟶}ℂ$$
98	26 97	eqeltri	$$⊢\left({log\upharpoonright }_D\right):D\underset{cn}{⟶}ℂ$$