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 ⊢ S = 1 ball ⁡ abs ∘ − 1
Assertion dvlog2 ⊢ ℂ D log ↾ S = x ∈ S ⟼ 1 x

Proof

Step Hyp Ref Expression
1 dvlog2.s ⊢ 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 ⊢ x ∈ ran ⁡ log → x ∈ ℂ
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 ⊢ S ⊆ ℂ
21 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
22 21 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
23 22 toponrestid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
24 21 23 dvres ⊢ ℂ ⊆ ℂ ∧ log ↾ ℂ ∖ −∞ 0 : ℂ ∖ −∞ 0 ⟶ ℂ ∧ ℂ ∖ −∞ 0 ⊆ ℂ ∧ S ⊆ ℂ → ℂ D log ↾ ℂ ∖ −∞ 0 ↾ S = log ↾ ℂ ∖ −∞ 0 ℂ ′ ↾ int ⁡ TopOpen ⁡ ℂ fld ⁡ S
25 2 13 14 20 24 mp4an ⊢ ℂ D log ↾ ℂ ∖ −∞ 0 ↾ S = log ↾ ℂ ∖ −∞ 0 ℂ ′ ↾ int ⁡ TopOpen ⁡ ℂ fld ⁡ S
26 1 dvlog2lem ⊢ S ⊆ ℂ ∖ −∞ 0
27 resabs1 ⊢ S ⊆ ℂ ∖ −∞ 0 → log ↾ ℂ ∖ −∞ 0 ↾ S = log ↾ S
28 26 27 ax-mp ⊢ log ↾ ℂ ∖ −∞ 0 ↾ S = log ↾ S
29 28 oveq2i ⊢ ℂ D log ↾ ℂ ∖ −∞ 0 ↾ S = ℂ D log ↾ S
30 10 dvlog ⊢ ℂ D log ↾ ℂ ∖ −∞ 0 = x ∈ ℂ ∖ −∞ 0 ⟼ 1 x
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 ⊢ S ∈ TopOpen ⁡ ℂ fld
36 isopn3i ⊢ TopOpen ⁡ ℂ fld ∈ Top ∧ S ∈ TopOpen ⁡ ℂ fld → int ⁡ TopOpen ⁡ ℂ fld ⁡ S = S
37 31 35 36 mp2an ⊢ int ⁡ TopOpen ⁡ ℂ fld ⁡ S = S
38 30 37 reseq12i ⊢ log ↾ ℂ ∖ −∞ 0 ℂ ′ ↾ int ⁡ TopOpen ⁡ ℂ fld ⁡ S = x ∈ ℂ ∖ −∞ 0 ⟼ 1 x ↾ S
39 25 29 38 3eqtr3i ⊢ ℂ D log ↾ S = x ∈ ℂ ∖ −∞ 0 ⟼ 1 x ↾ S
40 resmpt ⊢ S ⊆ ℂ ∖ −∞ 0 → x ∈ ℂ ∖ −∞ 0 ⟼ 1 x ↾ S = x ∈ S ⟼ 1 x
41 26 40 ax-mp ⊢ x ∈ ℂ ∖ −∞ 0 ⟼ 1 x ↾ S = x ∈ S ⟼ 1 x
42 39 41 eqtri ⊢ ℂ D log ↾ S = x ∈ S ⟼ 1 x