Metamath Proof Explorer

Theorem dvrelogpow2b

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

Ref Expression
Hypotheses dvrelogpow2b.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvrelogpow2b.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvrelogpow2b.3 ⊢ ( 𝜑 → 0 < 𝐴 )
dvrelogpow2b.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
dvrelogpow2b.5 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 logb 𝑥 ) ↑ 𝑁 ) )
dvrelogpow2b.6 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) )
dvrelogpow2b.7 ⊢ 𝐶 = ( 𝑁 / ( ( log ‘ 2 ) ↑ 𝑁 ) )
dvrelogpow2b.8 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion dvrelogpow2b ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )

Proof

Step Hyp Ref Expression
1 dvrelogpow2b.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvrelogpow2b.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dvrelogpow2b.3 ⊢ ( 𝜑 → 0 < 𝐴 )
4 dvrelogpow2b.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 dvrelogpow2b.5 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 logb 𝑥 ) ↑ 𝑁 ) )
6 dvrelogpow2b.6 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) )
7 dvrelogpow2b.7 ⊢ 𝐶 = ( 𝑁 / ( ( log ‘ 2 ) ↑ 𝑁 ) )
8 dvrelogpow2b.8 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 5 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 logb 𝑥 ) ↑ 𝑁 ) ) )
10 9 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 logb 𝑥 ) ↑ 𝑁 ) ) ) )
11 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
12 11 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
13 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
14 13 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
15 elioore ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℝ )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℝ )
17 16 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℂ )
18 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
20 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < 𝐴 )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ≤ 𝐵 )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
23 18 19 20 21 22 0nonelalab ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≠ 𝑥 )
24 23 necomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 0 )
25 17 24 logcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
26 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℂ )
27 0ne2 ⊢ 0 ≠ 2
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≠ 2 )
29 28 necomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
30 26 29 logcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 2 ) ∈ ℂ )
31 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
32 1lt2 ⊢ 1 < 2
33 32 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 < 2 )
34 2rp ⊢ 2 ∈ ℝ+
35 loggt0b ⊢ ( 2 ∈ ℝ+ → ( 0 < ( log ‘ 2 ) ↔ 1 < 2 ) )
36 34 35 ax-mp ⊢ ( 0 < ( log ‘ 2 ) ↔ 1 < 2 )
37 33 36 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < ( log ‘ 2 ) )
38 31 37 ltned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≠ ( log ‘ 2 ) )
39 38 necomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 2 ) ≠ 0 )
40 25 30 39 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ∈ ℂ )
41 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℝ )
42 41 33 ltned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ≠ 2 )
43 42 necomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 1 )
44 29 43 nelprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 2 ∈ { 0 , 1 } )
45 26 44 eldifd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ( ℂ ∖ { 0 , 1 } ) )
46 necom ⊢ ( 0 ≠ 𝑥 ↔ 𝑥 ≠ 0 )
47 46 imbi2i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≠ 𝑥 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 0 ) )
48 23 47 mpbi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 0 )
49 48 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 = 0 )
50 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
51 49 50 sylnibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 ∈ { 0 } )
52 17 51 eldifd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
53 logbval ⊢ ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 logb 𝑥 ) = ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) )
54 45 52 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 logb 𝑥 ) = ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) )
55 54 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 2 logb 𝑥 ) ∈ ℂ ↔ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ∈ ℂ ) )
56 40 55 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 logb 𝑥 ) ∈ ℂ )
57 34 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℝ+ )
58 57 relogcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 2 ) ∈ ℝ )
59 16 58 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 · ( log ‘ 2 ) ) ∈ ℝ )
60 57 rpne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
61 26 60 logcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 2 ) ∈ ℂ )
62 17 61 24 39 mulne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 · ( log ‘ 2 ) ) ≠ 0 )
63 41 59 62 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ∈ ℝ )
64 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
65 8 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
67 64 66 expcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝑁 ) ∈ ℂ )
68 8 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑁 ∈ ℂ )
70 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
71 8 70 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℕ0 )
73 64 72 expcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
74 69 73 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ )
75 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
76 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
77 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
78 77 1 3 ltled ⊢ ( 𝜑 → 0 ≤ 𝐴 )
79 eqid ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) )
80 eqid ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) )
81 75 76 78 4 79 80 dvrelog2b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) )
82 dvexp ⊢ ( 𝑁 ∈ ℕ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑁 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ) )
83 8 82 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑁 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ) )
84 oveq1 ⊢ ( 𝑦 = ( 2 logb 𝑥 ) → ( 𝑦 ↑ 𝑁 ) = ( ( 2 logb 𝑥 ) ↑ 𝑁 ) )
85 oveq1 ⊢ ( 𝑦 = ( 2 logb 𝑥 ) → ( 𝑦 ↑ ( 𝑁 − 1 ) ) = ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
86 85 oveq2d ⊢ ( 𝑦 = ( 2 logb 𝑥 ) → ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
87 12 14 56 63 67 74 81 83 84 86 dvmptco ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 logb 𝑥 ) ↑ 𝑁 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) ) )
88 6 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) ) )
89 7 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 = ( 𝑁 / ( ( log ‘ 2 ) ↑ 𝑁 ) ) )
90 89 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( 𝑁 / ( ( log ‘ 2 ) ↑ 𝑁 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) )
91 68 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑁 ∈ ℂ )
92 65 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑁 ∈ ℤ )
94 30 39 93 expclzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ 𝑁 ) ∈ ℂ )
95 71 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑁 − 1 ) ∈ ℕ0 )
96 25 95 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
97 30 39 93 expne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ 𝑁 ) ≠ 0 )
98 91 94 96 17 97 24 divmuldivd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 / ( ( log ‘ 2 ) ↑ 𝑁 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( ( log ‘ 2 ) ↑ 𝑁 ) · 𝑥 ) ) )
99 94 17 mulcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( log ‘ 2 ) ↑ 𝑁 ) · 𝑥 ) = ( 𝑥 · ( ( log ‘ 2 ) ↑ 𝑁 ) ) )
100 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
101 100 68 pncan3d ⊢ ( 𝜑 → ( 1 + ( 𝑁 − 1 ) ) = 𝑁 )
102 101 eqcomd ⊢ ( 𝜑 → 𝑁 = ( 1 + ( 𝑁 − 1 ) ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑁 = ( 1 + ( 𝑁 − 1 ) ) )
104 103 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ 𝑁 ) = ( ( log ‘ 2 ) ↑ ( 1 + ( 𝑁 − 1 ) ) ) )
105 1nn0 ⊢ 1 ∈ ℕ0
106 105 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℕ0 )
107 30 95 106 expaddd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ ( 1 + ( 𝑁 − 1 ) ) ) = ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) )
108 104 107 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ 𝑁 ) = ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) )
109 30 exp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ 1 ) = ( log ‘ 2 ) )
110 109 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) )
111 108 110 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ 𝑁 ) = ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) )
112 111 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 · ( ( log ‘ 2 ) ↑ 𝑁 ) ) = ( 𝑥 · ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) )
113 99 112 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( log ‘ 2 ) ↑ 𝑁 ) · 𝑥 ) = ( 𝑥 · ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) )
114 30 95 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
115 17 30 114 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 · ( log ‘ 2 ) ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) = ( 𝑥 · ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) )
116 115 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 · ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) = ( ( 𝑥 · ( log ‘ 2 ) ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) )
117 113 116 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( log ‘ 2 ) ↑ 𝑁 ) · 𝑥 ) = ( ( 𝑥 · ( log ‘ 2 ) ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) )
118 17 30 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 · ( log ‘ 2 ) ) ∈ ℂ )
119 118 114 mulcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 · ( log ‘ 2 ) ) · ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) · ( 𝑥 · ( log ‘ 2 ) ) ) )
120 117 119 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( log ‘ 2 ) ↑ 𝑁 ) · 𝑥 ) = ( ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) · ( 𝑥 · ( log ‘ 2 ) ) ) )
121 120 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( ( log ‘ 2 ) ↑ 𝑁 ) · 𝑥 ) ) = ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) · ( 𝑥 · ( log ‘ 2 ) ) ) ) )
122 98 121 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 / ( ( log ‘ 2 ) ↑ 𝑁 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) · ( 𝑥 · ( log ‘ 2 ) ) ) ) )
123 90 122 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) · ( 𝑥 · ( log ‘ 2 ) ) ) ) )
124 91 96 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ )
125 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℤ )
126 93 125 zsubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑁 − 1 ) ∈ ℤ )
127 30 39 126 expne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ≠ 0 )
128 124 114 118 127 62 divdiv1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) = ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) · ( 𝑥 · ( log ‘ 2 ) ) ) ) )
129 128 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) · ( 𝑥 · ( log ‘ 2 ) ) ) ) = ( ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
130 123 129 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
131 91 96 114 127 divassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) )
132 131 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝑁 · ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) = ( ( 𝑁 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
133 130 132 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( 𝑁 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
134 25 30 39 95 expdivd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) = ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) )
135 134 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) )
136 135 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑁 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) ) )
137 136 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / ( ( log ‘ 2 ) ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) = ( ( 𝑁 · ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
138 133 137 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( 𝑁 · ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
139 54 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) = ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) )
140 139 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) ) )
141 140 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) = ( ( 𝑁 · ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
142 141 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 · ( ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) = ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
143 138 142 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) )
144 56 95 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
145 91 144 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ )
146 145 118 62 divrecd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) / ( 𝑥 · ( log ‘ 2 ) ) ) = ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) )
147 143 146 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) = ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) )
148 147 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) ) )
149 88 148 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) ) )
150 149 eqcomd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 · ( ( 2 logb 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) ) = 𝐺 )
151 87 150 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 logb 𝑥 ) ↑ 𝑁 ) ) ) = 𝐺 )
152 10 151 eqtrd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )