Metamath Proof Explorer


Theorem dvrelog2

Description: The derivative of the logarithm, ftc2 version. (Contributed by metakunt, 11-Aug-2024)

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

Proof

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