Metamath Proof Explorer

Theorem dvrelog2b

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

Ref Expression
Hypotheses dvrelog2b.1 
|- ( ph -> A e. RR* )
dvrelog2b.2 
|- ( ph -> B e. RR* )
dvrelog2b.3 
|- ( ph -> 0 <_ A )
dvrelog2b.4 
|- ( ph -> A <_ B )
dvrelog2b.5 
|- F = ( x e. ( A (,) B ) |-> ( 2 logb x ) )
dvrelog2b.6 
|- G = ( x e. ( A (,) B ) |-> ( 1 / ( x x. ( log ` 2 ) ) ) )
Assertion dvrelog2b 
|- ( ph -> ( RR _D F ) = G )

Proof

Step Hyp Ref Expression
1 dvrelog2b.1 
 |-  ( ph -> A e. RR* )
2 dvrelog2b.2 
 |-  ( ph -> B e. RR* )
3 dvrelog2b.3 
 |-  ( ph -> 0 <_ A )
4 dvrelog2b.4 
 |-  ( ph -> A <_ B )
5 dvrelog2b.5 
 |-  F = ( x e. ( A (,) B ) |-> ( 2 logb x ) )
6 dvrelog2b.6 
 |-  G = ( x e. ( A (,) B ) |-> ( 1 / ( x x. ( log ` 2 ) ) ) )
7 5 a1i 
 |-  ( ph -> F = ( x e. ( A (,) B ) |-> ( 2 logb x ) ) )
8 2cnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 e. CC )
9 2ne0 
 |-  2 =/= 0
10 9 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 =/= 0 )
11 1red 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 e. RR )
12 1lt2 
 |-  1 < 2
13 12 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 < 2 )
14 11 13 ltned 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 1 =/= 2 )
15 14 necomd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 =/= 1 )
16 10 15 nelprd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. 2 e. { 0 , 1 } )
17 8 16 eldifd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 2 e. ( CC \ { 0 , 1 } ) )
18 elioore 
 |-  ( x e. ( A (,) B ) -> x e. RR )
19 recn 
 |-  ( x e. RR -> x e. CC )
20 18 19 syl 
 |-  ( x e. ( A (,) B ) -> x e. CC )
21 20 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. CC )
22 elsni 
 |-  ( x e. { 0 } -> x = 0 )
23 0xr 
 |-  0 e. RR*
24 23 a1i 
 |-  ( ph -> 0 e. RR* )
25 xrlenlt 
 |-  ( ( 0 e. RR* /\ A e. RR* ) -> ( 0 <_ A <-> -. A < 0 ) )
26 24 1 25 syl2anc 
 |-  ( ph -> ( 0 <_ A <-> -. A < 0 ) )
27 3 26 mpbid 
 |-  ( ph -> -. A < 0 )
28 27 orcd 
 |-  ( ph -> ( -. A < 0 \/ -. 0 < B ) )
29 ianor 
 |-  ( -. ( A < 0 /\ 0 < B ) <-> ( -. A < 0 \/ -. 0 < B ) )
30 28 29 sylibr 
 |-  ( ph -> -. ( A < 0 /\ 0 < B ) )
31 elioo5 
 |-  ( ( A e. RR* /\ B e. RR* /\ 0 e. RR* ) -> ( 0 e. ( A (,) B ) <-> ( A < 0 /\ 0 < B ) ) )
32 1 2 24 31 syl3anc 
 |-  ( ph -> ( 0 e. ( A (,) B ) <-> ( A < 0 /\ 0 < B ) ) )
33 32 notbid 
 |-  ( ph -> ( -. 0 e. ( A (,) B ) <-> -. ( A < 0 /\ 0 < B ) ) )
34 30 33 mpbird 
 |-  ( ph -> -. 0 e. ( A (,) B ) )
35 34 a1d 
 |-  ( ph -> ( 0 e. ( A (,) B ) -> -. 0 e. ( A (,) B ) ) )
36 35 imp 
 |-  ( ( ph /\ 0 e. ( A (,) B ) ) -> -. 0 e. ( A (,) B ) )
37 36 pm2.01da 
 |-  ( ph -> -. 0 e. ( A (,) B ) )
38 37 adantr 
 |-  ( ( ph /\ x = 0 ) -> -. 0 e. ( A (,) B ) )
39 eleq1 
 |-  ( x = 0 -> ( x e. ( A (,) B ) <-> 0 e. ( A (,) B ) ) )
40 39 adantl 
 |-  ( ( ph /\ x = 0 ) -> ( x e. ( A (,) B ) <-> 0 e. ( A (,) B ) ) )
41 38 40 mtbird 
 |-  ( ( ph /\ x = 0 ) -> -. x e. ( A (,) B ) )
42 22 41 sylan2 
 |-  ( ( ph /\ x e. { 0 } ) -> -. x e. ( A (,) B ) )
