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 
|- ( ph -> A e. RR )
dvrelogpow2b.2 
|- ( ph -> B e. RR )
dvrelogpow2b.3 
|- ( ph -> 0 < A )
dvrelogpow2b.4 
|- ( ph -> A <_ B )
dvrelogpow2b.5 
|- F = ( x e. ( A (,) B ) |-> ( ( 2 logb x ) ^ N ) )
dvrelogpow2b.6 
|- G = ( x e. ( A (,) B ) |-> ( C x. ( ( ( log ` x ) ^ ( N - 1 ) ) / x ) ) )
dvrelogpow2b.7 
|- C = ( N / ( ( log ` 2 ) ^ N ) )
dvrelogpow2b.8 
|- ( ph -> N e. NN )
Assertion dvrelogpow2b 
|- ( ph -> ( RR _D F ) = G )

Proof

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