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 𝐹 ) = 𝐺 )