Step | Hyp | Ref
| Expression |
1 | | dvrelogpow2b.5 |
. . . 4
โข ๐น = (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ๐)) |
2 | 1 | a1i 11 |
. . 3
โข (๐ โ ๐น = (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ๐))) |
3 | 2 | oveq2d 7374 |
. 2
โข (๐ โ (โ D ๐น) = (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ๐)))) |
4 | | reelprrecn 11148 |
. . . . 5
โข โ
โ {โ, โ} |
5 | 4 | a1i 11 |
. . . 4
โข (๐ โ โ โ {โ,
โ}) |
6 | | cnelprrecn 11149 |
. . . . 5
โข โ
โ {โ, โ} |
7 | 6 | a1i 11 |
. . . 4
โข (๐ โ โ โ {โ,
โ}) |
8 | | elioore 13300 |
. . . . . . . . 9
โข (๐ฅ โ (๐ด(,)๐ต) โ ๐ฅ โ โ) |
9 | 8 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ โ) |
10 | 9 | recnd 11188 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ โ) |
11 | | dvrelogpow2b.1 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
12 | 11 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ด โ โ) |
13 | | dvrelogpow2b.2 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
14 | 13 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ต โ โ) |
15 | | dvrelogpow2b.3 |
. . . . . . . . . 10
โข (๐ โ 0 < ๐ด) |
16 | 15 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < ๐ด) |
17 | | dvrelogpow2b.4 |
. . . . . . . . . 10
โข (๐ โ ๐ด โค ๐ต) |
18 | 17 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ด โค ๐ต) |
19 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ (๐ด(,)๐ต)) |
20 | 12, 14, 16, 18, 19 | 0nonelalab 40570 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 โ ๐ฅ) |
21 | 20 | necomd 2996 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ 0) |
22 | 10, 21 | logcld 25942 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ๐ฅ) โ โ) |
23 | | 2cnd 12236 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ โ) |
24 | | 0ne2 12365 |
. . . . . . . . 9
โข 0 โ
2 |
25 | 24 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 โ 2) |
26 | 25 | necomd 2996 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ 0) |
27 | 23, 26 | logcld 25942 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ2) โ
โ) |
28 | | 0red 11163 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 โ โ) |
29 | | 1lt2 12329 |
. . . . . . . . . 10
โข 1 <
2 |
30 | 29 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 < 2) |
31 | | 2rp 12925 |
. . . . . . . . . 10
โข 2 โ
โ+ |
32 | | loggt0b 26003 |
. . . . . . . . . 10
โข (2 โ
โ+ โ (0 < (logโ2) โ 1 <
2)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . 9
โข (0 <
(logโ2) โ 1 < 2) |
34 | 30, 33 | sylibr 233 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 <
(logโ2)) |
35 | 28, 34 | ltned 11296 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 โ
(logโ2)) |
36 | 35 | necomd 2996 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ2) โ
0) |
37 | 22, 27, 36 | divcld 11936 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ๐ฅ) / (logโ2)) โ
โ) |
38 | | 1red 11161 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 โ โ) |
39 | 38, 30 | ltned 11296 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 โ 2) |
40 | 39 | necomd 2996 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ 1) |
41 | 26, 40 | nelprd 4618 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ยฌ 2 โ {0,
1}) |
42 | 23, 41 | eldifd 3922 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ (โ โ {0,
1})) |
43 | | necom 2994 |
. . . . . . . . . . . 12
โข (0 โ
๐ฅ โ ๐ฅ โ 0) |
44 | 43 | imbi2i 336 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 โ ๐ฅ) โ ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ 0)) |
45 | 20, 44 | mpbi 229 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ 0) |
46 | 45 | neneqd 2945 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ยฌ ๐ฅ = 0) |
47 | | velsn 4603 |
. . . . . . . . 9
โข (๐ฅ โ {0} โ ๐ฅ = 0) |
48 | 46, 47 | sylnibr 329 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ยฌ ๐ฅ โ {0}) |
49 | 10, 48 | eldifd 3922 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ (โ โ
{0})) |
50 | | logbval 26132 |
. . . . . . 7
โข ((2
โ (โ โ {0, 1}) โง ๐ฅ โ (โ โ {0})) โ (2
logb ๐ฅ) =
((logโ๐ฅ) /
(logโ2))) |
51 | 42, 49, 50 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 logb ๐ฅ) = ((logโ๐ฅ) /
(logโ2))) |
52 | 51 | eleq1d 2819 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((2 logb ๐ฅ) โ โ โ
((logโ๐ฅ) /
(logโ2)) โ โ)) |
53 | 37, 52 | mpbird 257 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 logb ๐ฅ) โ
โ) |
54 | 31 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ
โ+) |
55 | 54 | relogcld 25994 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ2) โ
โ) |
56 | 9, 55 | remulcld 11190 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ฅ ยท (logโ2)) โ
โ) |
57 | 54 | rpne0d 12967 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ 0) |
58 | 23, 57 | logcld 25942 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ2) โ
โ) |
59 | 10, 58, 21, 36 | mulne0d 11812 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ฅ ยท (logโ2)) โ
0) |
60 | 38, 56, 59 | redivcld 11988 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (1 / (๐ฅ ยท (logโ2))) โ
โ) |
61 | | simpr 486 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ) โ ๐ฆ โ โ) |
62 | | dvrelogpow2b.8 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
63 | 62 | nnnn0d 12478 |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
64 | 63 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ) โ ๐ โ
โ0) |
65 | 61, 64 | expcld 14057 |
. . . 4
โข ((๐ โง ๐ฆ โ โ) โ (๐ฆโ๐) โ โ) |
66 | 62 | nncnd 12174 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
67 | 66 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ) โ ๐ โ โ) |
68 | | nnm1nn0 12459 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
69 | 62, 68 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ โ 1) โ
โ0) |
70 | 69 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ) โ (๐ โ 1) โ
โ0) |
71 | 61, 70 | expcld 14057 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ) โ (๐ฆโ(๐ โ 1)) โ
โ) |
72 | 67, 71 | mulcld 11180 |
. . . 4
โข ((๐ โง ๐ฆ โ โ) โ (๐ ยท (๐ฆโ(๐ โ 1))) โ
โ) |
73 | 11 | rexrd 11210 |
. . . . 5
โข (๐ โ ๐ด โ
โ*) |
74 | 13 | rexrd 11210 |
. . . . 5
โข (๐ โ ๐ต โ
โ*) |
75 | | 0red 11163 |
. . . . . 6
โข (๐ โ 0 โ
โ) |
76 | 75, 11, 15 | ltled 11308 |
. . . . 5
โข (๐ โ 0 โค ๐ด) |
77 | | eqid 2733 |
. . . . 5
โข (๐ฅ โ (๐ด(,)๐ต) โฆ (2 logb ๐ฅ)) = (๐ฅ โ (๐ด(,)๐ต) โฆ (2 logb ๐ฅ)) |
78 | | eqid 2733 |
. . . . 5
โข (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / (๐ฅ ยท (logโ2)))) = (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / (๐ฅ ยท (logโ2)))) |
79 | 73, 74, 76, 17, 77, 78 | dvrelog2b 40569 |
. . . 4
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ (2 logb ๐ฅ))) = (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / (๐ฅ ยท (logโ2))))) |
80 | | dvexp 25333 |
. . . . 5
โข (๐ โ โ โ (โ
D (๐ฆ โ โ โฆ
(๐ฆโ๐))) = (๐ฆ โ โ โฆ (๐ ยท (๐ฆโ(๐ โ 1))))) |
81 | 62, 80 | syl 17 |
. . . 4
โข (๐ โ (โ D (๐ฆ โ โ โฆ (๐ฆโ๐))) = (๐ฆ โ โ โฆ (๐ ยท (๐ฆโ(๐ โ 1))))) |
82 | | oveq1 7365 |
. . . 4
โข (๐ฆ = (2 logb ๐ฅ) โ (๐ฆโ๐) = ((2 logb ๐ฅ)โ๐)) |
83 | | oveq1 7365 |
. . . . 5
โข (๐ฆ = (2 logb ๐ฅ) โ (๐ฆโ(๐ โ 1)) = ((2 logb ๐ฅ)โ(๐ โ 1))) |
84 | 83 | oveq2d 7374 |
. . . 4
โข (๐ฆ = (2 logb ๐ฅ) โ (๐ ยท (๐ฆโ(๐ โ 1))) = (๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1)))) |
85 | 5, 7, 53, 60, 65, 72, 79, 81, 82, 84 | dvmptco 25352 |
. . 3
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ๐))) = (๐ฅ โ (๐ด(,)๐ต) โฆ ((๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) ยท (1 / (๐ฅ ยท
(logโ2)))))) |
86 | | dvrelogpow2b.6 |
. . . . . 6
โข ๐บ = (๐ฅ โ (๐ด(,)๐ต) โฆ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ))) |
87 | 86 | a1i 11 |
. . . . 5
โข (๐ โ ๐บ = (๐ฅ โ (๐ด(,)๐ต) โฆ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)))) |
88 | | dvrelogpow2b.7 |
. . . . . . . . . . . . . 14
โข ๐ถ = (๐ / ((logโ2)โ๐)) |
89 | 88 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ถ = (๐ / ((logโ2)โ๐))) |
90 | 89 | oveq1d 7373 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = ((๐ / ((logโ2)โ๐)) ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ))) |
91 | 66 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ โ โ) |
92 | 63 | nn0zd 12530 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โค) |
93 | 92 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ โ โค) |
94 | 27, 36, 93 | expclzd 14062 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ๐) โ
โ) |
95 | 69 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ โ 1) โ
โ0) |
96 | 22, 95 | expcld 14057 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ๐ฅ)โ(๐ โ 1)) โ
โ) |
97 | 27, 36, 93 | expne0d 14063 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ๐) โ 0) |
98 | 91, 94, 96, 10, 97, 21 | divmuldivd 11977 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ / ((logโ2)โ๐)) ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = ((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / (((logโ2)โ๐) ยท ๐ฅ))) |
99 | 94, 10 | mulcomd 11181 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((logโ2)โ๐) ยท ๐ฅ) = (๐ฅ ยท ((logโ2)โ๐))) |
100 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ 1 โ
โ) |
101 | 100, 66 | pncan3d 11520 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (1 + (๐ โ 1)) = ๐) |
102 | 101 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ = (1 + (๐ โ 1))) |
103 | 102 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ = (1 + (๐ โ 1))) |
104 | 103 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ๐) = ((logโ2)โ(1 +
(๐ โ
1)))) |
105 | | 1nn0 12434 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 1 โ
โ0 |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 โ
โ0) |
107 | 27, 95, 106 | expaddd 14059 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ(1 + (๐ โ 1))) =
(((logโ2)โ1) ยท ((logโ2)โ(๐ โ 1)))) |
108 | 104, 107 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ๐) = (((logโ2)โ1)
ยท ((logโ2)โ(๐ โ 1)))) |
109 | 27 | exp1d 14052 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ1) =
(logโ2)) |
110 | 109 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((logโ2)โ1) ยท
((logโ2)โ(๐
โ 1))) = ((logโ2) ยท ((logโ2)โ(๐ โ 1)))) |
111 | 108, 110 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ๐) = ((logโ2) ยท
((logโ2)โ(๐
โ 1)))) |
112 | 111 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ฅ ยท ((logโ2)โ๐)) = (๐ฅ ยท ((logโ2) ยท
((logโ2)โ(๐
โ 1))))) |
113 | 99, 112 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((logโ2)โ๐) ยท ๐ฅ) = (๐ฅ ยท ((logโ2) ยท
((logโ2)โ(๐
โ 1))))) |
114 | 27, 95 | expcld 14057 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ(๐ โ 1)) โ
โ) |
115 | 10, 27, 114 | mulassd 11183 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ฅ ยท (logโ2)) ยท
((logโ2)โ(๐
โ 1))) = (๐ฅ ยท
((logโ2) ยท ((logโ2)โ(๐ โ 1))))) |
116 | 115 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ฅ ยท ((logโ2) ยท
((logโ2)โ(๐
โ 1)))) = ((๐ฅ
ยท (logโ2)) ยท ((logโ2)โ(๐ โ 1)))) |
117 | 113, 116 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((logโ2)โ๐) ยท ๐ฅ) = ((๐ฅ ยท (logโ2)) ยท
((logโ2)โ(๐
โ 1)))) |
118 | 10, 27 | mulcld 11180 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ฅ ยท (logโ2)) โ
โ) |
119 | 118, 114 | mulcomd 11181 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ฅ ยท (logโ2)) ยท
((logโ2)โ(๐
โ 1))) = (((logโ2)โ(๐ โ 1)) ยท (๐ฅ ยท (logโ2)))) |
120 | 117, 119 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((logโ2)โ๐) ยท ๐ฅ) = (((logโ2)โ(๐ โ 1)) ยท (๐ฅ ยท (logโ2)))) |
121 | 120 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / (((logโ2)โ๐) ยท ๐ฅ)) = ((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / (((logโ2)โ(๐ โ 1)) ยท (๐ฅ ยท
(logโ2))))) |
122 | 98, 121 | eqtrd 2773 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ / ((logโ2)โ๐)) ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = ((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / (((logโ2)โ(๐ โ 1)) ยท (๐ฅ ยท
(logโ2))))) |
123 | 90, 122 | eqtrd 2773 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = ((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / (((logโ2)โ(๐ โ 1)) ยท (๐ฅ ยท
(logโ2))))) |
124 | 91, 96 | mulcld 11180 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) โ
โ) |
125 | | 1zzd 12539 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 โ โค) |
126 | 93, 125 | zsubcld 12617 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ โ 1) โ โค) |
127 | 27, 36, 126 | expne0d 14063 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ(๐ โ 1)) โ
0) |
128 | 124, 114,
118, 127, 59 | divdiv1d 11967 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / ((logโ2)โ(๐ โ 1))) / (๐ฅ ยท (logโ2))) =
((๐ ยท
((logโ๐ฅ)โ(๐ โ 1))) /
(((logโ2)โ(๐
โ 1)) ยท (๐ฅ
ยท (logโ2))))) |
129 | 128 | eqcomd 2739 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / (((logโ2)โ(๐ โ 1)) ยท (๐ฅ ยท (logโ2)))) =
(((๐ ยท
((logโ๐ฅ)โ(๐ โ 1))) /
((logโ2)โ(๐
โ 1))) / (๐ฅ ยท
(logโ2)))) |
130 | 123, 129 | eqtrd 2773 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = (((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / ((logโ2)โ(๐ โ 1))) / (๐ฅ ยท
(logโ2)))) |
131 | 91, 96, 114, 127 | divassd 11971 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / ((logโ2)โ(๐ โ 1))) = (๐ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ((logโ2)โ(๐ โ 1))))) |
132 | 131 | oveq1d 7373 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((๐ ยท ((logโ๐ฅ)โ(๐ โ 1))) / ((logโ2)โ(๐ โ 1))) / (๐ฅ ยท (logโ2))) =
((๐ ยท
(((logโ๐ฅ)โ(๐ โ 1)) /
((logโ2)โ(๐
โ 1)))) / (๐ฅ ยท
(logโ2)))) |
133 | 130, 132 | eqtrd 2773 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = ((๐ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ((logโ2)โ(๐ โ 1)))) / (๐ฅ ยท
(logโ2)))) |
134 | 22, 27, 36, 95 | expdivd 14071 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((logโ๐ฅ) / (logโ2))โ(๐ โ 1)) = (((logโ๐ฅ)โ(๐ โ 1)) / ((logโ2)โ(๐ โ 1)))) |
135 | 134 | eqcomd 2739 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((logโ๐ฅ)โ(๐ โ 1)) / ((logโ2)โ(๐ โ 1))) =
(((logโ๐ฅ) /
(logโ2))โ(๐
โ 1))) |
136 | 135 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ((logโ2)โ(๐ โ 1)))) = (๐ ยท (((logโ๐ฅ) / (logโ2))โ(๐ โ 1)))) |
137 | 136 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ((logโ2)โ(๐ โ 1)))) / (๐ฅ ยท (logโ2))) =
((๐ ยท
(((logโ๐ฅ) /
(logโ2))โ(๐
โ 1))) / (๐ฅ ยท
(logโ2)))) |
138 | 133, 137 | eqtrd 2773 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = ((๐ ยท (((logโ๐ฅ) / (logโ2))โ(๐ โ 1))) / (๐ฅ ยท (logโ2)))) |
139 | 51 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((2 logb ๐ฅ)โ(๐ โ 1)) = (((logโ๐ฅ) / (logโ2))โ(๐ โ 1))) |
140 | 139 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) = (๐ ยท (((logโ๐ฅ) / (logโ2))โ(๐ โ 1)))) |
141 | 140 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) / (๐ฅ ยท (logโ2))) = ((๐ ยท (((logโ๐ฅ) / (logโ2))โ(๐ โ 1))) / (๐ฅ ยท
(logโ2)))) |
142 | 141 | eqcomd 2739 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ ยท (((logโ๐ฅ) / (logโ2))โ(๐ โ 1))) / (๐ฅ ยท (logโ2))) = ((๐ ยท ((2 logb
๐ฅ)โ(๐ โ 1))) / (๐ฅ ยท (logโ2)))) |
143 | 138, 142 | eqtrd 2773 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = ((๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) / (๐ฅ ยท (logโ2)))) |
144 | 53, 95 | expcld 14057 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((2 logb ๐ฅ)โ(๐ โ 1)) โ
โ) |
145 | 91, 144 | mulcld 11180 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) โ
โ) |
146 | 145, 118,
59 | divrecd 11939 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) / (๐ฅ ยท (logโ2))) = ((๐ ยท ((2 logb
๐ฅ)โ(๐ โ 1))) ยท (1 / (๐ฅ ยท
(logโ2))))) |
147 | 143, 146 | eqtrd 2773 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ)) = ((๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) ยท (1 / (๐ฅ ยท
(logโ2))))) |
148 | 147 | mpteq2dva 5206 |
. . . . 5
โข (๐ โ (๐ฅ โ (๐ด(,)๐ต) โฆ (๐ถ ยท (((logโ๐ฅ)โ(๐ โ 1)) / ๐ฅ))) = (๐ฅ โ (๐ด(,)๐ต) โฆ ((๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) ยท (1 / (๐ฅ ยท
(logโ2)))))) |
149 | 87, 148 | eqtrd 2773 |
. . . 4
โข (๐ โ ๐บ = (๐ฅ โ (๐ด(,)๐ต) โฆ ((๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) ยท (1 / (๐ฅ ยท
(logโ2)))))) |
150 | 149 | eqcomd 2739 |
. . 3
โข (๐ โ (๐ฅ โ (๐ด(,)๐ต) โฆ ((๐ ยท ((2 logb ๐ฅ)โ(๐ โ 1))) ยท (1 / (๐ฅ ยท (logโ2))))) =
๐บ) |
151 | 85, 150 | eqtrd 2773 |
. 2
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ๐))) = ๐บ) |
152 | 3, 151 | eqtrd 2773 |
1
โข (๐ โ (โ D ๐น) = ๐บ) |