Metamath Proof Explorer

Theorem aks4d1p1p6

Description: Inequality lift to differentiable functions for a term in AKS inequality lemma. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p6.1 
|- ( ph -> A e. RR )
aks4d1p1p6.2 
|- ( ph -> B e. RR )
aks4d1p1p6.3 
|- ( ph -> 3 <_ A )
aks4d1p1p6.4 
|- ( ph -> A <_ B )
Assertion aks4d1p1p6 
|- ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) ) = ( x e. ( A (,) B ) |-> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p6.1 
 |-  ( ph -> A e. RR )
2 aks4d1p1p6.2 
 |-  ( ph -> B e. RR )
3 aks4d1p1p6.3 
 |-  ( ph -> 3 <_ A )
4 aks4d1p1p6.4 
 |-  ( ph -> A <_ B )
5 reelprrecn 
 |-  RR e. { RR , CC }
6 5 a1i 
 |-  ( ph -> RR e. { RR , CC } )
7 2cnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 e. CC )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 e. RR )
10 2pos 
 |-  0 < 2
11 10 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < 2 )
12 elioore 
 |-  ( x e. ( A (,) B ) -> x e. RR )
13 12 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. RR )
14 0red 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 e. RR )
15 1 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A e. RR )
16 3re 
 |-  3 e. RR
17 16 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 3 e. RR )
18 3pos 
 |-  0 < 3
19 18 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < 3 )
20 3 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 3 <_ A )
21 14 17 15 19 20 ltletrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < A )
22 simpr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
23 1 rexrd 
 |-  ( ph -> A e. RR* )
24 23 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A e. RR* )
25 2 rexrd 
 |-  ( ph -> B e. RR* )
26 25 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> B e. RR* )
27 13 rexrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. RR* )
28 elioo5 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. RR* ) -> ( x e. ( A (,) B ) <-> ( A < x /\ x < B ) ) )
29 24 26 27 28 syl3anc 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( x e. ( A (,) B ) <-> ( A < x /\ x < B ) ) )
30 22 29 mpbid 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( A < x /\ x < B ) )
31 30 simpld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A < x )
32 14 15 13 21 31 lttrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < x )
33 1red 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 e. RR )
34 1lt2 
 |-  1 < 2
35 34 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 < 2 )
36 33 35 ltned 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 =/= 2 )
37 36 necomd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 =/= 1 )
38 9 11 13 32 37 relogbcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 logb x ) e. RR )
39 5nn0 
 |-  5 e. NN0
40 39 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 5 e. NN0 )
41 38 40 reexpcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( 2 logb x ) ^ 5 ) e. RR )
42 41 33 readdcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) e. RR )
43 14 33 readdcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 0 + 1 ) e. RR )
44 14 ltp1d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < ( 0 + 1 ) )
45 40 nn0zd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 5 e. ZZ )
46 2cnd 
 |-  ( T. -> 2 e. CC )
47 0red 
 |-  ( T. -> 0 e. RR )
48 10 a1i 
 |-  ( T. -> 0 < 2 )
49 47 48 ltned 
 |-  ( T. -> 0 =/= 2 )
50 49 necomd 
 |-  ( T. -> 2 =/= 0 )
51 1red 
 |-  ( T. -> 1 e. RR )
52 34 a1i 
 |-  ( T. -> 1 < 2 )
53 51 52 ltned 
 |-  ( T. -> 1 =/= 2 )
54 53 necomd 
 |-  ( T. -> 2 =/= 1 )
55 logb1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
56 46 50 54 55 syl3anc 
 |-  ( T. -> ( 2 logb 1 ) = 0 )
57 56 mptru 
 |-  ( 2 logb 1 ) = 0
58 2lt3 
 |-  2 < 3
59 58 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 < 3 )
60 33 9 17 35 59 lttrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 < 3 )
61 33 17 15 60 20 ltletrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 < A )
62 33 15 13 61 31 lttrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 < x )
63 2z 
 |-  2 e. ZZ
