Step | Hyp | Ref
| Expression |
1 | | 2div2e1 12290 |
. . 3
โข (2 / 2) =
1 |
2 | | 2re 12223 |
. . . . 5
โข 2 โ
โ |
3 | 2 | a1i 11 |
. . . 4
โข (๐ โ 2 โ
โ) |
4 | | ioossre 13317 |
. . . . . 6
โข (0(,)1)
โ โ |
5 | | pntpbnd1.e |
. . . . . 6
โข (๐ โ ๐ธ โ (0(,)1)) |
6 | 4, 5 | sselid 3940 |
. . . . 5
โข (๐ โ ๐ธ โ โ) |
7 | | eliooord 13315 |
. . . . . . 7
โข (๐ธ โ (0(,)1) โ (0 <
๐ธ โง ๐ธ < 1)) |
8 | 5, 7 | syl 17 |
. . . . . 6
โข (๐ โ (0 < ๐ธ โง ๐ธ < 1)) |
9 | 8 | simpld 495 |
. . . . 5
โข (๐ โ 0 < ๐ธ) |
10 | 6, 9 | elrpd 12946 |
. . . 4
โข (๐ โ ๐ธ โ
โ+) |
11 | | 2rp 12912 |
. . . . 5
โข 2 โ
โ+ |
12 | 11 | a1i 11 |
. . . 4
โข (๐ โ 2 โ
โ+) |
13 | | pntpbnd1.c |
. . . . . . . . 9
โข ๐ถ = (๐ด + 2) |
14 | 13 | oveq1i 7363 |
. . . . . . . 8
โข (๐ถ โ ๐ด) = ((๐ด + 2) โ ๐ด) |
15 | | pntpbnd1.1 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ
โ+) |
16 | 15 | rpcnd 12951 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
17 | | 2cn 12224 |
. . . . . . . . 9
โข 2 โ
โ |
18 | | pncan2 11404 |
. . . . . . . . 9
โข ((๐ด โ โ โง 2 โ
โ) โ ((๐ด + 2)
โ ๐ด) =
2) |
19 | 16, 17, 18 | sylancl 586 |
. . . . . . . 8
โข (๐ โ ((๐ด + 2) โ ๐ด) = 2) |
20 | 14, 19 | eqtrid 2788 |
. . . . . . 7
โข (๐ โ (๐ถ โ ๐ด) = 2) |
21 | 20 | oveq1d 7368 |
. . . . . 6
โข (๐ โ ((๐ถ โ ๐ด) / ๐ธ) = (2 / ๐ธ)) |
22 | | rpaddcl 12929 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 2 โ โ+) โ (๐ด + 2) โ
โ+) |
23 | 15, 11, 22 | sylancl 586 |
. . . . . . . . 9
โข (๐ โ (๐ด + 2) โ
โ+) |
24 | 13, 23 | eqeltrid 2842 |
. . . . . . . 8
โข (๐ โ ๐ถ โ
โ+) |
25 | 24 | rpcnd 12951 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
26 | 6 | recnd 11179 |
. . . . . . 7
โข (๐ โ ๐ธ โ โ) |
27 | 10 | rpne0d 12954 |
. . . . . . 7
โข (๐ โ ๐ธ โ 0) |
28 | 25, 16, 26, 27 | divsubdird 11966 |
. . . . . 6
โข (๐ โ ((๐ถ โ ๐ด) / ๐ธ) = ((๐ถ / ๐ธ) โ (๐ด / ๐ธ))) |
29 | 21, 28 | eqtr3d 2778 |
. . . . 5
โข (๐ โ (2 / ๐ธ) = ((๐ถ / ๐ธ) โ (๐ด / ๐ธ))) |
30 | 24, 10 | rpdivcld 12966 |
. . . . . . 7
โข (๐ โ (๐ถ / ๐ธ) โ
โ+) |
31 | 30 | rpred 12949 |
. . . . . 6
โข (๐ โ (๐ถ / ๐ธ) โ โ) |
32 | 15 | rpred 12949 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
33 | 32, 10 | rerpdivcld 12980 |
. . . . . 6
โข (๐ โ (๐ด / ๐ธ) โ โ) |
34 | | resubcl 11461 |
. . . . . . . 8
โข (((๐ถ / ๐ธ) โ โ โง 2 โ โ)
โ ((๐ถ / ๐ธ) โ 2) โ
โ) |
35 | 31, 2, 34 | sylancl 586 |
. . . . . . 7
โข (๐ โ ((๐ถ / ๐ธ) โ 2) โ
โ) |
36 | | pntpbnd1.k |
. . . . . . . . . . . 12
โข (๐ โ ๐พ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) |
37 | 31 | reefcld 15962 |
. . . . . . . . . . . . 13
โข (๐ โ (expโ(๐ถ / ๐ธ)) โ โ) |
38 | | elicopnf 13354 |
. . . . . . . . . . . . 13
โข
((expโ(๐ถ /
๐ธ)) โ โ โ
(๐พ โ
((expโ(๐ถ / ๐ธ))[,)+โ) โ (๐พ โ โ โง
(expโ(๐ถ / ๐ธ)) โค ๐พ))) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (๐พ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โ (๐พ โ โ โง (expโ(๐ถ / ๐ธ)) โค ๐พ))) |
40 | 36, 39 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ (๐พ โ โ โง (expโ(๐ถ / ๐ธ)) โค ๐พ)) |
41 | 40 | simpld 495 |
. . . . . . . . . 10
โข (๐ โ ๐พ โ โ) |
42 | | 0red 11154 |
. . . . . . . . . . 11
โข (๐ โ 0 โ
โ) |
43 | | 1re 11151 |
. . . . . . . . . . . 12
โข 1 โ
โ |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 1 โ
โ) |
45 | | 0lt1 11673 |
. . . . . . . . . . . 12
โข 0 <
1 |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 0 < 1) |
47 | | efgt1 15990 |
. . . . . . . . . . . . 13
โข ((๐ถ / ๐ธ) โ โ+ โ 1 <
(expโ(๐ถ / ๐ธ))) |
48 | 30, 47 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ 1 < (expโ(๐ถ / ๐ธ))) |
49 | 40 | simprd 496 |
. . . . . . . . . . . 12
โข (๐ โ (expโ(๐ถ / ๐ธ)) โค ๐พ) |
50 | 44, 37, 41, 48, 49 | ltletrd 11311 |
. . . . . . . . . . 11
โข (๐ โ 1 < ๐พ) |
51 | 42, 44, 41, 46, 50 | lttrd 11312 |
. . . . . . . . . 10
โข (๐ โ 0 < ๐พ) |
52 | 41, 51 | elrpd 12946 |
. . . . . . . . 9
โข (๐ โ ๐พ โ
โ+) |
53 | 52 | relogcld 25962 |
. . . . . . . 8
โข (๐ โ (logโ๐พ) โ
โ) |
54 | | resubcl 11461 |
. . . . . . . 8
โข
(((logโ๐พ)
โ โ โง 2 โ โ) โ ((logโ๐พ) โ 2) โ
โ) |
55 | 53, 2, 54 | sylancl 586 |
. . . . . . 7
โข (๐ โ ((logโ๐พ) โ 2) โ
โ) |
56 | 52 | reeflogd 25963 |
. . . . . . . . . 10
โข (๐ โ
(expโ(logโ๐พ)) =
๐พ) |
57 | 49, 56 | breqtrrd 5131 |
. . . . . . . . 9
โข (๐ โ (expโ(๐ถ / ๐ธ)) โค (expโ(logโ๐พ))) |
58 | | efle 15992 |
. . . . . . . . . 10
โข (((๐ถ / ๐ธ) โ โ โง (logโ๐พ) โ โ) โ ((๐ถ / ๐ธ) โค (logโ๐พ) โ (expโ(๐ถ / ๐ธ)) โค (expโ(logโ๐พ)))) |
59 | 31, 53, 58 | syl2anc 584 |
. . . . . . . . 9
โข (๐ โ ((๐ถ / ๐ธ) โค (logโ๐พ) โ (expโ(๐ถ / ๐ธ)) โค (expโ(logโ๐พ)))) |
60 | 57, 59 | mpbird 256 |
. . . . . . . 8
โข (๐ โ (๐ถ / ๐ธ) โค (logโ๐พ)) |
61 | 31, 53, 3, 60 | lesub1dd 11767 |
. . . . . . 7
โข (๐ โ ((๐ถ / ๐ธ) โ 2) โค ((logโ๐พ) โ 2)) |
62 | | fzfid 13870 |
. . . . . . . . 9
โข (๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐))) โ Fin) |
63 | | ioossre 13317 |
. . . . . . . . . . . . . . 15
โข (๐(,)+โ) โ
โ |
64 | | pntpbnd1.y |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ (๐(,)+โ)) |
65 | 63, 64 | sselid 3940 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
66 | | pntpbnd1.x |
. . . . . . . . . . . . . . . . 17
โข ๐ = (expโ(2 / ๐ธ)) |
67 | | rerpdivcl 12937 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ โ โง ๐ธ
โ โ+) โ (2 / ๐ธ) โ โ) |
68 | 2, 10, 67 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (2 / ๐ธ) โ โ) |
69 | 68 | reefcld 15962 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (expโ(2 / ๐ธ)) โ
โ) |
70 | 66, 69 | eqeltrid 2842 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โ) |
71 | | efgt0 15977 |
. . . . . . . . . . . . . . . . . 18
โข ((2 /
๐ธ) โ โ โ 0
< (expโ(2 / ๐ธ))) |
72 | 68, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 0 < (expโ(2 /
๐ธ))) |
73 | 72, 66 | breqtrrdi 5145 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 < ๐) |
74 | 70 | rexrd 11201 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ โ
โ*) |
75 | | elioopnf 13352 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ*
โ (๐ โ (๐(,)+โ) โ (๐ โ โ โง ๐ < ๐))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ โ (๐(,)+โ) โ (๐ โ โ โง ๐ < ๐))) |
77 | 64, 76 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ โ โ โง ๐ < ๐)) |
78 | 77 | simprd 496 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ < ๐) |
79 | 42, 70, 65, 73, 78 | lttrd 11312 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 < ๐) |
80 | 42, 65, 79 | ltled 11299 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 โค ๐) |
81 | | flge0nn0 13717 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 0 โค
๐) โ
(โโ๐) โ
โ0) |
82 | 65, 80, 81 | syl2anc 584 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ๐) โ
โ0) |
83 | | nn0p1nn 12448 |
. . . . . . . . . . . . 13
โข
((โโ๐)
โ โ0 โ ((โโ๐) + 1) โ โ) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((โโ๐) + 1) โ
โ) |
85 | | elfzuz 13429 |
. . . . . . . . . . . 12
โข (๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐))) โ ๐ โ
(โคโฅโ((โโ๐) + 1))) |
86 | | eluznn 12835 |
. . . . . . . . . . . 12
โข
((((โโ๐)
+ 1) โ โ โง ๐
โ (โคโฅโ((โโ๐) + 1))) โ ๐ โ โ) |
87 | 84, 85, 86 | syl2an 596 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ โ โ) |
88 | 87 | peano2nnd 12166 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ + 1) โ โ) |
89 | 88 | nnrecred 12200 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (1 / (๐ + 1)) โ โ) |
90 | 62, 89 | fsumrecl 15611 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)) โ โ) |
91 | 53 | recnd 11179 |
. . . . . . . . . 10
โข (๐ โ (logโ๐พ) โ
โ) |
92 | | 2cnd 12227 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
93 | 65, 79 | elrpd 12946 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ
โ+) |
94 | 93 | relogcld 25962 |
. . . . . . . . . . 11
โข (๐ โ (logโ๐) โ
โ) |
95 | 94 | recnd 11179 |
. . . . . . . . . 10
โข (๐ โ (logโ๐) โ
โ) |
96 | 91, 92, 95 | pnpcan2d 11546 |
. . . . . . . . 9
โข (๐ โ (((logโ๐พ) + (logโ๐)) โ (2 + (logโ๐))) = ((logโ๐พ) โ 2)) |
97 | 52, 93 | relogmuld 25964 |
. . . . . . . . . . 11
โข (๐ โ (logโ(๐พ ยท ๐)) = ((logโ๐พ) + (logโ๐))) |
98 | 53, 94 | readdcld 11180 |
. . . . . . . . . . . . 13
โข (๐ โ ((logโ๐พ) + (logโ๐)) โ โ) |
99 | 97, 98 | eqeltrd 2838 |
. . . . . . . . . . . 12
โข (๐ โ (logโ(๐พ ยท ๐)) โ โ) |
100 | | fzfid 13870 |
. . . . . . . . . . . . . 14
โข (๐ โ (0...(โโ๐)) โ Fin) |
101 | | elfznn0 13526 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(0...(โโ๐))
โ ๐ โ
โ0) |
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (0...(โโ๐))) โ ๐ โ โ0) |
103 | | nn0p1nn 12448 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0...(โโ๐))) โ (๐ + 1) โ โ) |
105 | 104 | nnrecred 12200 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (0...(โโ๐))) โ (1 / (๐ + 1)) โ โ) |
106 | 100, 105 | fsumrecl 15611 |
. . . . . . . . . . . . 13
โข (๐ โ ฮฃ๐ โ (0...(โโ๐))(1 / (๐ + 1)) โ โ) |
107 | 106, 90 | readdcld 11180 |
. . . . . . . . . . . 12
โข (๐ โ (ฮฃ๐ โ (0...(โโ๐))(1 / (๐ + 1)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))) โ โ) |
108 | | readdcl 11130 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง (logโ๐) โ โ) โ (2 +
(logโ๐)) โ
โ) |
109 | 2, 94, 108 | sylancr 587 |
. . . . . . . . . . . . 13
โข (๐ โ (2 + (logโ๐)) โ
โ) |
110 | 109, 90 | readdcld 11180 |
. . . . . . . . . . . 12
โข (๐ โ ((2 + (logโ๐)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))) โ โ) |
111 | 41, 65 | remulcld 11181 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐พ ยท ๐) โ โ) |
112 | 65 | recnd 11179 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ โ โ) |
113 | 112 | mulid2d 11169 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (1 ยท ๐) = ๐) |
114 | 44, 41, 50 | ltled 11299 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ 1 โค ๐พ) |
115 | | lemul1 12003 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((1
โ โ โง ๐พ
โ โ โง (๐
โ โ โง 0 < ๐)) โ (1 โค ๐พ โ (1 ยท ๐) โค (๐พ ยท ๐))) |
116 | 44, 41, 65, 79, 115 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (1 โค ๐พ โ (1 ยท ๐) โค (๐พ ยท ๐))) |
117 | 114, 116 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (1 ยท ๐) โค (๐พ ยท ๐)) |
118 | 113, 117 | eqbrtrrd 5127 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ โค (๐พ ยท ๐)) |
119 | 42, 65, 111, 80, 118 | letrd 11308 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 0 โค (๐พ ยท ๐)) |
120 | | flge0nn0 13717 |
. . . . . . . . . . . . . . . . . 18
โข (((๐พ ยท ๐) โ โ โง 0 โค (๐พ ยท ๐)) โ (โโ(๐พ ยท ๐)) โ
โ0) |
121 | 111, 119,
120 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ(๐พ ยท ๐)) โ
โ0) |
122 | | nn0p1nn 12448 |
. . . . . . . . . . . . . . . . 17
โข
((โโ(๐พ
ยท ๐)) โ
โ0 โ ((โโ(๐พ ยท ๐)) + 1) โ โ) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โโ(๐พ ยท ๐)) + 1) โ โ) |
124 | 123 | nnrpd 12947 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ(๐พ ยท ๐)) + 1) โ
โ+) |
125 | 124 | relogcld 25962 |
. . . . . . . . . . . . . 14
โข (๐ โ
(logโ((โโ(๐พ ยท ๐)) + 1)) โ โ) |
126 | | 1zzd 12530 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โ
โค) |
127 | 111 | flcld 13695 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ(๐พ ยท ๐)) โ โค) |
128 | 127 | peano2zd 12606 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((โโ(๐พ ยท ๐)) + 1) โ โค) |
129 | | elfznn 13462 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ
(1...((โโ(๐พ
ยท ๐)) + 1)) โ
๐ โ
โ) |
130 | 129 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))) โ ๐ โ โ) |
131 | | nnrecre 12191 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ (1 /
๐) โ
โ) |
132 | 131 | recnd 11179 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (1 /
๐) โ
โ) |
133 | 130, 132 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))) โ (1 / ๐) โ โ) |
134 | | oveq2 7361 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ + 1) โ (1 / ๐) = (1 / (๐ + 1))) |
135 | 126, 126,
128, 133, 134 | fsumshftm 15658 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐) = ฮฃ๐ โ ((1 โ
1)...(((โโ(๐พ
ยท ๐)) + 1) โ
1))(1 / (๐ +
1))) |
136 | | 1m1e0 12221 |
. . . . . . . . . . . . . . . . . . 19
โข (1
โ 1) = 0 |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (1 โ 1) =
0) |
138 | 127 | zcnd 12604 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โโ(๐พ ยท ๐)) โ โ) |
139 | | ax-1cn 11105 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โ |
140 | | pncan 11403 |
. . . . . . . . . . . . . . . . . . 19
โข
(((โโ(๐พ
ยท ๐)) โ โ
โง 1 โ โ) โ (((โโ(๐พ ยท ๐)) + 1) โ 1) = (โโ(๐พ ยท ๐))) |
141 | 138, 139,
140 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((โโ(๐พ ยท ๐)) + 1) โ 1) = (โโ(๐พ ยท ๐))) |
142 | 137, 141 | oveq12d 7371 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((1 โ
1)...(((โโ(๐พ
ยท ๐)) + 1) โ
1)) = (0...(โโ(๐พ ยท ๐)))) |
143 | 142 | sumeq1d 15578 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ฮฃ๐ โ ((1 โ
1)...(((โโ(๐พ
ยท ๐)) + 1) โ
1))(1 / (๐ + 1)) =
ฮฃ๐ โ
(0...(โโ(๐พ
ยท ๐)))(1 / (๐ + 1))) |
144 | | reflcl 13693 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ
(โโ๐) โ
โ) |
145 | 65, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โโ๐) โ
โ) |
146 | 145 | ltp1d 12081 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ๐) < ((โโ๐) + 1)) |
147 | | fzdisj 13460 |
. . . . . . . . . . . . . . . . . 18
โข
((โโ๐)
< ((โโ๐) +
1) โ ((0...(โโ๐)) โฉ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) = โ
) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((0...(โโ๐)) โฉ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) = โ
) |
149 | | flwordi 13709 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง (๐พ ยท ๐) โ โ โง ๐ โค (๐พ ยท ๐)) โ (โโ๐) โค (โโ(๐พ ยท ๐))) |
150 | 65, 111, 118, 149 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โโ๐) โค (โโ(๐พ ยท ๐))) |
151 | | elfz2nn0 13524 |
. . . . . . . . . . . . . . . . . . 19
โข
((โโ๐)
โ (0...(โโ(๐พ ยท ๐))) โ ((โโ๐) โ โ0 โง
(โโ(๐พ ยท
๐)) โ
โ0 โง (โโ๐) โค (โโ(๐พ ยท ๐)))) |
152 | 82, 121, 150, 151 | syl3anbrc 1343 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ๐) โ
(0...(โโ(๐พ
ยท ๐)))) |
153 | | fzsplit 13459 |
. . . . . . . . . . . . . . . . . 18
โข
((โโ๐)
โ (0...(โโ(๐พ ยท ๐))) โ (0...(โโ(๐พ ยท ๐))) = ((0...(โโ๐)) โช (((โโ๐) + 1)...(โโ(๐พ ยท ๐))))) |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (0...(โโ(๐พ ยท ๐))) = ((0...(โโ๐)) โช (((โโ๐) + 1)...(โโ(๐พ ยท ๐))))) |
155 | | fzfid 13870 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (0...(โโ(๐พ ยท ๐))) โ Fin) |
156 | | elfznn0 13526 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ
(0...(โโ(๐พ
ยท ๐))) โ ๐ โ
โ0) |
157 | 156 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ (0...(โโ(๐พ ยท ๐)))) โ ๐ โ โ0) |
158 | 157, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ (0...(โโ(๐พ ยท ๐)))) โ (๐ + 1) โ โ) |
159 | 158 | nnrecred 12200 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (0...(โโ(๐พ ยท ๐)))) โ (1 / (๐ + 1)) โ โ) |
160 | 159 | recnd 11179 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (0...(โโ(๐พ ยท ๐)))) โ (1 / (๐ + 1)) โ โ) |
161 | 148, 154,
155, 160 | fsumsplit 15618 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ฮฃ๐ โ (0...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)) = (ฮฃ๐ โ (0...(โโ๐))(1 / (๐ + 1)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)))) |
162 | 135, 143,
161 | 3eqtrd 2780 |
. . . . . . . . . . . . . . 15
โข (๐ โ ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐) = (ฮฃ๐ โ (0...(โโ๐))(1 / (๐ + 1)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)))) |
163 | 162, 107 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐) โ โ) |
164 | | fllep1 13698 |
. . . . . . . . . . . . . . . 16
โข ((๐พ ยท ๐) โ โ โ (๐พ ยท ๐) โค ((โโ(๐พ ยท ๐)) + 1)) |
165 | 111, 164 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐พ ยท ๐) โค ((โโ(๐พ ยท ๐)) + 1)) |
166 | 52, 93 | rpmulcld 12965 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐พ ยท ๐) โ
โ+) |
167 | 166, 124 | logled 25966 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐พ ยท ๐) โค ((โโ(๐พ ยท ๐)) + 1) โ (logโ(๐พ ยท ๐)) โค (logโ((โโ(๐พ ยท ๐)) + 1)))) |
168 | 165, 167 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ (logโ(๐พ ยท ๐)) โค (logโ((โโ(๐พ ยท ๐)) + 1))) |
169 | | emre 26339 |
. . . . . . . . . . . . . . . . 17
โข ฮณ
โ โ |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ฮณ โ
โ) |
171 | 163, 125 | resubcld 11579 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐) โ (logโ((โโ(๐พ ยท ๐)) + 1))) โ โ) |
172 | | 0re 11153 |
. . . . . . . . . . . . . . . . . 18
โข 0 โ
โ |
173 | | emgt0 26340 |
. . . . . . . . . . . . . . . . . 18
โข 0 <
ฮณ |
174 | 172, 169,
173 | ltleii 11274 |
. . . . . . . . . . . . . . . . 17
โข 0 โค
ฮณ |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 โค
ฮณ) |
176 | | harmonicbnd 26337 |
. . . . . . . . . . . . . . . . . 18
โข
(((โโ(๐พ
ยท ๐)) + 1) โ
โ โ (ฮฃ๐
โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐) โ (logโ((โโ(๐พ ยท ๐)) + 1))) โ
(ฮณ[,]1)) |
177 | 123, 176 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐) โ (logโ((โโ(๐พ ยท ๐)) + 1))) โ
(ฮณ[,]1)) |
178 | 169, 43 | elicc2i 13322 |
. . . . . . . . . . . . . . . . . 18
โข
((ฮฃ๐ โ
(1...((โโ(๐พ
ยท ๐)) + 1))(1 /
๐) โ
(logโ((โโ(๐พ ยท ๐)) + 1))) โ (ฮณ[,]1) โ
((ฮฃ๐ โ
(1...((โโ(๐พ
ยท ๐)) + 1))(1 /
๐) โ
(logโ((โโ(๐พ ยท ๐)) + 1))) โ โ โง ฮณ โค
(ฮฃ๐ โ
(1...((โโ(๐พ
ยท ๐)) + 1))(1 /
๐) โ
(logโ((โโ(๐พ ยท ๐)) + 1))) โง (ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐) โ (logโ((โโ(๐พ ยท ๐)) + 1))) โค 1)) |
179 | 178 | simp2bi 1146 |
. . . . . . . . . . . . . . . . 17
โข
((ฮฃ๐ โ
(1...((โโ(๐พ
ยท ๐)) + 1))(1 /
๐) โ
(logโ((โโ(๐พ ยท ๐)) + 1))) โ (ฮณ[,]1) โ
ฮณ โค (ฮฃ๐
โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐) โ (logโ((โโ(๐พ ยท ๐)) + 1)))) |
180 | 177, 179 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ฮณ โค (ฮฃ๐ โ
(1...((โโ(๐พ
ยท ๐)) + 1))(1 /
๐) โ
(logโ((โโ(๐พ ยท ๐)) + 1)))) |
181 | 42, 170, 171, 175, 180 | letrd 11308 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 โค (ฮฃ๐ โ
(1...((โโ(๐พ
ยท ๐)) + 1))(1 /
๐) โ
(logโ((โโ(๐พ ยท ๐)) + 1)))) |
182 | 163, 125 | subge0d 11741 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0 โค (ฮฃ๐ โ
(1...((โโ(๐พ
ยท ๐)) + 1))(1 /
๐) โ
(logโ((โโ(๐พ ยท ๐)) + 1))) โ
(logโ((โโ(๐พ ยท ๐)) + 1)) โค ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐))) |
183 | 181, 182 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ
(logโ((โโ(๐พ ยท ๐)) + 1)) โค ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐)) |
184 | 99, 125, 163, 168, 183 | letrd 11308 |
. . . . . . . . . . . . 13
โข (๐ โ (logโ(๐พ ยท ๐)) โค ฮฃ๐ โ (1...((โโ(๐พ ยท ๐)) + 1))(1 / ๐)) |
185 | 184, 162 | breqtrd 5129 |
. . . . . . . . . . . 12
โข (๐ โ (logโ(๐พ ยท ๐)) โค (ฮฃ๐ โ (0...(โโ๐))(1 / (๐ + 1)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)))) |
186 | 65 | flcld 13695 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ๐) โ
โค) |
187 | 186 | peano2zd 12606 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โโ๐) + 1) โ
โค) |
188 | | elfznn 13462 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(1...((โโ๐) +
1)) โ ๐ โ
โ) |
189 | 188 | adantl 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (1...((โโ๐) + 1))) โ ๐ โ
โ) |
190 | 189, 132 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...((โโ๐) + 1))) โ (1 / ๐) โ
โ) |
191 | 126, 126,
187, 190, 134 | fsumshftm 15658 |
. . . . . . . . . . . . . . 15
โข (๐ โ ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) = ฮฃ๐ โ ((1 โ
1)...(((โโ๐) +
1) โ 1))(1 / (๐ +
1))) |
192 | 145 | recnd 11179 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ๐) โ
โ) |
193 | | pncan 11403 |
. . . . . . . . . . . . . . . . . 18
โข
(((โโ๐)
โ โ โง 1 โ โ) โ (((โโ๐) + 1) โ 1) =
(โโ๐)) |
194 | 192, 139,
193 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((โโ๐) + 1) โ 1) =
(โโ๐)) |
195 | 137, 194 | oveq12d 7371 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((1 โ
1)...(((โโ๐) +
1) โ 1)) = (0...(โโ๐))) |
196 | 195 | sumeq1d 15578 |
. . . . . . . . . . . . . . 15
โข (๐ โ ฮฃ๐ โ ((1 โ
1)...(((โโ๐) +
1) โ 1))(1 / (๐ + 1))
= ฮฃ๐ โ
(0...(โโ๐))(1 /
(๐ + 1))) |
197 | 191, 196 | eqtrd 2776 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) = ฮฃ๐ โ (0...(โโ๐))(1 / (๐ + 1))) |
198 | 197, 106 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
โข (๐ โ ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) โ โ) |
199 | 84 | nnrpd 12947 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((โโ๐) + 1) โ
โ+) |
200 | 199 | relogcld 25962 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(logโ((โโ๐) + 1)) โ โ) |
201 | | readdcl 11130 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง (logโ((โโ๐) + 1)) โ โ) โ (1 +
(logโ((โโ๐) + 1))) โ โ) |
202 | 43, 200, 201 | sylancr 587 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 +
(logโ((โโ๐) + 1))) โ โ) |
203 | | harmonicbnd 26337 |
. . . . . . . . . . . . . . . . . 18
โข
(((โโ๐)
+ 1) โ โ โ (ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) โ (logโ((โโ๐) + 1))) โ
(ฮณ[,]1)) |
204 | 84, 203 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) โ (logโ((โโ๐) + 1))) โ
(ฮณ[,]1)) |
205 | 169, 43 | elicc2i 13322 |
. . . . . . . . . . . . . . . . . 18
โข
((ฮฃ๐ โ
(1...((โโ๐) +
1))(1 / ๐) โ
(logโ((โโ๐) + 1))) โ (ฮณ[,]1) โ
((ฮฃ๐ โ
(1...((โโ๐) +
1))(1 / ๐) โ
(logโ((โโ๐) + 1))) โ โ โง ฮณ โค
(ฮฃ๐ โ
(1...((โโ๐) +
1))(1 / ๐) โ
(logโ((โโ๐) + 1))) โง (ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) โ (logโ((โโ๐) + 1))) โค
1)) |
206 | 205 | simp3bi 1147 |
. . . . . . . . . . . . . . . . 17
โข
((ฮฃ๐ โ
(1...((โโ๐) +
1))(1 / ๐) โ
(logโ((โโ๐) + 1))) โ (ฮณ[,]1) โ
(ฮฃ๐ โ
(1...((โโ๐) +
1))(1 / ๐) โ
(logโ((โโ๐) + 1))) โค 1) |
207 | 204, 206 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) โ (logโ((โโ๐) + 1))) โค
1) |
208 | 198, 200,
44 | lesubaddd 11748 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((ฮฃ๐ โ
(1...((โโ๐) +
1))(1 / ๐) โ
(logโ((โโ๐) + 1))) โค 1 โ ฮฃ๐ โ
(1...((โโ๐) +
1))(1 / ๐) โค (1 +
(logโ((โโ๐) + 1))))) |
209 | 207, 208 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข (๐ โ ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) โค (1 + (logโ((โโ๐) + 1)))) |
210 | | readdcl 11130 |
. . . . . . . . . . . . . . . . . 18
โข ((1
โ โ โง (logโ๐) โ โ) โ (1 +
(logโ๐)) โ
โ) |
211 | 43, 94, 210 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1 + (logโ๐)) โ
โ) |
212 | | peano2re 11324 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((โโ๐)
โ โ โ ((โโ๐) + 1) โ โ) |
213 | 145, 212 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((โโ๐) + 1) โ
โ) |
214 | 3, 65 | remulcld 11181 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (2 ยท ๐) โ
โ) |
215 | | epr 16082 |
. . . . . . . . . . . . . . . . . . . . . 22
โข e โ
โ+ |
216 | | rpmulcl 12930 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((e
โ โ+ โง ๐ โ โ+) โ (e
ยท ๐) โ
โ+) |
217 | 215, 93, 216 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (e ยท ๐) โ
โ+) |
218 | 217 | rpred 12949 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (e ยท ๐) โ
โ) |
219 | | flle 13696 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ
(โโ๐) โค
๐) |
220 | 65, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โโ๐) โค ๐) |
221 | 12, 10 | rpdivcld 12966 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (2 / ๐ธ) โ
โ+) |
222 | | efgt1 15990 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((2 /
๐ธ) โ
โ+ โ 1 < (expโ(2 / ๐ธ))) |
223 | 221, 222 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ 1 < (expโ(2 /
๐ธ))) |
224 | 223, 66 | breqtrrdi 5145 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ 1 < ๐) |
225 | 44, 70, 65, 224, 78 | lttrd 11312 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ 1 < ๐) |
226 | 44, 65, 225 | ltled 11299 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 1 โค ๐) |
227 | 145, 44, 65, 65, 220, 226 | le2addd 11770 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((โโ๐) + 1) โค (๐ + ๐)) |
228 | 112 | 2timesd 12392 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (2 ยท ๐) = (๐ + ๐)) |
229 | 227, 228 | breqtrrd 5131 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((โโ๐) + 1) โค (2 ยท ๐)) |
230 | | ere 15963 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข e โ
โ |
231 | | egt2lt3 16080 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (2 < e
โง e < 3) |
232 | 231 | simpli 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 <
e |
233 | 2, 230, 232 | ltleii 11274 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 2 โค
e |
234 | 233 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ 2 โค e) |
235 | 230 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ e โ
โ) |
236 | | lemul1 12003 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((2
โ โ โง e โ โ โง (๐ โ โ โง 0 < ๐)) โ (2 โค e โ (2
ยท ๐) โค (e
ยท ๐))) |
237 | 3, 235, 65, 79, 236 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (2 โค e โ (2
ยท ๐) โค (e
ยท ๐))) |
238 | 234, 237 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (2 ยท ๐) โค (e ยท ๐)) |
239 | 213, 214,
218, 229, 238 | letrd 11308 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((โโ๐) + 1) โค (e ยท ๐)) |
240 | 199, 217 | logled 25966 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((โโ๐) + 1) โค (e ยท ๐) โ
(logโ((โโ๐) + 1)) โค (logโ(e ยท ๐)))) |
241 | 239, 240 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(logโ((โโ๐) + 1)) โค (logโ(e ยท ๐))) |
242 | | relogmul 25931 |
. . . . . . . . . . . . . . . . . . . 20
โข ((e
โ โ+ โง ๐ โ โ+) โ
(logโ(e ยท ๐))
= ((logโe) + (logโ๐))) |
243 | 215, 93, 242 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (logโ(e ยท
๐)) = ((logโe) +
(logโ๐))) |
244 | | loge 25926 |
. . . . . . . . . . . . . . . . . . . 20
โข
(logโe) = 1 |
245 | 244 | oveq1i 7363 |
. . . . . . . . . . . . . . . . . . 19
โข
((logโe) + (logโ๐)) = (1 + (logโ๐)) |
246 | 243, 245 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (logโ(e ยท
๐)) = (1 + (logโ๐))) |
247 | 241, 246 | breqtrd 5129 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(logโ((โโ๐) + 1)) โค (1 + (logโ๐))) |
248 | 200, 211,
44, 247 | leadd2dd 11766 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 +
(logโ((โโ๐) + 1))) โค (1 + (1 + (logโ๐)))) |
249 | | df-2 12212 |
. . . . . . . . . . . . . . . . . 18
โข 2 = (1 +
1) |
250 | 249 | oveq1i 7363 |
. . . . . . . . . . . . . . . . 17
โข (2 +
(logโ๐)) = ((1 + 1) +
(logโ๐)) |
251 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 1 โ
โ) |
252 | 251, 251,
95 | addassd 11173 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((1 + 1) +
(logโ๐)) = (1 + (1 +
(logโ๐)))) |
253 | 250, 252 | eqtrid 2788 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 + (logโ๐)) = (1 + (1 + (logโ๐)))) |
254 | 248, 253 | breqtrrd 5131 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 +
(logโ((โโ๐) + 1))) โค (2 + (logโ๐))) |
255 | 198, 202,
109, 209, 254 | letrd 11308 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ (1...((โโ๐) + 1))(1 / ๐) โค (2 + (logโ๐))) |
256 | 197, 255 | eqbrtrrd 5127 |
. . . . . . . . . . . . 13
โข (๐ โ ฮฃ๐ โ (0...(โโ๐))(1 / (๐ + 1)) โค (2 + (logโ๐))) |
257 | 106, 109,
90, 256 | leadd1dd 11765 |
. . . . . . . . . . . 12
โข (๐ โ (ฮฃ๐ โ (0...(โโ๐))(1 / (๐ + 1)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))) โค ((2 + (logโ๐)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)))) |
258 | 99, 107, 110, 185, 257 | letrd 11308 |
. . . . . . . . . . 11
โข (๐ โ (logโ(๐พ ยท ๐)) โค ((2 + (logโ๐)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)))) |
259 | 97, 258 | eqbrtrrd 5127 |
. . . . . . . . . 10
โข (๐ โ ((logโ๐พ) + (logโ๐)) โค ((2 + (logโ๐)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)))) |
260 | 98, 109, 90 | lesubadd2d 11750 |
. . . . . . . . . 10
โข (๐ โ ((((logโ๐พ) + (logโ๐)) โ (2 + (logโ๐))) โค ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)) โ ((logโ๐พ) + (logโ๐)) โค ((2 + (logโ๐)) + ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))))) |
261 | 259, 260 | mpbird 256 |
. . . . . . . . 9
โข (๐ โ (((logโ๐พ) + (logโ๐)) โ (2 + (logโ๐))) โค ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))) |
262 | 96, 261 | eqbrtrrd 5127 |
. . . . . . . 8
โข (๐ โ ((logโ๐พ) โ 2) โค ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))) |
263 | 89 | recnd 11179 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (1 / (๐ + 1)) โ โ) |
264 | 62, 26, 263 | fsummulc2 15661 |
. . . . . . . . . 10
โข (๐ โ (๐ธ ยท ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))) = ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(๐ธ ยท (1 / (๐ + 1)))) |
265 | 6 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ธ โ โ) |
266 | 265 | recnd 11179 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ธ โ โ) |
267 | 88 | nncnd 12165 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ + 1) โ โ) |
268 | 88 | nnne0d 12199 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ + 1) โ 0) |
269 | 266, 267,
268 | divrecd 11930 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ธ / (๐ + 1)) = (๐ธ ยท (1 / (๐ + 1)))) |
270 | 265, 88 | nndivred 12203 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ธ / (๐ + 1)) โ โ) |
271 | 269, 270 | eqeltrrd 2839 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ธ ยท (1 / (๐ + 1))) โ โ) |
272 | 62, 271 | fsumrecl 15611 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(๐ธ ยท (1 / (๐ + 1))) โ โ) |
273 | 87 | nnrpd 12947 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ โ โ+) |
274 | | pntpbnd.r |
. . . . . . . . . . . . . . . . . 18
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
275 | 274 | pntrf 26895 |
. . . . . . . . . . . . . . . . 17
โข ๐
:โ+โถโ |
276 | 275 | ffvelcdmi 7030 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ+
โ (๐
โ๐) โ
โ) |
277 | 273, 276 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐
โ๐) โ โ) |
278 | 87, 88 | nnmulcld 12202 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ ยท (๐ + 1)) โ โ) |
279 | 277, 278 | nndivred 12203 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((๐
โ๐) / (๐ ยท (๐ + 1))) โ โ) |
280 | 279 | recnd 11179 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((๐
โ๐) / (๐ ยท (๐ + 1))) โ โ) |
281 | 280 | abscld 15313 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (absโ((๐
โ๐) / (๐ ยท (๐ + 1)))) โ โ) |
282 | 62, 281 | fsumrecl 15611 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(absโ((๐
โ๐) / (๐ ยท (๐ + 1)))) โ โ) |
283 | 277, 87 | nndivred 12203 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((๐
โ๐) / ๐) โ โ) |
284 | 283 | recnd 11179 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((๐
โ๐) / ๐) โ โ) |
285 | 284 | abscld 15313 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (absโ((๐
โ๐) / ๐)) โ โ) |
286 | 88 | nnrpd 12947 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ + 1) โ
โ+) |
287 | | pntpbnd1.3 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ยฌ โ๐ฆ โ โ ((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โง (absโ((๐
โ๐ฆ) / ๐ฆ)) โค ๐ธ)) |
288 | 287 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ยฌ โ๐ฆ โ โ ((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โง (absโ((๐
โ๐ฆ) / ๐ฆ)) โค ๐ธ)) |
289 | | elfzle1 13436 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐))) โ ((โโ๐) + 1) โค ๐) |
290 | 289 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((โโ๐) + 1) โค ๐) |
291 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ โ โ) |
292 | 291 | flcld 13695 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (โโ๐) โ โค) |
293 | 87 | nnzd 12522 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ โ โค) |
294 | | zltp1le 12549 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((โโ๐)
โ โค โง ๐
โ โค) โ ((โโ๐) < ๐ โ ((โโ๐) + 1) โค ๐)) |
295 | 292, 293,
294 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((โโ๐) < ๐ โ ((โโ๐) + 1) โค ๐)) |
296 | 290, 295 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (โโ๐) < ๐) |
297 | | fllt 13703 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โค) โ (๐ < ๐ โ (โโ๐) < ๐)) |
298 | 291, 293,
297 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ < ๐ โ (โโ๐) < ๐)) |
299 | 296, 298 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ < ๐) |
300 | | elfzle2 13437 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐))) โ ๐ โค (โโ(๐พ ยท ๐))) |
301 | 300 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ โค (โโ(๐พ ยท ๐))) |
302 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐พ ยท ๐) โ โ) |
303 | | flge 13702 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐พ ยท ๐) โ โ โง ๐ โ โค) โ (๐ โค (๐พ ยท ๐) โ ๐ โค (โโ(๐พ ยท ๐)))) |
304 | 302, 293,
303 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ โค (๐พ ยท ๐) โ ๐ โค (โโ(๐พ ยท ๐)))) |
305 | 301, 304 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ โค (๐พ ยท ๐)) |
306 | | breq2 5107 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = ๐ โ (๐ < ๐ฆ โ ๐ < ๐)) |
307 | | breq1 5106 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = ๐ โ (๐ฆ โค (๐พ ยท ๐) โ ๐ โค (๐พ ยท ๐))) |
308 | 306, 307 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = ๐ โ ((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โ (๐ < ๐ โง ๐ โค (๐พ ยท ๐)))) |
309 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ = ๐ โ (๐
โ๐ฆ) = (๐
โ๐)) |
310 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ = ๐ โ ๐ฆ = ๐) |
311 | 309, 310 | oveq12d 7371 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ = ๐ โ ((๐
โ๐ฆ) / ๐ฆ) = ((๐
โ๐) / ๐)) |
312 | 311 | fveq2d 6843 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = ๐ โ (absโ((๐
โ๐ฆ) / ๐ฆ)) = (absโ((๐
โ๐) / ๐))) |
313 | 312 | breq1d 5113 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = ๐ โ ((absโ((๐
โ๐ฆ) / ๐ฆ)) โค ๐ธ โ (absโ((๐
โ๐) / ๐)) โค ๐ธ)) |
314 | 308, 313 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ = ๐ โ (((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โง (absโ((๐
โ๐ฆ) / ๐ฆ)) โค ๐ธ) โ ((๐ < ๐ โง ๐ โค (๐พ ยท ๐)) โง (absโ((๐
โ๐) / ๐)) โค ๐ธ))) |
315 | 314 | rspcev 3579 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ((๐ < ๐ โง ๐ โค (๐พ ยท ๐)) โง (absโ((๐
โ๐) / ๐)) โค ๐ธ)) โ โ๐ฆ โ โ ((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โง (absโ((๐
โ๐ฆ) / ๐ฆ)) โค ๐ธ)) |
316 | 315 | expr 457 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (๐ < ๐ โง ๐ โค (๐พ ยท ๐))) โ ((absโ((๐
โ๐) / ๐)) โค ๐ธ โ โ๐ฆ โ โ ((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โง (absโ((๐
โ๐ฆ) / ๐ฆ)) โค ๐ธ))) |
317 | 87, 299, 305, 316 | syl12anc 835 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((absโ((๐
โ๐) / ๐)) โค ๐ธ โ โ๐ฆ โ โ ((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โง (absโ((๐
โ๐ฆ) / ๐ฆ)) โค ๐ธ))) |
318 | 288, 317 | mtod 197 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ยฌ (absโ((๐
โ๐) / ๐)) โค ๐ธ) |
319 | 285, 265 | letrid 11303 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((absโ((๐
โ๐) / ๐)) โค ๐ธ โจ ๐ธ โค (absโ((๐
โ๐) / ๐)))) |
320 | 319 | ord 862 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (ยฌ (absโ((๐
โ๐) / ๐)) โค ๐ธ โ ๐ธ โค (absโ((๐
โ๐) / ๐)))) |
321 | 318, 320 | mpd 15 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ธ โค (absโ((๐
โ๐) / ๐))) |
322 | 265, 285,
286, 321 | lediv1dd 13007 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ธ / (๐ + 1)) โค ((absโ((๐
โ๐) / ๐)) / (๐ + 1))) |
323 | 284, 267,
268 | absdivd 15332 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (absโ(((๐
โ๐) / ๐) / (๐ + 1))) = ((absโ((๐
โ๐) / ๐)) / (absโ(๐ + 1)))) |
324 | 277 | recnd 11179 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐
โ๐) โ โ) |
325 | 87 | nncnd 12165 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ โ โ) |
326 | 87 | nnne0d 12199 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ๐ โ 0) |
327 | 324, 325,
267, 326, 268 | divdiv1d 11958 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (((๐
โ๐) / ๐) / (๐ + 1)) = ((๐
โ๐) / (๐ ยท (๐ + 1)))) |
328 | 327 | fveq2d 6843 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (absโ(((๐
โ๐) / ๐) / (๐ + 1))) = (absโ((๐
โ๐) / (๐ ยท (๐ + 1))))) |
329 | 286 | rprege0d 12956 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((๐ + 1) โ โ โง 0 โค (๐ + 1))) |
330 | | absid 15173 |
. . . . . . . . . . . . . . . 16
โข (((๐ + 1) โ โ โง 0
โค (๐ + 1)) โ
(absโ(๐ + 1)) =
(๐ + 1)) |
331 | 329, 330 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (absโ(๐ + 1)) = (๐ + 1)) |
332 | 331 | oveq2d 7369 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((absโ((๐
โ๐) / ๐)) / (absโ(๐ + 1))) = ((absโ((๐
โ๐) / ๐)) / (๐ + 1))) |
333 | 323, 328,
332 | 3eqtr3rd 2785 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ ((absโ((๐
โ๐) / ๐)) / (๐ + 1)) = (absโ((๐
โ๐) / (๐ ยท (๐ + 1))))) |
334 | 322, 269,
333 | 3brtr3d 5134 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))) โ (๐ธ ยท (1 / (๐ + 1))) โค (absโ((๐
โ๐) / (๐ ยท (๐ + 1))))) |
335 | 62, 271, 281, 334 | fsumle 15676 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(๐ธ ยท (1 / (๐ + 1))) โค ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(absโ((๐
โ๐) / (๐ ยท (๐ + 1))))) |
336 | | pntpbnd1.2 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ โ โ๐ โ โค (absโฮฃ๐ฆ โ (๐...๐)((๐
โ๐ฆ) / (๐ฆ ยท (๐ฆ + 1)))) โค ๐ด) |
337 | 274, 5, 66, 64, 15, 336, 13, 36, 287 | pntpbnd1 26918 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(absโ((๐
โ๐) / (๐ ยท (๐ + 1)))) โค ๐ด) |
338 | 272, 282,
32, 335, 337 | letrd 11308 |
. . . . . . . . . 10
โข (๐ โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(๐ธ ยท (1 / (๐ + 1))) โค ๐ด) |
339 | 264, 338 | eqbrtrd 5125 |
. . . . . . . . 9
โข (๐ โ (๐ธ ยท ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))) โค ๐ด) |
340 | 90, 32, 10 | lemuldiv2d 12999 |
. . . . . . . . 9
โข (๐ โ ((๐ธ ยท ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1))) โค ๐ด โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)) โค (๐ด / ๐ธ))) |
341 | 339, 340 | mpbid 231 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(1 / (๐ + 1)) โค (๐ด / ๐ธ)) |
342 | 55, 90, 33, 262, 341 | letrd 11308 |
. . . . . . 7
โข (๐ โ ((logโ๐พ) โ 2) โค (๐ด / ๐ธ)) |
343 | 35, 55, 33, 61, 342 | letrd 11308 |
. . . . . 6
โข (๐ โ ((๐ถ / ๐ธ) โ 2) โค (๐ด / ๐ธ)) |
344 | 31, 3, 33, 343 | subled 11754 |
. . . . 5
โข (๐ โ ((๐ถ / ๐ธ) โ (๐ด / ๐ธ)) โค 2) |
345 | 29, 344 | eqbrtrd 5125 |
. . . 4
โข (๐ โ (2 / ๐ธ) โค 2) |
346 | 3, 10, 12, 345 | lediv23d 13017 |
. . 3
โข (๐ โ (2 / 2) โค ๐ธ) |
347 | 1, 346 | eqbrtrrid 5139 |
. 2
โข (๐ โ 1 โค ๐ธ) |
348 | 8 | simprd 496 |
. . 3
โข (๐ โ ๐ธ < 1) |
349 | | ltnle 11230 |
. . . 4
โข ((๐ธ โ โ โง 1 โ
โ) โ (๐ธ < 1
โ ยฌ 1 โค ๐ธ)) |
350 | 6, 43, 349 | sylancl 586 |
. . 3
โข (๐ โ (๐ธ < 1 โ ยฌ 1 โค ๐ธ)) |
351 | 348, 350 | mpbid 231 |
. 2
โข (๐ โ ยฌ 1 โค ๐ธ) |
352 | 347, 351 | pm2.65i 193 |
1
โข ยฌ
๐ |