Step | Hyp | Ref
| Expression |
1 | | logbval 26260 |
. . 3
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (๐ต
logb ๐) =
((logโ๐) /
(logโ๐ต))) |
2 | 1 | oveq2d 7421 |
. 2
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (๐ตโ๐(๐ต logb ๐)) = (๐ตโ๐((logโ๐) / (logโ๐ต)))) |
3 | | eldifi 4125 |
. . . 4
โข (๐ต โ (โ โ {0, 1})
โ ๐ต โ
โ) |
4 | 3 | adantr 481 |
. . 3
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ ๐ต
โ โ) |
5 | | eldif 3957 |
. . . . 5
โข (๐ต โ (โ โ {0, 1})
โ (๐ต โ โ
โง ยฌ ๐ต โ {0,
1})) |
6 | | c0ex 11204 |
. . . . . . . . 9
โข 0 โ
V |
7 | 6 | prid1 4765 |
. . . . . . . 8
โข 0 โ
{0, 1} |
8 | | eleq1 2821 |
. . . . . . . 8
โข (๐ต = 0 โ (๐ต โ {0, 1} โ 0 โ {0,
1})) |
9 | 7, 8 | mpbiri 257 |
. . . . . . 7
โข (๐ต = 0 โ ๐ต โ {0, 1}) |
10 | 9 | necon3bi 2967 |
. . . . . 6
โข (ยฌ
๐ต โ {0, 1} โ
๐ต โ 0) |
11 | 10 | adantl 482 |
. . . . 5
โข ((๐ต โ โ โง ยฌ
๐ต โ {0, 1}) โ
๐ต โ 0) |
12 | 5, 11 | sylbi 216 |
. . . 4
โข (๐ต โ (โ โ {0, 1})
โ ๐ต โ
0) |
13 | 12 | adantr 481 |
. . 3
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ ๐ต โ
0) |
14 | | eldif 3957 |
. . . . . . 7
โข (๐ โ (โ โ {0})
โ (๐ โ โ
โง ยฌ ๐ โ
{0})) |
15 | 6 | snid 4663 |
. . . . . . . . . 10
โข 0 โ
{0} |
16 | | eleq1 2821 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ โ {0} โ 0 โ
{0})) |
17 | 15, 16 | mpbiri 257 |
. . . . . . . . 9
โข (๐ = 0 โ ๐ โ {0}) |
18 | 17 | necon3bi 2967 |
. . . . . . . 8
โข (ยฌ
๐ โ {0} โ ๐ โ 0) |
19 | 18 | anim2i 617 |
. . . . . . 7
โข ((๐ โ โ โง ยฌ
๐ โ {0}) โ (๐ โ โ โง ๐ โ 0)) |
20 | 14, 19 | sylbi 216 |
. . . . . 6
โข (๐ โ (โ โ {0})
โ (๐ โ โ
โง ๐ โ
0)) |
21 | | logcl 26068 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ 0) โ (logโ๐) โ
โ) |
22 | 20, 21 | syl 17 |
. . . . 5
โข (๐ โ (โ โ {0})
โ (logโ๐) โ
โ) |
23 | 22 | adantl 482 |
. . . 4
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (logโ๐) โ โ) |
24 | 10 | anim2i 617 |
. . . . . . 7
โข ((๐ต โ โ โง ยฌ
๐ต โ {0, 1}) โ
(๐ต โ โ โง
๐ต โ 0)) |
25 | 5, 24 | sylbi 216 |
. . . . . 6
โข (๐ต โ (โ โ {0, 1})
โ (๐ต โ โ
โง ๐ต โ
0)) |
26 | | logcl 26068 |
. . . . . 6
โข ((๐ต โ โ โง ๐ต โ 0) โ (logโ๐ต) โ
โ) |
27 | 25, 26 | syl 17 |
. . . . 5
โข (๐ต โ (โ โ {0, 1})
โ (logโ๐ต) โ
โ) |
28 | 27 | adantr 481 |
. . . 4
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (logโ๐ต) โ โ) |
29 | | eldifpr 4659 |
. . . . . . 7
โข (๐ต โ (โ โ {0, 1})
โ (๐ต โ โ
โง ๐ต โ 0 โง ๐ต โ 1)) |
30 | 29 | biimpi 215 |
. . . . . 6
โข (๐ต โ (โ โ {0, 1})
โ (๐ต โ โ
โง ๐ต โ 0 โง ๐ต โ 1)) |
31 | 30 | adantr 481 |
. . . . 5
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (๐ต
โ โ โง ๐ต โ
0 โง ๐ต โ
1)) |
32 | | logccne0 26078 |
. . . . 5
โข ((๐ต โ โ โง ๐ต โ 0 โง ๐ต โ 1) โ (logโ๐ต) โ 0) |
33 | 31, 32 | syl 17 |
. . . 4
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (logโ๐ต) โ 0) |
34 | 23, 28, 33 | divcld 11986 |
. . 3
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ ((logโ๐) / (logโ๐ต)) โ โ) |
35 | 4, 13, 34 | cxpefd 26211 |
. 2
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (๐ตโ๐((logโ๐) / (logโ๐ต))) = (expโ(((logโ๐) / (logโ๐ต)) ยท (logโ๐ต)))) |
36 | | eldifsn 4789 |
. . . . . . 7
โข (๐ โ (โ โ {0})
โ (๐ โ โ
โง ๐ โ
0)) |
37 | 36, 21 | sylbi 216 |
. . . . . 6
โข (๐ โ (โ โ {0})
โ (logโ๐) โ
โ) |
38 | 37 | adantl 482 |
. . . . 5
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (logโ๐) โ โ) |
39 | 29, 32 | sylbi 216 |
. . . . . 6
โข (๐ต โ (โ โ {0, 1})
โ (logโ๐ต) โ
0) |
40 | 39 | adantr 481 |
. . . . 5
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (logโ๐ต) โ 0) |
41 | 38, 28, 40 | divcan1d 11987 |
. . . 4
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (((logโ๐) / (logโ๐ต)) ยท (logโ๐ต)) = (logโ๐)) |
42 | 41 | fveq2d 6892 |
. . 3
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (expโ(((logโ๐) / (logโ๐ต)) ยท (logโ๐ต))) = (expโ(logโ๐))) |
43 | | eflog 26076 |
. . . . 5
โข ((๐ โ โ โง ๐ โ 0) โ
(expโ(logโ๐)) =
๐) |
44 | 36, 43 | sylbi 216 |
. . . 4
โข (๐ โ (โ โ {0})
โ (expโ(logโ๐)) = ๐) |
45 | 44 | adantl 482 |
. . 3
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (expโ(logโ๐)) = ๐) |
46 | 42, 45 | eqtrd 2772 |
. 2
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (expโ(((logโ๐) / (logโ๐ต)) ยท (logโ๐ต))) = ๐) |
47 | 2, 35, 46 | 3eqtrd 2776 |
1
โข ((๐ต โ (โ โ {0, 1})
โง ๐ โ (โ
โ {0})) โ (๐ตโ๐(๐ต logb ๐)) = ๐) |