dvlog

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

		Ref	Expression
	Hypothesis	logcn.d	$⊢ D = ℂ ∖ (−∞, 0]$
	Assertion	dvlog	$⊢ ℂ D ({log ↾}_{D}) = (x \in D ⟼ \frac{1}{x})$

Proof

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

Metamath Proof Explorer

Theorem dvlog

Proof