Metamath Proof Explorer


Theorem dvrelog2b

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

Ref Expression
Hypotheses dvrelog2b.1 φ A *
dvrelog2b.2 φ B *
dvrelog2b.3 φ 0 A
dvrelog2b.4 φ A B
dvrelog2b.5 F = x A B log 2 x
dvrelog2b.6 G = x A B 1 x log 2
Assertion dvrelog2b φ D F = G

Proof

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