64 63 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 e. ZZ )
65 64 uzidd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 e. ( ZZ>= ` 2 ) )
66 1rp 
 |-  1 e. RR+
67 66 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 e. RR+ )
68 13 32 elrpd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. RR+ )
69 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ 1 e. RR+ /\ x e. RR+ ) -> ( 1 < x <-> ( 2 logb 1 ) < ( 2 logb x ) ) )
70 65 67 68 69 syl3anc 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 1 < x <-> ( 2 logb 1 ) < ( 2 logb x ) ) )
71 62 70 mpbid 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 logb 1 ) < ( 2 logb x ) )
72 57 71 eqbrtrrid 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < ( 2 logb x ) )
73 expgt0 
 |-  ( ( ( 2 logb x ) e. RR /\ 5 e. ZZ /\ 0 < ( 2 logb x ) ) -> 0 < ( ( 2 logb x ) ^ 5 ) )
74 38 45 72 73 syl3anc 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < ( ( 2 logb x ) ^ 5 ) )
75 14 41 33 74 ltadd1dd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 0 + 1 ) < ( ( ( 2 logb x ) ^ 5 ) + 1 ) )
76 14 43 42 44 75 lttrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < ( ( ( 2 logb x ) ^ 5 ) + 1 ) )
77 9 11 42 76 37 relogbcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) e. RR )
78 recn 
 |-  ( ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) e. RR -> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) e. CC )
79 77 78 syl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) e. CC )
80 7 79 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) e. CC )
81 2rp 
 |-  2 e. RR+
82 81 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 e. RR+ )
83 82 relogcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( log ` 2 ) e. RR )
84 42 83 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) e. RR )
85 41 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( 2 logb x ) ^ 5 ) e. CC )
86 1cnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 e. CC )
87 85 86 addcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) e. CC )
88 11 gt0ne0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 =/= 0 )
89 7 88 logcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( log ` 2 ) e. CC )
90 76 gt0ne0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) =/= 0 )
91 0red 
 |-  ( ph -> 0 e. RR )
92 loggt0b 
 |-  ( 2 e. RR+ -> ( 0 < ( log ` 2 ) <-> 1 < 2 ) )
93 81 92 ax-mp 
 |-  ( 0 < ( log ` 2 ) <-> 1 < 2 )
94 34 93 mpbir 
 |-  0 < ( log ` 2 )
95 94 a1i 
 |-  ( ph -> 0 < ( log ` 2 ) )
96 91 95 ltned 
 |-  ( ph -> 0 =/= ( log ` 2 ) )
97 96 necomd 
 |-  ( ph -> ( log ` 2 ) =/= 0 )
98 97 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( log ` 2 ) =/= 0 )
99 87 89 90 98 mulne0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) =/= 0 )
100 33 84 99 redivcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) e. RR )
101 5re 
 |-  5 e. RR
102 101 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 5 e. RR )
103 4nn0 
 |-  4 e. NN0
104 103 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 4 e. NN0 )
105 38 104 reexpcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( 2 logb x ) ^ 4 ) e. RR )
106 102 105 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 5 x. ( ( 2 logb x ) ^ 4 ) ) e. RR )
107 13 83 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( x x. ( log ` 2 ) ) e. RR )
108 13 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. CC )
109 14 32 gtned 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x =/= 0 )
110 108 89 109 98 mulne0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( x x. ( log ` 2 ) ) =/= 0 )
111 33 107 110 redivcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 1 / ( x x. ( log ` 2 ) ) ) e. RR )
112 106 111 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) e. RR )
113 112 14 readdcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) e. RR )
114 100 113 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) e. RR )
115 9 114 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) e. RR )
116 42 76 elrpd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) e. RR+ )
117 8 a1i 
 |-  ( ( ph /\ y e. RR+ ) -> 2 e. RR )
118 10 a1i 
 |-  ( ( ph /\ y e. RR+ ) -> 0 < 2 )
119 rpre 
 |-  ( y e. RR+ -> y e. RR )
120 119 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR )
121 rpgt0 
 |-  ( y e. RR+ -> 0 < y )
122 121 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> 0 < y )
123 1red 
 |-  ( ( ph /\ y e. RR+ ) -> 1 e. RR )
124 34 a1i 
 |-  ( ( ph /\ y e. RR+ ) -> 1 < 2 )
125 123 124 ltned 
 |-  ( ( ph /\ y e. RR+ ) -> 1 =/= 2 )
126 125 necomd 
 |-  ( ( ph /\ y e. RR+ ) -> 2 =/= 1 )
127 117 118 120 122 126 relogbcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( 2 logb y ) e. RR )
128 127 recnd 
 |-  ( ( ph /\ y e. RR+ ) -> ( 2 logb y ) e. CC )
129 81 a1i 
 |-  ( ( ph /\ y e. RR+ ) -> 2 e. RR+ )
130 129 relogcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( log ` 2 ) e. RR )
131 120 130 remulcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( y x. ( log ` 2 ) ) e. RR )
132 120 recnd 
 |-  ( ( ph /\ y e. RR+ ) -> y e. CC )
133 2cnd 
 |-  ( ( ph /\ y e. RR+ ) -> 2 e. CC )
134 129 rpne0d 
 |-  ( ( ph /\ y e. RR+ ) -> 2 =/= 0 )
135 133 134 logcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( log ` 2 ) e. CC )
136 rpne0 
 |-  ( y e. RR+ -> y =/= 0 )
137 136 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> y =/= 0 )
138 97 necomd 
 |-  ( ph -> 0 =/= ( log ` 2 ) )
139 138 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> 0 =/= ( log ` 2 ) )
140 139 necomd 
 |-  ( ( ph /\ y e. RR+ ) -> ( log ` 2 ) =/= 0 )
141 132 135 137 140 mulne0d 
 |-  ( ( ph /\ y e. RR+ ) -> ( y x. ( log ` 2 ) ) =/= 0 )
142 123 131 141 redivcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( 1 / ( y x. ( log ` 2 ) ) ) e. RR )
143 cnelprrecn 
 |-  CC e. { RR , CC }
144 143 a1i 
 |-  ( ph -> CC e. { RR , CC } )
145 38 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 logb x ) e. CC )
146 simpr 
 |-  ( ( ph /\ z e. CC ) -> z e. CC )
147 39 a1i 
 |-  ( ( ph /\ z e. CC ) -> 5 e. NN0 )
148 146 147 expcld 
 |-  ( ( ph /\ z e. CC ) -> ( z ^ 5 ) e. CC )
149 5cn 
 |-  5 e. CC
150 149 a1i 
 |-  ( ( ph /\ z e. CC ) -> 5 e. CC )
151 103 a1i 
 |-  ( ( ph /\ z e. CC ) -> 4 e. NN0 )
152 146 151 expcld 
 |-  ( ( ph /\ z e. CC ) -> ( z ^ 4 ) e. CC )
153 150 152 mulcld 
 |-  ( ( ph /\ z e. CC ) -> ( 5 x. ( z ^ 4 ) ) e. CC )
154 16 a1i 
 |-  ( ph -> 3 e. RR )
155 18 a1i 
 |-  ( ph -> 0 < 3 )
156 91 154 1 155 3 ltletrd 
 |-  ( ph -> 0 < A )
157 91 1 156 ltled 
 |-  ( ph -> 0 <_ A )
158 eqid 
 |-  ( x e. ( A (,) B ) |-> ( 2 logb x ) ) = ( x e. ( A (,) B ) |-> ( 2 logb x ) )
159 eqid 
 |-  ( x e. ( A (,) B ) |-> ( 1 / ( x x. ( log ` 2 ) ) ) ) = ( x e. ( A (,) B ) |-> ( 1 / ( x x. ( log ` 2 ) ) ) )
160 23 25 157 4 158 159 dvrelog2b 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( 2 logb x ) ) ) = ( x e. ( A (,) B ) |-> ( 1 / ( x x. ( log ` 2 ) ) ) ) )
161 5nn 
 |-  5 e. NN
162 dvexp 
 |-  ( 5 e. NN -> ( CC _D ( z e. CC |-> ( z ^ 5 ) ) ) = ( z e. CC |-> ( 5 x. ( z ^ ( 5 - 1 ) ) ) ) )
