This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 / 𝑥 ) )