Step | Hyp | Ref
| Expression |
1 | | fzfid 13870 |
. . . . . 6
โข (๐ด โ โ+
โ (1...(โโ๐ด)) โ Fin) |
2 | | elfznn 13462 |
. . . . . . . 8
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
3 | 2 | adantl 482 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ โ
(1...(โโ๐ด)))
โ ๐ โ
โ) |
4 | 3 | nnrecred 12200 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ โ
(1...(โโ๐ด)))
โ (1 / ๐) โ
โ) |
5 | 1, 4 | fsumrecl 15611 |
. . . . 5
โข (๐ด โ โ+
โ ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
โ) |
6 | 5 | recnd 11179 |
. . . 4
โข (๐ด โ โ+
โ ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
โ) |
7 | | relogcl 25915 |
. . . . 5
โข (๐ด โ โ+
โ (logโ๐ด) โ
โ) |
8 | 7 | recnd 11179 |
. . . 4
โข (๐ด โ โ+
โ (logโ๐ด) โ
โ) |
9 | | emre 26339 |
. . . . . 6
โข ฮณ
โ โ |
10 | 9 | a1i 11 |
. . . . 5
โข (๐ด โ โ+
โ ฮณ โ โ) |
11 | 10 | recnd 11179 |
. . . 4
โข (๐ด โ โ+
โ ฮณ โ โ) |
12 | 6, 8, 11 | subsub4d 11539 |
. . 3
โข (๐ด โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โ ฮณ) =
(ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
((logโ๐ด) +
ฮณ))) |
13 | 12 | fveq2d 6843 |
. 2
โข (๐ด โ โ+
โ (absโ((ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ๐ด)) โ ฮณ)) =
(absโ(ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
((logโ๐ด) +
ฮณ)))) |
14 | | rpreccl 12933 |
. . . . . 6
โข (๐ด โ โ+
โ (1 / ๐ด) โ
โ+) |
15 | 14 | rpred 12949 |
. . . . 5
โข (๐ด โ โ+
โ (1 / ๐ด) โ
โ) |
16 | | resubcl 11461 |
. . . . 5
โข ((ฮณ
โ โ โง (1 / ๐ด) โ โ) โ (ฮณ โ (1
/ ๐ด)) โ
โ) |
17 | 9, 15, 16 | sylancr 587 |
. . . 4
โข (๐ด โ โ+
โ (ฮณ โ (1 / ๐ด)) โ โ) |
18 | | rprege0 12922 |
. . . . . . . . 9
โข (๐ด โ โ+
โ (๐ด โ โ
โง 0 โค ๐ด)) |
19 | | flge0nn0 13717 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(โโ๐ด) โ
โ0) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ+
โ (โโ๐ด)
โ โ0) |
21 | | nn0p1nn 12448 |
. . . . . . . 8
โข
((โโ๐ด)
โ โ0 โ ((โโ๐ด) + 1) โ โ) |
22 | 20, 21 | syl 17 |
. . . . . . 7
โข (๐ด โ โ+
โ ((โโ๐ด) +
1) โ โ) |
23 | 22 | nnrpd 12947 |
. . . . . 6
โข (๐ด โ โ+
โ ((โโ๐ด) +
1) โ โ+) |
24 | | relogcl 25915 |
. . . . . 6
โข
(((โโ๐ด)
+ 1) โ โ+ โ (logโ((โโ๐ด) + 1)) โ
โ) |
25 | 23, 24 | syl 17 |
. . . . 5
โข (๐ด โ โ+
โ (logโ((โโ๐ด) + 1)) โ โ) |
26 | 5, 25 | resubcld 11579 |
. . . 4
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โ โ) |
27 | 5, 7 | resubcld 11579 |
. . . 4
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โ
โ) |
28 | 22 | nnrecred 12200 |
. . . . . 6
โข (๐ด โ โ+
โ (1 / ((โโ๐ด) + 1)) โ โ) |
29 | | fzfid 13870 |
. . . . . . . 8
โข (๐ด โ โ+
โ (1...((โโ๐ด) + 1)) โ Fin) |
30 | | elfznn 13462 |
. . . . . . . . . 10
โข (๐ โ
(1...((โโ๐ด) +
1)) โ ๐ โ
โ) |
31 | 30 | adantl 482 |
. . . . . . . . 9
โข ((๐ด โ โ+
โง ๐ โ
(1...((โโ๐ด) +
1))) โ ๐ โ
โ) |
32 | 31 | nnrecred 12200 |
. . . . . . . 8
โข ((๐ด โ โ+
โง ๐ โ
(1...((โโ๐ด) +
1))) โ (1 / ๐) โ
โ) |
33 | 29, 32 | fsumrecl 15611 |
. . . . . . 7
โข (๐ด โ โ+
โ ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
โ) |
34 | 33, 25 | resubcld 11579 |
. . . . . 6
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1))) โ โ) |
35 | | harmonicbnd 26337 |
. . . . . . . 8
โข
(((โโ๐ด)
+ 1) โ โ โ (ฮฃ๐ โ (1...((โโ๐ด) + 1))(1 / ๐) โ (logโ((โโ๐ด) + 1))) โ
(ฮณ[,]1)) |
36 | 22, 35 | syl 17 |
. . . . . . 7
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1))) โ
(ฮณ[,]1)) |
37 | | 1re 11151 |
. . . . . . . . 9
โข 1 โ
โ |
38 | 9, 37 | elicc2i 13322 |
. . . . . . . 8
โข
((ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1))) โ (ฮณ[,]1) โ
((ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1))) โ โ โง ฮณ โค
(ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1))) โง (ฮฃ๐ โ (1...((โโ๐ด) + 1))(1 / ๐) โ (logโ((โโ๐ด) + 1))) โค
1)) |
39 | 38 | simp2bi 1146 |
. . . . . . 7
โข
((ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1))) โ (ฮณ[,]1) โ ฮณ
โค (ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1)))) |
40 | 36, 39 | syl 17 |
. . . . . 6
โข (๐ด โ โ+
โ ฮณ โค (ฮฃ๐ โ (1...((โโ๐ด) + 1))(1 / ๐) โ (logโ((โโ๐ด) + 1)))) |
41 | | rpre 12915 |
. . . . . . . 8
โข (๐ด โ โ+
โ ๐ด โ
โ) |
42 | | fllep1 13698 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โค ((โโ๐ด) + 1)) |
43 | 41, 42 | syl 17 |
. . . . . . 7
โข (๐ด โ โ+
โ ๐ด โค
((โโ๐ด) +
1)) |
44 | | rpregt0 12921 |
. . . . . . . 8
โข (๐ด โ โ+
โ (๐ด โ โ
โง 0 < ๐ด)) |
45 | 22 | nnred 12164 |
. . . . . . . 8
โข (๐ด โ โ+
โ ((โโ๐ด) +
1) โ โ) |
46 | 22 | nngt0d 12198 |
. . . . . . . 8
โข (๐ด โ โ+
โ 0 < ((โโ๐ด) + 1)) |
47 | | lerec 12034 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 <
๐ด) โง
(((โโ๐ด) + 1)
โ โ โง 0 < ((โโ๐ด) + 1))) โ (๐ด โค ((โโ๐ด) + 1) โ (1 / ((โโ๐ด) + 1)) โค (1 / ๐ด))) |
48 | 44, 45, 46, 47 | syl12anc 835 |
. . . . . . 7
โข (๐ด โ โ+
โ (๐ด โค
((โโ๐ด) + 1)
โ (1 / ((โโ๐ด) + 1)) โค (1 / ๐ด))) |
49 | 43, 48 | mpbid 231 |
. . . . . 6
โข (๐ด โ โ+
โ (1 / ((โโ๐ด) + 1)) โค (1 / ๐ด)) |
50 | 10, 28, 34, 15, 40, 49 | le2subd 11771 |
. . . . 5
โข (๐ด โ โ+
โ (ฮณ โ (1 / ๐ด)) โค ((ฮฃ๐ โ (1...((โโ๐ด) + 1))(1 / ๐) โ (logโ((โโ๐ด) + 1))) โ (1 /
((โโ๐ด) +
1)))) |
51 | 33 | recnd 11179 |
. . . . . . 7
โข (๐ด โ โ+
โ ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
โ) |
52 | 25 | recnd 11179 |
. . . . . . 7
โข (๐ด โ โ+
โ (logโ((โโ๐ด) + 1)) โ โ) |
53 | 28 | recnd 11179 |
. . . . . . 7
โข (๐ด โ โ+
โ (1 / ((โโ๐ด) + 1)) โ โ) |
54 | 51, 52, 53 | sub32d 11540 |
. . . . . 6
โข (๐ด โ โ+
โ ((ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1))) โ (1 / ((โโ๐ด) + 1))) = ((ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ (1 /
((โโ๐ด) + 1)))
โ (logโ((โโ๐ด) + 1)))) |
55 | | nnuz 12798 |
. . . . . . . . . . 11
โข โ =
(โคโฅโ1) |
56 | 22, 55 | eleqtrdi 2848 |
. . . . . . . . . 10
โข (๐ด โ โ+
โ ((โโ๐ด) +
1) โ (โคโฅโ1)) |
57 | 32 | recnd 11179 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง ๐ โ
(1...((โโ๐ด) +
1))) โ (1 / ๐) โ
โ) |
58 | | oveq2 7361 |
. . . . . . . . . 10
โข (๐ = ((โโ๐ด) + 1) โ (1 / ๐) = (1 / ((โโ๐ด) + 1))) |
59 | 56, 57, 58 | fsumm1 15628 |
. . . . . . . . 9
โข (๐ด โ โ+
โ ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) = (ฮฃ๐ โ
(1...(((โโ๐ด) +
1) โ 1))(1 / ๐) + (1
/ ((โโ๐ด) +
1)))) |
60 | 20 | nn0cnd 12471 |
. . . . . . . . . . . . 13
โข (๐ด โ โ+
โ (โโ๐ด)
โ โ) |
61 | | ax-1cn 11105 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
62 | | pncan 11403 |
. . . . . . . . . . . . 13
โข
(((โโ๐ด)
โ โ โง 1 โ โ) โ (((โโ๐ด) + 1) โ 1) =
(โโ๐ด)) |
63 | 60, 61, 62 | sylancl 586 |
. . . . . . . . . . . 12
โข (๐ด โ โ+
โ (((โโ๐ด)
+ 1) โ 1) = (โโ๐ด)) |
64 | 63 | oveq2d 7369 |
. . . . . . . . . . 11
โข (๐ด โ โ+
โ (1...(((โโ๐ด) + 1) โ 1)) =
(1...(โโ๐ด))) |
65 | 64 | sumeq1d 15578 |
. . . . . . . . . 10
โข (๐ด โ โ+
โ ฮฃ๐ โ
(1...(((โโ๐ด) +
1) โ 1))(1 / ๐) =
ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐)) |
66 | 65 | oveq1d 7368 |
. . . . . . . . 9
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...(((โโ๐ด) +
1) โ 1))(1 / ๐) + (1
/ ((โโ๐ด) + 1)))
= (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) + (1 /
((โโ๐ด) +
1)))) |
67 | 59, 66 | eqtrd 2776 |
. . . . . . . 8
โข (๐ด โ โ+
โ ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) = (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) + (1 /
((โโ๐ด) +
1)))) |
68 | 6, 53, 67 | mvrraddd 11563 |
. . . . . . 7
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ (1 /
((โโ๐ด) + 1))) =
ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐)) |
69 | 68 | oveq1d 7368 |
. . . . . 6
โข (๐ด โ โ+
โ ((ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ (1 /
((โโ๐ด) + 1)))
โ (logโ((โโ๐ด) + 1))) = (ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ((โโ๐ด) + 1)))) |
70 | 54, 69 | eqtrd 2776 |
. . . . 5
โข (๐ด โ โ+
โ ((ฮฃ๐ โ
(1...((โโ๐ด) +
1))(1 / ๐) โ
(logโ((โโ๐ด) + 1))) โ (1 / ((โโ๐ด) + 1))) = (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1)))) |
71 | 50, 70 | breqtrd 5129 |
. . . 4
โข (๐ด โ โ+
โ (ฮณ โ (1 / ๐ด)) โค (ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ((โโ๐ด) + 1)))) |
72 | | logleb 25942 |
. . . . . . 7
โข ((๐ด โ โ+
โง ((โโ๐ด) +
1) โ โ+) โ (๐ด โค ((โโ๐ด) + 1) โ (logโ๐ด) โค (logโ((โโ๐ด) + 1)))) |
73 | 23, 72 | mpdan 685 |
. . . . . 6
โข (๐ด โ โ+
โ (๐ด โค
((โโ๐ด) + 1)
โ (logโ๐ด) โค
(logโ((โโ๐ด) + 1)))) |
74 | 43, 73 | mpbid 231 |
. . . . 5
โข (๐ด โ โ+
โ (logโ๐ด) โค
(logโ((โโ๐ด) + 1))) |
75 | 7, 25, 5, 74 | lesub2dd 11768 |
. . . 4
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โค (ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ๐ด))) |
76 | 17, 26, 27, 71, 75 | letrd 11308 |
. . 3
โข (๐ด โ โ+
โ (ฮณ โ (1 / ๐ด)) โค (ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ๐ด))) |
77 | 27, 15 | resubcld 11579 |
. . . . 5
โข (๐ด โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โ (1 / ๐ด)) โ
โ) |
78 | 15 | recnd 11179 |
. . . . . . 7
โข (๐ด โ โ+
โ (1 / ๐ด) โ
โ) |
79 | 6, 8, 78 | subsub4d 11539 |
. . . . . 6
โข (๐ด โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โ (1 / ๐ด)) = (ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ ((logโ๐ด) + (1 / ๐ด)))) |
80 | 7, 15 | readdcld 11180 |
. . . . . . 7
โข (๐ด โ โ+
โ ((logโ๐ด) + (1
/ ๐ด)) โ
โ) |
81 | | id 22 |
. . . . . . . . . 10
โข (๐ด โ โ+
โ ๐ด โ
โ+) |
82 | 23, 81 | relogdivd 25965 |
. . . . . . . . 9
โข (๐ด โ โ+
โ (logโ(((โโ๐ด) + 1) / ๐ด)) = ((logโ((โโ๐ด) + 1)) โ (logโ๐ด))) |
83 | | rerpdivcl 12937 |
. . . . . . . . . . . . 13
โข
((((โโ๐ด)
+ 1) โ โ โง ๐ด
โ โ+) โ (((โโ๐ด) + 1) / ๐ด) โ โ) |
84 | 45, 83 | mpancom 686 |
. . . . . . . . . . . 12
โข (๐ด โ โ+
โ (((โโ๐ด)
+ 1) / ๐ด) โ
โ) |
85 | 37 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ด โ โ+
โ 1 โ โ) |
86 | 85, 15 | readdcld 11180 |
. . . . . . . . . . . 12
โข (๐ด โ โ+
โ (1 + (1 / ๐ด)) โ
โ) |
87 | 15 | reefcld 15962 |
. . . . . . . . . . . 12
โข (๐ด โ โ+
โ (expโ(1 / ๐ด))
โ โ) |
88 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ+
โ 1 โ โ) |
89 | | rpcnne0 12925 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ+
โ (๐ด โ โ
โง ๐ด โ
0)) |
90 | | divdir 11834 |
. . . . . . . . . . . . . 14
โข
(((โโ๐ด)
โ โ โง 1 โ โ โง (๐ด โ โ โง ๐ด โ 0)) โ (((โโ๐ด) + 1) / ๐ด) = (((โโ๐ด) / ๐ด) + (1 / ๐ด))) |
91 | 60, 88, 89, 90 | syl3anc 1371 |
. . . . . . . . . . . . 13
โข (๐ด โ โ+
โ (((โโ๐ด)
+ 1) / ๐ด) =
(((โโ๐ด) / ๐ด) + (1 / ๐ด))) |
92 | | reflcl 13693 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
93 | 41, 92 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ+
โ (โโ๐ด)
โ โ) |
94 | | rerpdivcl 12937 |
. . . . . . . . . . . . . . 15
โข
(((โโ๐ด)
โ โ โง ๐ด
โ โ+) โ ((โโ๐ด) / ๐ด) โ โ) |
95 | 93, 94 | mpancom 686 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ+
โ ((โโ๐ด) /
๐ด) โ
โ) |
96 | | flle 13696 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โ โ
(โโ๐ด) โค
๐ด) |
97 | 41, 96 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ+
โ (โโ๐ด)
โค ๐ด) |
98 | | rpcn 12917 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โ+
โ ๐ด โ
โ) |
99 | 98 | mulid1d 11168 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ+
โ (๐ด ยท 1) =
๐ด) |
100 | 97, 99 | breqtrrd 5131 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ+
โ (โโ๐ด)
โค (๐ด ยท
1)) |
101 | | ledivmul 12027 |
. . . . . . . . . . . . . . . 16
โข
(((โโ๐ด)
โ โ โง 1 โ โ โง (๐ด โ โ โง 0 < ๐ด)) โ (((โโ๐ด) / ๐ด) โค 1 โ (โโ๐ด) โค (๐ด ยท 1))) |
102 | 93, 85, 44, 101 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ+
โ (((โโ๐ด)
/ ๐ด) โค 1 โ
(โโ๐ด) โค
(๐ด ยท
1))) |
103 | 100, 102 | mpbird 256 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ+
โ ((โโ๐ด) /
๐ด) โค 1) |
104 | 95, 85, 15, 103 | leadd1dd 11765 |
. . . . . . . . . . . . 13
โข (๐ด โ โ+
โ (((โโ๐ด)
/ ๐ด) + (1 / ๐ด)) โค (1 + (1 / ๐ด))) |
105 | 91, 104 | eqbrtrd 5125 |
. . . . . . . . . . . 12
โข (๐ด โ โ+
โ (((โโ๐ด)
+ 1) / ๐ด) โค (1 + (1 /
๐ด))) |
106 | | efgt1p 15989 |
. . . . . . . . . . . . . 14
โข ((1 /
๐ด) โ
โ+ โ (1 + (1 / ๐ด)) < (expโ(1 / ๐ด))) |
107 | 14, 106 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ด โ โ+
โ (1 + (1 / ๐ด)) <
(expโ(1 / ๐ด))) |
108 | 86, 87, 107 | ltled 11299 |
. . . . . . . . . . . 12
โข (๐ด โ โ+
โ (1 + (1 / ๐ด)) โค
(expโ(1 / ๐ด))) |
109 | 84, 86, 87, 105, 108 | letrd 11308 |
. . . . . . . . . . 11
โข (๐ด โ โ+
โ (((โโ๐ด)
+ 1) / ๐ด) โค
(expโ(1 / ๐ด))) |
110 | | rpdivcl 12932 |
. . . . . . . . . . . . 13
โข
((((โโ๐ด)
+ 1) โ โ+ โง ๐ด โ โ+) โ
(((โโ๐ด) + 1) /
๐ด) โ
โ+) |
111 | 23, 110 | mpancom 686 |
. . . . . . . . . . . 12
โข (๐ด โ โ+
โ (((โโ๐ด)
+ 1) / ๐ด) โ
โ+) |
112 | 15 | rpefcld 15979 |
. . . . . . . . . . . 12
โข (๐ด โ โ+
โ (expโ(1 / ๐ด))
โ โ+) |
113 | 111, 112 | logled 25966 |
. . . . . . . . . . 11
โข (๐ด โ โ+
โ ((((โโ๐ด)
+ 1) / ๐ด) โค
(expโ(1 / ๐ด)) โ
(logโ(((โโ๐ด) + 1) / ๐ด)) โค (logโ(expโ(1 / ๐ด))))) |
114 | 109, 113 | mpbid 231 |
. . . . . . . . . 10
โข (๐ด โ โ+
โ (logโ(((โโ๐ด) + 1) / ๐ด)) โค (logโ(expโ(1 / ๐ด)))) |
115 | 15 | relogefd 25967 |
. . . . . . . . . 10
โข (๐ด โ โ+
โ (logโ(expโ(1 / ๐ด))) = (1 / ๐ด)) |
116 | 114, 115 | breqtrd 5129 |
. . . . . . . . 9
โข (๐ด โ โ+
โ (logโ(((โโ๐ด) + 1) / ๐ด)) โค (1 / ๐ด)) |
117 | 82, 116 | eqbrtrrd 5127 |
. . . . . . . 8
โข (๐ด โ โ+
โ ((logโ((โโ๐ด) + 1)) โ (logโ๐ด)) โค (1 / ๐ด)) |
118 | 25, 7, 15 | lesubadd2d 11750 |
. . . . . . . 8
โข (๐ด โ โ+
โ (((logโ((โโ๐ด) + 1)) โ (logโ๐ด)) โค (1 / ๐ด) โ (logโ((โโ๐ด) + 1)) โค ((logโ๐ด) + (1 / ๐ด)))) |
119 | 117, 118 | mpbid 231 |
. . . . . . 7
โข (๐ด โ โ+
โ (logโ((โโ๐ด) + 1)) โค ((logโ๐ด) + (1 / ๐ด))) |
120 | 25, 80, 5, 119 | lesub2dd 11768 |
. . . . . 6
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
((logโ๐ด) + (1 / ๐ด))) โค (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1)))) |
121 | 79, 120 | eqbrtrd 5125 |
. . . . 5
โข (๐ด โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โ (1 / ๐ด)) โค (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1)))) |
122 | | harmonicbnd3 26341 |
. . . . . . 7
โข
((โโ๐ด)
โ โ0 โ (ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ((โโ๐ด) + 1))) โ
(0[,]ฮณ)) |
123 | 20, 122 | syl 17 |
. . . . . 6
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โ
(0[,]ฮณ)) |
124 | | 0re 11153 |
. . . . . . . 8
โข 0 โ
โ |
125 | 124, 9 | elicc2i 13322 |
. . . . . . 7
โข
((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โ (0[,]ฮณ) โ
((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โ โ โง 0 โค
(ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โง (ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ((โโ๐ด) + 1))) โค
ฮณ)) |
126 | 125 | simp3bi 1147 |
. . . . . 6
โข
((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โ (0[,]ฮณ) โ
(ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โค ฮณ) |
127 | 123, 126 | syl 17 |
. . . . 5
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ
(logโ((โโ๐ด) + 1))) โค ฮณ) |
128 | 77, 26, 10, 121, 127 | letrd 11308 |
. . . 4
โข (๐ด โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โ (1 / ๐ด)) โค
ฮณ) |
129 | 27, 15, 10 | lesubaddd 11748 |
. . . 4
โข (๐ด โ โ+
โ (((ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โ (1 / ๐ด)) โค ฮณ โ
(ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โค (ฮณ + (1 / ๐ด)))) |
130 | 128, 129 | mpbid 231 |
. . 3
โข (๐ด โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โค (ฮณ + (1 / ๐ด))) |
131 | 27, 10, 15 | absdifled 15311 |
. . 3
โข (๐ด โ โ+
โ ((absโ((ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ๐ด)) โ ฮณ)) โค (1 / ๐ด) โ ((ฮณ โ (1 /
๐ด)) โค (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โง (ฮฃ๐ โ
(1...(โโ๐ด))(1 /
๐) โ (logโ๐ด)) โค (ฮณ + (1 / ๐ด))))) |
132 | 76, 130, 131 | mpbir2and 711 |
. 2
โข (๐ด โ โ+
โ (absโ((ฮฃ๐ โ (1...(โโ๐ด))(1 / ๐) โ (logโ๐ด)) โ ฮณ)) โค (1 / ๐ด)) |
133 | 13, 132 | eqbrtrrd 5127 |
1
โข (๐ด โ โ+
โ (absโ(ฮฃ๐
โ (1...(โโ๐ด))(1 / ๐) โ ((logโ๐ด) + ฮณ))) โค (1 / ๐ด)) |