Theorem dvlog2

Description: The derivative of the complex logarithm function on the open unit ball centered at 1 , a sometimes easier region to work with than the CC \ ( -oo , 0 ] of dvlog . (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypothesis	dvlog2.s	⊢ 𝑆 = ( 1 ( ball ‘ ( abs ∘ − ) ) 1 )
Assertion	dvlog2	⊢ ( ℂ D ( log ↾ 𝑆 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 / 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		dvlog2.s	⊢ 𝑆 = ( 1 ( ball ‘ ( abs ∘ − ) ) 1 )
2		ssid	⊢ ℂ ⊆ ℂ
3		logf1o	⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
4		f1of	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
5	3 4	ax-mp	⊢ log : ( ℂ ∖ { 0 } ) ⟶ ran log
6		logrncn	⊢ ( 𝑥 ∈ ran log → 𝑥 ∈ ℂ )
7	6	ssriv	⊢ ran log ⊆ ℂ
8		fss	⊢ ( ( log : ( ℂ ∖ { 0 } ) ⟶ ran log ∧ ran log ⊆ ℂ ) → log : ( ℂ ∖ { 0 } ) ⟶ ℂ )
9	5 7 8	mp2an	⊢ log : ( ℂ ∖ { 0 } ) ⟶ ℂ
10		eqid	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
11	10	logdmss	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } )
12		fssres	⊢ ( ( log : ( ℂ ∖ { 0 } ) ⟶ ℂ ∧ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } ) ) → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) ⟶ ℂ )
13	9 11 12	mp2an	⊢ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) ⟶ ℂ
14		difss	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ
15		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
16		ax-1cn	⊢ 1 ∈ ℂ
17		1xr	⊢ 1 ∈ ℝ*
18		blssm	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ* ) → ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ℂ )
19	15 16 17 18	mp3an	⊢ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ℂ
20	1 19	eqsstri	⊢ 𝑆 ⊆ ℂ
21		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
22	21	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
23	22	toponrestid	⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
24	21 23	dvres	⊢ ( ( ( ℂ ⊆ ℂ ∧ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) ⟶ ℂ ) ∧ ( ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ ∧ 𝑆 ⊆ ℂ ) ) → ( ℂ D ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↾ 𝑆 ) ) = ( ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) ) )
25	2 13 14 20 24	mp4an	⊢ ( ℂ D ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↾ 𝑆 ) ) = ( ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) )
26	1	dvlog2lem	⊢ 𝑆 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )
27		resabs1	⊢ ( 𝑆 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↾ 𝑆 ) = ( log ↾ 𝑆 ) )
28	26 27	ax-mp	⊢ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↾ 𝑆 ) = ( log ↾ 𝑆 )
29	28	oveq2i	⊢ ( ℂ D ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↾ 𝑆 ) ) = ( ℂ D ( log ↾ 𝑆 ) )
30	10	dvlog	⊢ ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑥 ) )
31	21	cnfldtop	⊢ ( TopOpen ‘ ℂfld ) ∈ Top
32	21	cnfldtopn	⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
33	32	blopn	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ* ) → ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ ( TopOpen ‘ ℂfld ) )
34	15 16 17 33	mp3an	⊢ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ ( TopOpen ‘ ℂfld )
35	1 34	eqeltri	⊢ 𝑆 ∈ ( TopOpen ‘ ℂfld )
36		isopn3i	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ∈ ( TopOpen ‘ ℂfld ) ) → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) = 𝑆 )
37	31 35 36	mp2an	⊢ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) = 𝑆
38	30 37	reseq12i	⊢ ( ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) ) = ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑥 ) ) ↾ 𝑆 )
39	25 29 38	3eqtr3i	⊢ ( ℂ D ( log ↾ 𝑆 ) ) = ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑥 ) ) ↾ 𝑆 )
40		resmpt	⊢ ( 𝑆 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑥 ) ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 / 𝑥 ) ) )
41	26 40	ax-mp	⊢ ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑥 ) ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 / 𝑥 ) )
42	39 41	eqtri	⊢ ( ℂ D ( log ↾ 𝑆 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 / 𝑥 ) )