43 42 ex 
 |-  ( ph -> ( x e. { 0 } -> -. x e. ( A (,) B ) ) )
44 43 con2d 
 |-  ( ph -> ( x e. ( A (,) B ) -> -. x e. { 0 } ) )
45 44 imp 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. x e. { 0 } )
46 21 45 eldifd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( CC \ { 0 } ) )
47 logbval 
 |-  ( ( 2 e. ( CC \ { 0 , 1 } ) /\ x e. ( CC \ { 0 } ) ) -> ( 2 logb x ) = ( ( log ` x ) / ( log ` 2 ) ) )
48 17 46 47 syl2anc 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 2 logb x ) = ( ( log ` x ) / ( log ` 2 ) ) )
49 48 mpteq2dva 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( 2 logb x ) ) = ( x e. ( A (,) B ) |-> ( ( log ` x ) / ( log ` 2 ) ) ) )
50 7 49 eqtrd 
 |-  ( ph -> F = ( x e. ( A (,) B ) |-> ( ( log ` x ) / ( log ` 2 ) ) ) )
51 50 oveq2d 
 |-  ( ph -> ( RR _D F ) = ( RR _D ( x e. ( A (,) B ) |-> ( ( log ` x ) / ( log ` 2 ) ) ) ) )
52 reelprrecn 
 |-  RR e. { RR , CC }
53 52 a1i 
 |-  ( ph -> RR e. { RR , CC } )
54 41 ex 
 |-  ( ph -> ( x = 0 -> -. x e. ( A (,) B ) ) )
55 54 con2d 
 |-  ( ph -> ( x e. ( A (,) B ) -> -. x = 0 ) )
56 biidd 
 |-  ( x e. ( A (,) B ) -> ( x = 0 <-> x = 0 ) )
57 56 necon3bbid 
 |-  ( x e. ( A (,) B ) -> ( -. x = 0 <-> x =/= 0 ) )
58 57 pm5.74i 
 |-  ( ( x e. ( A (,) B ) -> -. x = 0 ) <-> ( x e. ( A (,) B ) -> x =/= 0 ) )
59 55 58 sylib 
 |-  ( ph -> ( x e. ( A (,) B ) -> x =/= 0 ) )
60 59 imp 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x =/= 0 )
61 21 60 logcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( log ` x ) e. CC )
62 18 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. RR )
63 11 62 60 redivcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( 1 / x ) e. RR )
64 eqid 
 |-  ( x e. ( A (,) B ) |-> ( log ` x ) ) = ( x e. ( A (,) B ) |-> ( log ` x ) )
65 eqid 
 |-  ( x e. ( A (,) B ) |-> ( 1 / x ) ) = ( x e. ( A (,) B ) |-> ( 1 / x ) )
66 1 2 3 4 64 65 dvrelog3 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( log ` x ) ) ) = ( x e. ( A (,) B ) |-> ( 1 / x ) ) )
67 2cnd 
 |-  ( ph -> 2 e. CC )
68 9 a1i 
 |-  ( ph -> 2 =/= 0 )
69 67 68 logcld 
 |-  ( ph -> ( log ` 2 ) e. CC )
70 0red 
 |-  ( ph -> 0 e. RR )
71 2rp 
 |-  2 e. RR+
72 loggt0b 
 |-  ( 2 e. RR+ -> ( 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 
 |-  ( ph -> 0 < ( log ` 2 ) )
76 70 75 ltned 
 |-  ( ph -> 0 =/= ( log ` 2 ) )
77 76 necomd 
 |-  ( ph -> ( log ` 2 ) =/= 0 )
78 53 61 63 66 69 77 dvmptdivc 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( ( log ` x ) / ( log ` 2 ) ) ) ) = ( x e. ( A (,) B ) |-> ( ( 1 / x ) / ( log ` 2 ) ) ) )
79 8 10 logcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( log ` 2 ) e. CC )
80 77 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( log ` 2 ) =/= 0 )
81 21 79 60 80 recdiv2d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( 1 / x ) / ( log ` 2 ) ) = ( 1 / ( x x. ( log ` 2 ) ) ) )
82 81 mpteq2dva 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( 1 / x ) / ( log ` 2 ) ) ) = ( x e. ( A (,) B ) |-> ( 1 / ( x x. ( log ` 2 ) ) ) ) )
83 6 a1i 
 |-  ( ph -> G = ( x e. ( A (,) B ) |-> ( 1 / ( x x. ( log ` 2 ) ) ) ) )
84 83 eqcomd 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( 1 / ( x x. ( log ` 2 ) ) ) ) = G )
85 82 84 eqtrd 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( 1 / x ) / ( log ` 2 ) ) ) = G )
86 78 85 eqtrd 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( ( log ` x ) / ( log ` 2 ) ) ) ) = G )
87 51 86 eqtrd 
 |-  ( ph -> ( RR _D F ) = G )