Metamath Proof Explorer


Theorem dvrelog3

Description: The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024)

Ref Expression
Hypotheses dvrelog3.1 ( 𝜑𝐴 ∈ ℝ* )
dvrelog3.2 ( 𝜑𝐵 ∈ ℝ* )
dvrelog3.3 ( 𝜑 → 0 ≤ 𝐴 )
dvrelog3.4 ( 𝜑𝐴𝐵 )
dvrelog3.5 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) )
dvrelog3.6 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) )
Assertion dvrelog3 ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )

Proof

Step Hyp Ref Expression
1 dvrelog3.1 ( 𝜑𝐴 ∈ ℝ* )
2 dvrelog3.2 ( 𝜑𝐵 ∈ ℝ* )
3 dvrelog3.3 ( 𝜑 → 0 ≤ 𝐴 )
4 dvrelog3.4 ( 𝜑𝐴𝐵 )
5 dvrelog3.5 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) )
6 dvrelog3.6 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) )
7 5 a1i ( 𝜑𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) )
8 7 oveq2d ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) )
9 reelprrecn ℝ ∈ { ℝ , ℂ }
10 9 a1i ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
11 rpcn ( 𝑥 ∈ ℝ+𝑥 ∈ ℂ )
12 11 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
13 rpne0 ( 𝑥 ∈ ℝ+𝑥 ≠ 0 )
14 13 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
15 12 14 logcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
16 1red ( ( 𝜑𝑥 ∈ ℝ+ ) → 1 ∈ ℝ )
17 rpre ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ )
18 17 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
19 16 18 14 redivcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ )
20 logf1o log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
21 f1of ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
22 20 21 ax-mp log : ( ℂ ∖ { 0 } ) ⟶ ran log
23 22 a1i ( 𝜑 → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
24 0nrp ¬ 0 ∈ ℝ+
25 disjsn ( ( ℝ+ ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ℝ+ )
26 24 25 mpbir ( ℝ+ ∩ { 0 } ) = ∅
27 disjdif2 ( ( ℝ+ ∩ { 0 } ) = ∅ → ( ℝ+ ∖ { 0 } ) = ℝ+ )
28 26 27 ax-mp ( ℝ+ ∖ { 0 } ) = ℝ+
29 rpssre + ⊆ ℝ
30 ax-resscn ℝ ⊆ ℂ
31 29 30 sstri + ⊆ ℂ
32 ssdif ( ℝ+ ⊆ ℂ → ( ℝ+ ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } ) )
33 31 32 ax-mp ( ℝ+ ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } )
34 28 33 eqsstrri + ⊆ ( ℂ ∖ { 0 } )
35 34 a1i ( 𝜑 → ℝ+ ⊆ ( ℂ ∖ { 0 } ) )
36 23 35 feqresmpt ( 𝜑 → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
37 36 eqcomd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) = ( log ↾ ℝ+ ) )
38 37 oveq2d ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( ℝ D ( log ↾ ℝ+ ) ) )
39 dvrelog ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
40 39 a1i ( 𝜑 → ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
41 38 40 eqtrd ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
42 elioo2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦𝑦 < 𝐵 ) ) )
43 1 2 42 syl2anc ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦𝑦 < 𝐵 ) ) )
44 43 biimpa ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦𝑦 < 𝐵 ) )
45 44 simp1d ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ )
46 0red ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
47 46 rexrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ* )
48 1 adantr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
49 45 rexrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ* )
50 3 adantr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ 𝐴 )
51 44 simp2d ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑦 )
52 47 48 49 50 51 xrlelttrd ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < 𝑦 )
53 45 52 jca ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) )
54 elrp ( 𝑦 ∈ ℝ+ ↔ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) )
55 53 54 sylibr ( ( 𝜑𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ+ )
56 55 ex ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → 𝑦 ∈ ℝ+ ) )
57 56 ssrdv ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ+ )
58 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
59 58 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
60 retop ( topGen ‘ ran (,) ) ∈ Top
61 60 a1i ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
62 iooretop ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
63 62 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
64 isopn3i ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
65 61 63 64 syl2anc ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
66 10 15 19 41 57 59 58 65 dvmptres2 ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) )
67 8 66 eqtrd ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) )
68 6 a1i ( 𝜑𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) )
69 68 eqcomd ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) = 𝐺 )
70 67 69 eqtrd ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )