Theorem dvlog

Description: The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015)

	Ref	Expression
Hypothesis	logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
Assertion	dvlog	$$⊢ℂ\mathrm{D}\left({log\upharpoonright }_D\right)=\left(x\in D⟼\frac{1}{x}\right)$$

Proof

Step	Hyp	Ref	Expression
1		logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3	2	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
4	3	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
5		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
6	5	a1i	$$⊢\top \to ℂ\in \left\{ℝ,ℂ\right\}$$
7	1	logdmopn	$$⊢D\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
8	7	a1i	$$⊢\top \to D\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
9		logf1o	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log$$
10		f1of1	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log\to log:ℂ\setminus \left\{0\right\}\underset{1-1}{⟶}\mathrm{ran}log$$
11	9 10	ax-mp	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1}{⟶}\mathrm{ran}log$$
12	1	logdmss	$$⊢D\subseteq ℂ\setminus \left\{0\right\}$$
13		f1ores	$$⊢\left(log:ℂ\setminus \left\{0\right\}\underset{1-1}{⟶}\mathrm{ran}log\wedge D\subseteq ℂ\setminus \left\{0\right\}\right)\to \left({log\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}log\left[D\right]$$
14	11 12 13	mp2an	$$⊢\left({log\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}log\left[D\right]$$
15		f1ocnv	$$⊢\left({log\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}log\left[D\right]\to {\left({log\upharpoonright }_D\right)}^{-1}:log\left[D\right]\underset{1-1\; onto}{⟶}D$$
16	14 15	ax-mp	$$⊢{\left({log\upharpoonright }_D\right)}^{-1}:log\left[D\right]\underset{1-1\; onto}{⟶}D$$
17		df-log	$$⊢log={\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}$$
18	17	reseq1i	$$⊢{log\upharpoonright }_D={{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\upharpoonright }_D$$
19	18	cnveqi	$$⊢{\left({log\upharpoonright }_D\right)}^{-1}={\left({{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\upharpoonright }_D\right)}^{-1}$$
20		eff	$$⊢\exp :ℂ⟶ℂ$$
21		cnvimass	$$⊢{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]\subseteq \mathrm{dom}\Im$$
22		imf	$$⊢\Im :ℂ⟶ℝ$$
23	22	fdmi	$$⊢\mathrm{dom}\Im =ℂ$$
24	21 23	sseqtri	$$⊢{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]\subseteq ℂ$$
25		fssres	$$⊢\left(\exp :ℂ⟶ℂ\wedge {\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]\subseteq ℂ\right)\to \left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right):{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]⟶ℂ$$
26	20 24 25	mp2an	$$⊢\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right):{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]⟶ℂ$$
27		ffun	$$⊢\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right):{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]⟶ℂ\to \mathrm{Fun}\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)$$
28		funcnvres2	$$⊢\mathrm{Fun}\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)\to {\left({{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\upharpoonright }_D\right)}^{-1}={\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)\upharpoonright }_{{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]}$$
29	26 27 28	mp2b	$$⊢{\left({{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\upharpoonright }_D\right)}^{-1}={\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)\upharpoonright }_{{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]}$$
30		cnvimass	$$⊢{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]\subseteq \mathrm{dom}\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)$$
31	26	fdmi	$$⊢\mathrm{dom}\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
32	30 31	sseqtri	$$⊢{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]\subseteq {\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
33		resabs1	$$⊢{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]\subseteq {\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]\to {\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)\upharpoonright }_{{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]}={\exp \upharpoonright }_{{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]}$$
34	32 33	ax-mp	$$⊢{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)\upharpoonright }_{{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]}={\exp \upharpoonright }_{{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]}$$
35	19 29 34	3eqtri	$$⊢{\left({log\upharpoonright }_D\right)}^{-1}={\exp \upharpoonright }_{{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]}$$
36	17	imaeq1i	$$⊢log\left[D\right]={\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]$$
37	36	reseq2i	$$⊢{\exp \upharpoonright }_{log\left[D\right]}={\exp \upharpoonright }_{{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}\left[D\right]}$$
38	35 37	eqtr4i	$$⊢{\left({log\upharpoonright }_D\right)}^{-1}={\exp \upharpoonright }_{log\left[D\right]}$$
39		f1oeq1	$$⊢{\left({log\upharpoonright }_D\right)}^{-1}={\exp \upharpoonright }_{log\left[D\right]}\to \left({\left({log\upharpoonright }_D\right)}^{-1}:log\left[D\right]\underset{1-1\; onto}{⟶}D\leftrightarrow \left({\exp \upharpoonright }_{log\left[D\right]}\right):log\left[D\right]\underset{1-1\; onto}{⟶}D\right)$$
40	38 39	ax-mp	$$⊢{\left({log\upharpoonright }_D\right)}^{-1}:log\left[D\right]\underset{1-1\; onto}{⟶}D\leftrightarrow \left({\exp \upharpoonright }_{log\left[D\right]}\right):log\left[D\right]\underset{1-1\; onto}{⟶}D$$
41	16 40	mpbi	$$⊢\left({\exp \upharpoonright }_{log\left[D\right]}\right):log\left[D\right]\underset{1-1\; onto}{⟶}D$$
42	41	a1i	$$⊢\top \to \left({\exp \upharpoonright }_{log\left[D\right]}\right):log\left[D\right]\underset{1-1\; onto}{⟶}D$$
43	38	cnveqi	$$⊢{{\left({log\upharpoonright }_D\right)}^{-1}}^{-1}={\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}$$
44		relres	$$⊢\mathrm{Rel}\left({log\upharpoonright }_D\right)$$
45		dfrel2	$$⊢\mathrm{Rel}\left({log\upharpoonright }_D\right)\leftrightarrow {{\left({log\upharpoonright }_D\right)}^{-1}}^{-1}={log\upharpoonright }_D$$
46	44 45	mpbi	$$⊢{{\left({log\upharpoonright }_D\right)}^{-1}}^{-1}={log\upharpoonright }_D$$
47	43 46	eqtr3i	$$⊢{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}={log\upharpoonright }_D$$
48		f1of	$$⊢\left({log\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}log\left[D\right]\to \left({log\upharpoonright }_D\right):D⟶log\left[D\right]$$
49	14 48	mp1i	$$⊢\top \to \left({log\upharpoonright }_D\right):D⟶log\left[D\right]$$
50		imassrn	$$⊢log\left[D\right]\subseteq \mathrm{ran}log$$
51		logrncn	$$⊢x\in \mathrm{ran}log\to x\in ℂ$$
52	51	ssriv	$$⊢\mathrm{ran}log\subseteq ℂ$$
53	50 52	sstri	$$⊢log\left[D\right]\subseteq ℂ$$
54	1	logcn	$$⊢\left({log\upharpoonright }_D\right):D\underset{cn}{⟶}ℂ$$
55		cncfcdm	$$⊢\left(log\left[D\right]\subseteq ℂ\wedge \left({log\upharpoonright }_D\right):D\underset{cn}{⟶}ℂ\right)\to \left(\left({log\upharpoonright }_D\right):D\underset{cn}{⟶}log\left[D\right]\leftrightarrow \left({log\upharpoonright }_D\right):D⟶log\left[D\right]\right)$$
56	53 54 55	mp2an	$$⊢\left({log\upharpoonright }_D\right):D\underset{cn}{⟶}log\left[D\right]\leftrightarrow \left({log\upharpoonright }_D\right):D⟶log\left[D\right]$$
57	49 56	sylibr	$$⊢\top \to \left({log\upharpoonright }_D\right):D\underset{cn}{⟶}log\left[D\right]$$
58	47 57	eqeltrid	$$⊢\top \to {\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}:D\underset{cn}{⟶}log\left[D\right]$$
59		ssid	$$⊢ℂ\subseteq ℂ$$
60	2 4	dvres	$$⊢\left(\left(ℂ\subseteq ℂ\wedge \exp :ℂ⟶ℂ\right)\wedge \left(ℂ\subseteq ℂ\wedge log\left[D\right]\subseteq ℂ\right)\right)\to ℂ\mathrm{D}\left({\exp \upharpoonright }_{log\left[D\right]}\right)={{\exp }_{ℂ}^{\prime }\upharpoonright }_{\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(log\left[D\right]\right)}$$
61	59 20 59 53 60	mp4an	$$⊢ℂ\mathrm{D}\left({\exp \upharpoonright }_{log\left[D\right]}\right)={{\exp }_{ℂ}^{\prime }\upharpoonright }_{\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(log\left[D\right]\right)}$$
62		dvef	$$⊢ℂ\mathrm{D}\exp =\exp$$
63	2	cnfldtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
64	1	dvloglem	$$⊢log\left[D\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
65		isopn3i	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge log\left[D\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(log\left[D\right]\right)=log\left[D\right]$$
66	63 64 65	mp2an	$$⊢\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(log\left[D\right]\right)=log\left[D\right]$$
67	62 66	reseq12i	$$⊢{{\exp }_{ℂ}^{\prime }\upharpoonright }_{\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(log\left[D\right]\right)}={\exp \upharpoonright }_{log\left[D\right]}$$
68	61 67	eqtri	$$⊢ℂ\mathrm{D}\left({\exp \upharpoonright }_{log\left[D\right]}\right)={\exp \upharpoonright }_{log\left[D\right]}$$
69	68	dmeqi	$$⊢\mathrm{dom}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }=\mathrm{dom}\left({\exp \upharpoonright }_{log\left[D\right]}\right)$$
70		dmres	$$⊢\mathrm{dom}\left({\exp \upharpoonright }_{log\left[D\right]}\right)=log\left[D\right]\cap \mathrm{dom}\exp$$
71	20	fdmi	$$⊢\mathrm{dom}\exp =ℂ$$
72	53 71	sseqtrri	$$⊢log\left[D\right]\subseteq \mathrm{dom}\exp$$
73		df-ss	$$⊢log\left[D\right]\subseteq \mathrm{dom}\exp \leftrightarrow log\left[D\right]\cap \mathrm{dom}\exp =log\left[D\right]$$
74	72 73	mpbi	$$⊢log\left[D\right]\cap \mathrm{dom}\exp =log\left[D\right]$$
75	69 70 74	3eqtri	$$⊢\mathrm{dom}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }=log\left[D\right]$$
76	75	a1i	$$⊢\top \to \mathrm{dom}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }=log\left[D\right]$$
77		neirr	$$⊢\neg 0\ne 0$$
78		resss	$$⊢{{\exp }_{ℂ}^{\prime }\upharpoonright }_{\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(log\left[D\right]\right)}\subseteq ℂ\mathrm{D}\exp$$
79	61 78	eqsstri	$$⊢ℂ\mathrm{D}\left({\exp \upharpoonright }_{log\left[D\right]}\right)\subseteq ℂ\mathrm{D}\exp$$
80	79 62	sseqtri	$$⊢ℂ\mathrm{D}\left({\exp \upharpoonright }_{log\left[D\right]}\right)\subseteq \exp$$
81	80	rnssi	$$⊢\mathrm{ran}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\subseteq \mathrm{ran}\exp$$
82		eff2	$$⊢\exp :ℂ⟶ℂ\setminus \left\{0\right\}$$
83		frn	$$⊢\exp :ℂ⟶ℂ\setminus \left\{0\right\}\to \mathrm{ran}\exp \subseteq ℂ\setminus \left\{0\right\}$$
84	82 83	ax-mp	$$⊢\mathrm{ran}\exp \subseteq ℂ\setminus \left\{0\right\}$$
85	81 84	sstri	$$⊢\mathrm{ran}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\subseteq ℂ\setminus \left\{0\right\}$$
86	85	sseli	$$⊢0\in \mathrm{ran}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\to 0\in \left(ℂ\setminus \left\{0\right\}\right)$$
87		eldifsn	$$⊢0\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(0\in ℂ\wedge 0\ne 0\right)$$
88	86 87	sylib	$$⊢0\in \mathrm{ran}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\to \left(0\in ℂ\wedge 0\ne 0\right)$$
89	88	simprd	$$⊢0\in \mathrm{ran}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\to 0\ne 0$$
90	77 89	mto	$$⊢\neg 0\in \mathrm{ran}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }$$
91	90	a1i	$$⊢\top \to \neg 0\in \mathrm{ran}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }$$
92	2 4 6 8 42 58 76 91	dvcnv	$$⊢\top \to ℂ\mathrm{D}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}=\left(x\in D⟼\frac{1}{{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)}\right)$$
93	92	mptru	$$⊢ℂ\mathrm{D}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}=\left(x\in D⟼\frac{1}{{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)}\right)$$
94	47	oveq2i	$$⊢ℂ\mathrm{D}{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}=ℂ\mathrm{D}\left({log\upharpoonright }_D\right)$$
95	68	fveq1i	$$⊢{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)=\left({\exp \upharpoonright }_{log\left[D\right]}\right)\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)$$
96		f1ocnvfv2	$$⊢\left(\left({\exp \upharpoonright }_{log\left[D\right]}\right):log\left[D\right]\underset{1-1\; onto}{⟶}D\wedge x\in D\right)\to \left({\exp \upharpoonright }_{log\left[D\right]}\right)\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)=x$$
97	41 96	mpan	$$⊢x\in D\to \left({\exp \upharpoonright }_{log\left[D\right]}\right)\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)=x$$
98	95 97	eqtrid	$$⊢x\in D\to {\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)=x$$
99	98	oveq2d	$$⊢x\in D\to \frac{1}{{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)}=\frac{1}{x}$$
100	99	mpteq2ia	$$⊢\left(x\in D⟼\frac{1}{{\left({\exp \upharpoonright }_{log\left[D\right]}\right)}_{ℂ}^{\prime }\left({\left({\exp \upharpoonright }_{log\left[D\right]}\right)}^{-1}\left(x\right)\right)}\right)=\left(x\in D⟼\frac{1}{x}\right)$$
101	93 94 100	3eqtr3i	$$⊢ℂ\mathrm{D}\left({log\upharpoonright }_D\right)=\left(x\in D⟼\frac{1}{x}\right)$$