163 161 162 ax-mp 
 |-  ( CC _D ( z e. CC |-> ( z ^ 5 ) ) ) = ( z e. CC |-> ( 5 x. ( z ^ ( 5 - 1 ) ) ) )
164 5m1e4 
 |-  ( 5 - 1 ) = 4
165 164 a1i 
 |-  ( ( ph /\ z e. CC ) -> ( 5 - 1 ) = 4 )
166 165 oveq2d 
 |-  ( ( ph /\ z e. CC ) -> ( z ^ ( 5 - 1 ) ) = ( z ^ 4 ) )
167 166 oveq2d 
 |-  ( ( ph /\ z e. CC ) -> ( 5 x. ( z ^ ( 5 - 1 ) ) ) = ( 5 x. ( z ^ 4 ) ) )
168 167 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> ( 5 x. ( z ^ ( 5 - 1 ) ) ) ) = ( z e. CC |-> ( 5 x. ( z ^ 4 ) ) ) )
169 163 168 eqtrid 
 |-  ( ph -> ( CC _D ( z e. CC |-> ( z ^ 5 ) ) ) = ( z e. CC |-> ( 5 x. ( z ^ 4 ) ) ) )
170 oveq1 
 |-  ( z = ( 2 logb x ) -> ( z ^ 5 ) = ( ( 2 logb x ) ^ 5 ) )
171 oveq1 
 |-  ( z = ( 2 logb x ) -> ( z ^ 4 ) = ( ( 2 logb x ) ^ 4 ) )
172 171 oveq2d 
 |-  ( z = ( 2 logb x ) -> ( 5 x. ( z ^ 4 ) ) = ( 5 x. ( ( 2 logb x ) ^ 4 ) ) )
173 6 144 145 111 148 153 160 169 170 172 dvmptco 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( ( 2 logb x ) ^ 5 ) ) ) = ( x e. ( A (,) B ) |-> ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) ) )
174 1cnd 
 |-  ( ph -> 1 e. CC )
175 174 adantr 
 |-  ( ( ph /\ x e. RR ) -> 1 e. CC )
176 0red 
 |-  ( ( ph /\ x e. RR ) -> 0 e. RR )
177 6 174 dvmptc 
 |-  ( ph -> ( RR _D ( x e. RR |-> 1 ) ) = ( x e. RR |-> 0 ) )
178 ioossre 
 |-  ( A (,) B ) C_ RR
179 178 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
180 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
181 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
182 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
183 182 a1i 
 |-  ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
184 6 175 176 177 179 180 181 183 dvmptres 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> 1 ) ) = ( x e. ( A (,) B ) |-> 0 ) )
185 6 85 112 173 86 14 184 dvmptadd 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) = ( x e. ( A (,) B ) |-> ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) )
186 dfrp2 
 |-  RR+ = ( 0 (,) +oo )
187 186 a1i 
 |-  ( ph -> RR+ = ( 0 (,) +oo ) )
188 187 mpteq1d 
 |-  ( ph -> ( y e. RR+ |-> ( 2 logb y ) ) = ( y e. ( 0 (,) +oo ) |-> ( 2 logb y ) ) )
189 188 oveq2d 
 |-  ( ph -> ( RR _D ( y e. RR+ |-> ( 2 logb y ) ) ) = ( RR _D ( y e. ( 0 (,) +oo ) |-> ( 2 logb y ) ) ) )
190 91 rexrd 
 |-  ( ph -> 0 e. RR* )
191 pnfxr 
 |-  +oo e. RR*
192 191 a1i 
 |-  ( ph -> +oo e. RR* )
193 91 leidd 
 |-  ( ph -> 0 <_ 0 )
194 0lepnf 
 |-  0 <_ +oo
195 194 a1i 
 |-  ( ph -> 0 <_ +oo )
196 eqid 
 |-  ( y e. ( 0 (,) +oo ) |-> ( 2 logb y ) ) = ( y e. ( 0 (,) +oo ) |-> ( 2 logb y ) )
197 eqid 
 |-  ( y e. ( 0 (,) +oo ) |-> ( 1 / ( y x. ( log ` 2 ) ) ) ) = ( y e. ( 0 (,) +oo ) |-> ( 1 / ( y x. ( log ` 2 ) ) ) )
