Step | Hyp | Ref
| Expression |
1 | | rpre 12988 |
. . . . . . 7
โข (๐ด โ โ+
โ ๐ด โ
โ) |
2 | | flge1nn 13792 |
. . . . . . 7
โข ((๐ด โ โ โง 1 โค
๐ด) โ
(โโ๐ด) โ
โ) |
3 | 1, 2 | sylan 579 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ) |
4 | 3 | nnnn0d 12536 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ0) |
5 | 4 | faccld 14249 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(!โ(โโ๐ด))
โ โ) |
6 | 5 | nnrpd 13020 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(!โ(โโ๐ด))
โ โ+) |
7 | 6 | relogcld 26512 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โ โ) |
8 | 1 | adantr 480 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ) |
9 | | reflcl 13767 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
10 | 8, 9 | syl 17 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ) |
11 | 3 | nnrpd 13020 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ+) |
12 | 11 | relogcld 26512 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(โโ๐ด)) โ โ) |
13 | 10, 12 | remulcld 11248 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด) ยท
(logโ(โโ๐ด))) โ โ) |
14 | | relogcl 26464 |
. . . 4
โข (๐ด โ โ+
โ (logโ๐ด) โ
โ) |
15 | 14 | adantr 480 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ๐ด) โ
โ) |
16 | 8, 15 | remulcld 11248 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(๐ด ยท
(logโ๐ด)) โ
โ) |
17 | | facubnd 14265 |
. . . . 5
โข
((โโ๐ด)
โ โ0 โ (!โ(โโ๐ด)) โค ((โโ๐ด)โ(โโ๐ด))) |
18 | 4, 17 | syl 17 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(!โ(โโ๐ด))
โค ((โโ๐ด)โ(โโ๐ด))) |
19 | 3, 4 | nnexpcld 14213 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด)โ(โโ๐ด)) โ โ) |
20 | 19 | nnrpd 13020 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด)โ(โโ๐ด)) โ
โ+) |
21 | 6, 20 | logled 26516 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((!โ(โโ๐ด)) โค ((โโ๐ด)โ(โโ๐ด)) โ
(logโ(!โ(โโ๐ด))) โค (logโ((โโ๐ด)โ(โโ๐ด))))) |
22 | 18, 21 | mpbid 231 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โค (logโ((โโ๐ด)โ(โโ๐ด)))) |
23 | 3 | nnzd 12589 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โค) |
24 | | relogexp 26485 |
. . . 4
โข
(((โโ๐ด)
โ โ+ โง (โโ๐ด) โ โค) โ
(logโ((โโ๐ด)โ(โโ๐ด))) = ((โโ๐ด) ยท (logโ(โโ๐ด)))) |
25 | 11, 23, 24 | syl2anc 583 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ((โโ๐ด)โ(โโ๐ด))) = ((โโ๐ด) ยท (logโ(โโ๐ด)))) |
26 | 22, 25 | breqtrd 5167 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โค ((โโ๐ด) ยท (logโ(โโ๐ด)))) |
27 | | flle 13770 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โค
๐ด) |
28 | 8, 27 | syl 17 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โค
๐ด) |
29 | | simpl 482 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ+) |
30 | 11, 29 | logled 26516 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด) โค
๐ด โ
(logโ(โโ๐ด)) โค (logโ๐ด))) |
31 | 28, 30 | mpbid 231 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(โโ๐ด)) โค (logโ๐ด)) |
32 | 11 | rprege0d 13029 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด) โ
โ โง 0 โค (โโ๐ด))) |
33 | | log1 26474 |
. . . . . 6
โข
(logโ1) = 0 |
34 | 3 | nnge1d 12264 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โค (โโ๐ด)) |
35 | | 1rp 12984 |
. . . . . . . 8
โข 1 โ
โ+ |
36 | | logleb 26492 |
. . . . . . . 8
โข ((1
โ โ+ โง (โโ๐ด) โ โ+) โ (1 โค
(โโ๐ด) โ
(logโ1) โค (logโ(โโ๐ด)))) |
37 | 35, 11, 36 | sylancr 586 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ (1
โค (โโ๐ด)
โ (logโ1) โค (logโ(โโ๐ด)))) |
38 | 34, 37 | mpbid 231 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ1) โค (logโ(โโ๐ด))) |
39 | 33, 38 | eqbrtrrid 5177 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 0
โค (logโ(โโ๐ด))) |
40 | 12, 39 | jca 511 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((logโ(โโ๐ด)) โ โ โง 0 โค
(logโ(โโ๐ด)))) |
41 | | lemul12a 12076 |
. . . 4
โข
(((((โโ๐ด) โ โ โง 0 โค
(โโ๐ด)) โง
๐ด โ โ) โง
(((logโ(โโ๐ด)) โ โ โง 0 โค
(logโ(โโ๐ด))) โง (logโ๐ด) โ โ)) โ
(((โโ๐ด) โค
๐ด โง
(logโ(โโ๐ด)) โค (logโ๐ด)) โ ((โโ๐ด) ยท (logโ(โโ๐ด))) โค (๐ด ยท (logโ๐ด)))) |
42 | 32, 8, 40, 15, 41 | syl22anc 836 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(((โโ๐ด) โค
๐ด โง
(logโ(โโ๐ด)) โค (logโ๐ด)) โ ((โโ๐ด) ยท (logโ(โโ๐ด))) โค (๐ด ยท (logโ๐ด)))) |
43 | 28, 31, 42 | mp2and 696 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด) ยท
(logโ(โโ๐ด))) โค (๐ด ยท (logโ๐ด))) |
44 | 7, 13, 16, 26, 43 | letrd 11375 |
1
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โค (๐ด ยท (logโ๐ด))) |