Step | Hyp | Ref
| Expression |
1 | | rpre 12978 |
. . . . . . 7
โข (๐ด โ โ+
โ ๐ด โ
โ) |
2 | | flge1nn 13782 |
. . . . . . 7
โข ((๐ด โ โ โง 1 โค
๐ด) โ
(โโ๐ด) โ
โ) |
3 | 1, 2 | sylan 580 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ) |
4 | 3 | nnnn0d 12528 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ0) |
5 | 4 | faccld 14240 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(!โ(โโ๐ด))
โ โ) |
6 | 5 | nnrpd 13010 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(!โ(โโ๐ด))
โ โ+) |
7 | 6 | relogcld 26122 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โ โ) |
8 | 1 | adantr 481 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ) |
9 | | reflcl 13757 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
10 | 8, 9 | syl 17 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ) |
11 | 3 | nnrpd 13010 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ+) |
12 | 11 | relogcld 26122 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(โโ๐ด)) โ โ) |
13 | 10, 12 | remulcld 11240 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด) ยท
(logโ(โโ๐ด))) โ โ) |
14 | | relogcl 26075 |
. . . 4
โข (๐ด โ โ+
โ (logโ๐ด) โ
โ) |
15 | 14 | adantr 481 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ๐ด) โ
โ) |
16 | 8, 15 | remulcld 11240 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(๐ด ยท
(logโ๐ด)) โ
โ) |
17 | | facubnd 14256 |
. . . . 5
โข
((โโ๐ด)
โ โ0 โ (!โ(โโ๐ด)) โค ((โโ๐ด)โ(โโ๐ด))) |
18 | 4, 17 | syl 17 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(!โ(โโ๐ด))
โค ((โโ๐ด)โ(โโ๐ด))) |
19 | 3, 4 | nnexpcld 14204 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด)โ(โโ๐ด)) โ โ) |
20 | 19 | nnrpd 13010 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด)โ(โโ๐ด)) โ
โ+) |
21 | 6, 20 | logled 26126 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((!โ(โโ๐ด)) โค ((โโ๐ด)โ(โโ๐ด)) โ
(logโ(!โ(โโ๐ด))) โค (logโ((โโ๐ด)โ(โโ๐ด))))) |
22 | 18, 21 | mpbid 231 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โค (logโ((โโ๐ด)โ(โโ๐ด)))) |
23 | 3 | nnzd 12581 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โค) |
24 | | relogexp 26095 |
. . . 4
โข
(((โโ๐ด)
โ โ+ โง (โโ๐ด) โ โค) โ
(logโ((โโ๐ด)โ(โโ๐ด))) = ((โโ๐ด) ยท (logโ(โโ๐ด)))) |
25 | 11, 23, 24 | syl2anc 584 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ((โโ๐ด)โ(โโ๐ด))) = ((โโ๐ด) ยท (logโ(โโ๐ด)))) |
26 | 22, 25 | breqtrd 5173 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โค ((โโ๐ด) ยท (logโ(โโ๐ด)))) |
27 | | flle 13760 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โค
๐ด) |
28 | 8, 27 | syl 17 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โค
๐ด) |
29 | | simpl 483 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ+) |
30 | 11, 29 | logled 26126 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด) โค
๐ด โ
(logโ(โโ๐ด)) โค (logโ๐ด))) |
31 | 28, 30 | mpbid 231 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(โโ๐ด)) โค (logโ๐ด)) |
32 | 11 | rprege0d 13019 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด) โ
โ โง 0 โค (โโ๐ด))) |
33 | | log1 26085 |
. . . . . 6
โข
(logโ1) = 0 |
34 | 3 | nnge1d 12256 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โค (โโ๐ด)) |
35 | | 1rp 12974 |
. . . . . . . 8
โข 1 โ
โ+ |
36 | | logleb 26102 |
. . . . . . . 8
โข ((1
โ โ+ โง (โโ๐ด) โ โ+) โ (1 โค
(โโ๐ด) โ
(logโ1) โค (logโ(โโ๐ด)))) |
37 | 35, 11, 36 | sylancr 587 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ (1
โค (โโ๐ด)
โ (logโ1) โค (logโ(โโ๐ด)))) |
38 | 34, 37 | mpbid 231 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ1) โค (logโ(โโ๐ด))) |
39 | 33, 38 | eqbrtrrid 5183 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 0
โค (logโ(โโ๐ด))) |
40 | 12, 39 | jca 512 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((logโ(โโ๐ด)) โ โ โง 0 โค
(logโ(โโ๐ด)))) |
41 | | lemul12a 12068 |
. . . 4
โข
(((((โโ๐ด) โ โ โง 0 โค
(โโ๐ด)) โง
๐ด โ โ) โง
(((logโ(โโ๐ด)) โ โ โง 0 โค
(logโ(โโ๐ด))) โง (logโ๐ด) โ โ)) โ
(((โโ๐ด) โค
๐ด โง
(logโ(โโ๐ด)) โค (logโ๐ด)) โ ((โโ๐ด) ยท (logโ(โโ๐ด))) โค (๐ด ยท (logโ๐ด)))) |
42 | 32, 8, 40, 15, 41 | syl22anc 837 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(((โโ๐ด) โค
๐ด โง
(logโ(โโ๐ด)) โค (logโ๐ด)) โ ((โโ๐ด) ยท (logโ(โโ๐ด))) โค (๐ด ยท (logโ๐ด)))) |
43 | 28, 31, 42 | mp2and 697 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((โโ๐ด) ยท
(logโ(โโ๐ด))) โค (๐ด ยท (logโ๐ด))) |
44 | 7, 13, 16, 26, 43 | letrd 11367 |
1
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โค (๐ด ยท (logโ๐ด))) |