198 190 192 193 195 196 197 dvrelog2b 
 |-  ( ph -> ( RR _D ( y e. ( 0 (,) +oo ) |-> ( 2 logb y ) ) ) = ( y e. ( 0 (,) +oo ) |-> ( 1 / ( y x. ( log ` 2 ) ) ) ) )
199 187 eqcomd 
 |-  ( ph -> ( 0 (,) +oo ) = RR+ )
200 199 mpteq1d 
 |-  ( ph -> ( y e. ( 0 (,) +oo ) |-> ( 1 / ( y x. ( log ` 2 ) ) ) ) = ( y e. RR+ |-> ( 1 / ( y x. ( log ` 2 ) ) ) ) )
201 198 200 eqtrd 
 |-  ( ph -> ( RR _D ( y e. ( 0 (,) +oo ) |-> ( 2 logb y ) ) ) = ( y e. RR+ |-> ( 1 / ( y x. ( log ` 2 ) ) ) ) )
202 189 201 eqtrd 
 |-  ( ph -> ( RR _D ( y e. RR+ |-> ( 2 logb y ) ) ) = ( y e. RR+ |-> ( 1 / ( y x. ( log ` 2 ) ) ) ) )
203 oveq2 
 |-  ( y = ( ( ( 2 logb x ) ^ 5 ) + 1 ) -> ( 2 logb y ) = ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) )
204 oveq1 
 |-  ( y = ( ( ( 2 logb x ) ^ 5 ) + 1 ) -> ( y x. ( log ` 2 ) ) = ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) )
205 204 oveq2d 
 |-  ( y = ( ( ( 2 logb x ) ^ 5 ) + 1 ) -> ( 1 / ( y x. ( log ` 2 ) ) ) = ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) )
206 6 6 116 113 128 142 185 202 203 205 dvmptco 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) ) = ( x e. ( A (,) B ) |-> ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) )
207 8 a1i 
 |-  ( ph -> 2 e. RR )
208 207 recnd 
 |-  ( ph -> 2 e. CC )
209 6 79 114 206 208 dvmptcmul 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) ) ) = ( x e. ( A (,) B ) |-> ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) ) )
210 145 sqcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( 2 logb x ) ^ 2 ) e. CC )
211 83 resqcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( log ` 2 ) ^ 2 ) e. RR )
212 82 rpne0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 =/= 0 )
213 7 212 logcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( log ` 2 ) e. CC )
214 213 98 64 expne0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( log ` 2 ) ^ 2 ) =/= 0 )
215 9 211 214 redivcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 / ( ( log ` 2 ) ^ 2 ) ) e. RR )
216 68 relogcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( log ` x ) e. RR )
217 2m1e1 
 |-  ( 2 - 1 ) = 1
218 1nn0 
 |-  1 e. NN0
219 217 218 eqeltri 
 |-  ( 2 - 1 ) e. NN0
220 219 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 - 1 ) e. NN0 )
221 216 220 reexpcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( log ` x ) ^ ( 2 - 1 ) ) e. RR )
222 68 rpne0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x =/= 0 )
223 221 13 222 redivcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) e. RR )
224 215 223 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) e. RR )
225 eqid 
 |-  ( x e. ( A (,) B ) |-> ( ( 2 logb x ) ^ 2 ) ) = ( x e. ( A (,) B ) |-> ( ( 2 logb x ) ^ 2 ) )
226 eqid 
 |-  ( x e. ( A (,) B ) |-> ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) = ( x e. ( A (,) B ) |-> ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) )
227 eqid 
 |-  ( 2 / ( ( log ` 2 ) ^ 2 ) ) = ( 2 / ( ( log ` 2 ) ^ 2 ) )
228 2nn 
 |-  2 e. NN
229 228 a1i 
 |-  ( ph -> 2 e. NN )
230 1 2 156 4 225 226 227 229 dvrelogpow2b 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( ( 2 logb x ) ^ 2 ) ) ) = ( x e. ( A (,) B ) |-> ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) )
231 6 80 115 209 210 224 230 dvmptadd 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) ) = ( x e. ( A (,) B ) |-> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) ) )