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

Metamath Proof Explorer

Theorem dvrelog

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

Ref Expression
Assertion dvrelog ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )

Proof

Step Hyp Ref Expression
1 dfrelog ⊢ ( log ↾ ℝ+ ) = ◡ ( exp ↾ ℝ )
2 1 oveq2i ⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( ℝ D ◡ ( exp ↾ ℝ ) )
3 reeff1o ⊢ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+
4 f1of ⊢ ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ → ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ )
5 3 4 ax-mp ⊢ ( exp ↾ ℝ ) : ℝ ⟶ ℝ+
6 rpssre ⊢ ℝ+ ⊆ ℝ
7 fss ⊢ ( ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ ∧ ℝ+ ⊆ ℝ ) → ( exp ↾ ℝ ) : ℝ ⟶ ℝ )
8 5 6 7 mp2an ⊢ ( exp ↾ ℝ ) : ℝ ⟶ ℝ
9 ax-resscn ⊢ ℝ ⊆ ℂ
10 efcn ⊢ exp ∈ ( ℂ –cn→ ℂ )
11 rescncf ⊢ ( ℝ ⊆ ℂ → ( exp ∈ ( ℂ –cn→ ℂ ) → ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) )
12 9 10 11 mp2 ⊢ ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℂ )
13 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) → ( ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) ↔ ( exp ↾ ℝ ) : ℝ ⟶ ℝ ) )
14 9 12 13 mp2an ⊢ ( ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) ↔ ( exp ↾ ℝ ) : ℝ ⟶ ℝ )
15 8 14 mpbir ⊢ ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )
16 15 a1i ⊢ ( ⊤ → ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) )
17 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
18 eff ⊢ exp : ℂ ⟶ ℂ
19 ssid ⊢ ℂ ⊆ ℂ
20 dvef ⊢ ( ℂ D exp ) = exp
21 20 dmeqi ⊢ dom ( ℂ D exp ) = dom exp
22 18 fdmi ⊢ dom exp = ℂ
23 21 22 eqtri ⊢ dom ( ℂ D exp ) = ℂ
24 9 23 sseqtrri ⊢ ℝ ⊆ dom ( ℂ D exp )
25 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ exp : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D exp ) ) ) → ( ℝ D ( exp ↾ ℝ ) ) = ( ( ℂ D exp ) ↾ ℝ ) )
26 17 18 19 24 25 mp4an ⊢ ( ℝ D ( exp ↾ ℝ ) ) = ( ( ℂ D exp ) ↾ ℝ )
27 20 reseq1i ⊢ ( ( ℂ D exp ) ↾ ℝ ) = ( exp ↾ ℝ )
28 26 27 eqtri ⊢ ( ℝ D ( exp ↾ ℝ ) ) = ( exp ↾ ℝ )
29 28 dmeqi ⊢ dom ( ℝ D ( exp ↾ ℝ ) ) = dom ( exp ↾ ℝ )
30 5 fdmi ⊢ dom ( exp ↾ ℝ ) = ℝ
31 29 30 eqtri ⊢ dom ( ℝ D ( exp ↾ ℝ ) ) = ℝ
32 31 a1i ⊢ ( ⊤ → dom ( ℝ D ( exp ↾ ℝ ) ) = ℝ )
33 0nrp ⊢ ¬ 0 ∈ ℝ+
34 28 rneqi ⊢ ran ( ℝ D ( exp ↾ ℝ ) ) = ran ( exp ↾ ℝ )
35 f1ofo ⊢ ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ → ( exp ↾ ℝ ) : ℝ –onto→ ℝ+ )
36 forn ⊢ ( ( exp ↾ ℝ ) : ℝ –onto→ ℝ+ → ran ( exp ↾ ℝ ) = ℝ+ )
37 3 35 36 mp2b ⊢ ran ( exp ↾ ℝ ) = ℝ+
38 34 37 eqtri ⊢ ran ( ℝ D ( exp ↾ ℝ ) ) = ℝ+
39 38 eleq2i ⊢ ( 0 ∈ ran ( ℝ D ( exp ↾ ℝ ) ) ↔ 0 ∈ ℝ+ )
40 33 39 mtbir ⊢ ¬ 0 ∈ ran ( ℝ D ( exp ↾ ℝ ) )
41 40 a1i ⊢ ( ⊤ → ¬ 0 ∈ ran ( ℝ D ( exp ↾ ℝ ) ) )
42 3 a1i ⊢ ( ⊤ → ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ )
43 16 32 41 42 dvcnvre ⊢ ( ⊤ → ( ℝ D ◡ ( exp ↾ ℝ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) ) ) )
44 43 mptru ⊢ ( ℝ D ◡ ( exp ↾ ℝ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) ) )
45 28 fveq1i ⊢ ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) = ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) )
46 f1ocnvfv2 ⊢ ( ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) = 𝑥 )
47 3 46 mpan ⊢ ( 𝑥 ∈ ℝ+ → ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) = 𝑥 )
48 45 47 eqtrid ⊢ ( 𝑥 ∈ ℝ+ → ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) = 𝑥 )
49 48 oveq2d ⊢ ( 𝑥 ∈ ℝ+ → ( 1 / ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) ) = ( 1 / 𝑥 ) )
50 49 mpteq2ia ⊢ ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
51 44 50 eqtri ⊢ ( ℝ D ◡ ( exp ↾ ℝ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
52 2 51 eqtri ⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )