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

Proof

Step Hyp Ref Expression
1 dvlog2.s ⊢S=1ball⁡abs∘−1
2 ssid ⊢ℂ⊆ℂ
3 logf1o ⊢log:ℂ∖0⟶1-1 ontoran⁡log
4 f1of ⊢log:ℂ∖0⟶1-1 ontoran⁡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∈ℝ*→1ball⁡abs∘−1⊆ℂ
19 15 16 17 18 mp3an ⊢1ball⁡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⊆ℂ→ℂDlog↾ℂ∖−∞0↾S=log↾ℂ∖−∞0ℂ′↾int⁡TopOpen⁡ℂfld⁡S
25 2 13 14 20 24 mp4an ⊢ℂDlog↾ℂ∖−∞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 ⊢ℂDlog↾ℂ∖−∞0↾S=ℂDlog↾S
30 10 dvlog ⊢ℂDlog↾ℂ∖−∞0=x∈ℂ∖−∞0⟼1x
31 21 cnfldtop ⊢TopOpen⁡ℂfld∈Top
32 21 cnfldtopn ⊢TopOpen⁡ℂfld=MetOpen⁡abs∘−
33 32 blopn ⊢abs∘−∈∞Met⁡ℂ∧1∈ℂ∧1∈ℝ*→1ball⁡abs∘−1∈TopOpen⁡ℂfld
34 15 16 17 33 mp3an ⊢1ball⁡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⟼1x↾S
39 25 29 38 3eqtr3i ⊢ℂDlog↾S=x∈ℂ∖−∞0⟼1x↾S
40 resmpt ⊢S⊆ℂ∖−∞0→x∈ℂ∖−∞0⟼1x↾S=x∈S⟼1x
41 26 40 ax-mp ⊢x∈ℂ∖−∞0⟼1x↾S=x∈S⟼1x
42 39 41 eqtri ⊢ℂDlog↾S=x∈S⟼1x