Metamath Proof Explorer


Theorem dvrelog2b

Description: Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 dvrelog2b.1 ( 𝜑𝐴 ∈ ℝ* )
2 dvrelog2b.2 ( 𝜑𝐵 ∈ ℝ* )
3 dvrelog2b.3 ( 𝜑 → 0 ≤ 𝐴 )
4 dvrelog2b.4 ( 𝜑𝐴𝐵 )
5 dvrelog2b.5 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) )
6 dvrelog2b.6 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) )
7 5 a1i ( 𝜑𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) ) )
8 2cnd ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℂ )
9 2ne0 2 ≠ 0
10 9 a1i ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
11 1red ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℝ )
12 1lt2 1 < 2
13 12 a1i ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 < 2 )
14 11 13 ltned ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ≠ 2 )
15 14 necomd ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 1 )
16 10 15 nelprd ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 2 ∈ { 0 , 1 } )
17 8 16 eldifd ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ( ℂ ∖ { 0 , 1 } ) )
18 elioore ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℝ )
19 recn ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
20 18 19 syl ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℂ )
21 20 adantl ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℂ )
22 elsni ( 𝑥 ∈ { 0 } → 𝑥 = 0 )
23 0xr 0 ∈ ℝ*
24 23 a1i ( 𝜑 → 0 ∈ ℝ* )
25 xrlenlt ( ( 0 ∈ ℝ*𝐴 ∈ ℝ* ) → ( 0 ≤ 𝐴 ↔ ¬ 𝐴 < 0 ) )
26 24 1 25 syl2anc ( 𝜑 → ( 0 ≤ 𝐴 ↔ ¬ 𝐴 < 0 ) )
27 3 26 mpbid ( 𝜑 → ¬ 𝐴 < 0 )
28 27 orcd ( 𝜑 → ( ¬ 𝐴 < 0 ∨ ¬ 0 < 𝐵 ) )
29 ianor ( ¬ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ↔ ( ¬ 𝐴 < 0 ∨ ¬ 0 < 𝐵 ) )
30 28 29 sylibr ( 𝜑 → ¬ ( 𝐴 < 0 ∧ 0 < 𝐵 ) )
31 elioo5 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 0 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) )
32 1 2 24 31 syl3anc ( 𝜑 → ( 0 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) )
33 32 notbid ( 𝜑 → ( ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) ↔ ¬ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) )
34 30 33 mpbird ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
35 34 a1d ( 𝜑 → ( 0 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) ) )
36 35 imp ( ( 𝜑 ∧ 0 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
37 36 pm2.01da ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
38 37 adantr ( ( 𝜑𝑥 = 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
39 eleq1 ( 𝑥 = 0 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ 0 ∈ ( 𝐴 (,) 𝐵 ) ) )
40 39 adantl ( ( 𝜑𝑥 = 0 ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ 0 ∈ ( 𝐴 (,) 𝐵 ) ) )
41 38 40 mtbird ( ( 𝜑𝑥 = 0 ) → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
42 22 41 sylan2 ( ( 𝜑𝑥 ∈ { 0 } ) → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
43 42 ex ( 𝜑 → ( 𝑥 ∈ { 0 } → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
44 43 con2d ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑥 ∈ { 0 } ) )
45 44 imp ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 ∈ { 0 } )
46 21 45 eldifd ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
47 logbval ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 logb 𝑥 ) = ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) )
48 17 46 47 syl2anc ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 logb 𝑥 ) = ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) )
49 48 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) )
50 7 49 eqtrd ( 𝜑𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) )
51 50 oveq2d ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) ) )
52 reelprrecn ℝ ∈ { ℝ , ℂ }
53 52 a1i ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
54 41 ex ( 𝜑 → ( 𝑥 = 0 → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
55 54 con2d ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑥 = 0 ) )
56 biidd ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑥 = 0 ↔ 𝑥 = 0 ) )
57 56 necon3bbid ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ¬ 𝑥 = 0 ↔ 𝑥 ≠ 0 ) )
58 57 pm5.74i ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑥 = 0 ) ↔ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ≠ 0 ) )
59 55 58 sylib ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ≠ 0 ) )
60 59 imp ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 0 )
61 21 60 logcld ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
62 18 adantl ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℝ )
63 11 62 60 redivcld ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 𝑥 ) ∈ ℝ )
64 eqid ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) )
65 eqid ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) )
66 1 2 3 4 64 65 dvrelog3 ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) )
67 2cnd ( 𝜑 → 2 ∈ ℂ )
68 9 a1i ( 𝜑 → 2 ≠ 0 )
69 67 68 logcld ( 𝜑 → ( log ‘ 2 ) ∈ ℂ )
70 0red ( 𝜑 → 0 ∈ ℝ )
71 2rp 2 ∈ ℝ+
72 loggt0b ( 2 ∈ ℝ+ → ( 0 < ( log ‘ 2 ) ↔ 1 < 2 ) )
73 71 72 ax-mp ( 0 < ( log ‘ 2 ) ↔ 1 < 2 )
74 12 73 mpbir 0 < ( log ‘ 2 )
75 74 a1i ( 𝜑 → 0 < ( log ‘ 2 ) )
76 70 75 ltned ( 𝜑 → 0 ≠ ( log ‘ 2 ) )
77 76 necomd ( 𝜑 → ( log ‘ 2 ) ≠ 0 )
78 53 61 63 66 69 77 dvmptdivc ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 1 / 𝑥 ) / ( log ‘ 2 ) ) ) )
79 8 10 logcld ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 2 ) ∈ ℂ )
80 77 adantr ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 2 ) ≠ 0 )
81 21 79 60 80 recdiv2d ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 / 𝑥 ) / ( log ‘ 2 ) ) = ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) )
82 81 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 1 / 𝑥 ) / ( log ‘ 2 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) )
83 6 a1i ( 𝜑𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) )
84 83 eqcomd ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) = 𝐺 )
85 82 84 eqtrd ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 1 / 𝑥 ) / ( log ‘ 2 ) ) ) = 𝐺 )
86 78 85 eqtrd ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) ) = 𝐺 )
87 51 86 eqtrd ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )