Step | Hyp | Ref
| Expression |
1 | | 2re 12232 |
. . . . 5
โข 2 โ
โ |
2 | | fzfid 13884 |
. . . . . 6
โข (๐ โ (1...(โโ(๐ / ๐))) โ Fin) |
3 | | elfznn 13476 |
. . . . . . . . . 10
โข (๐ โ
(1...(โโ(๐ /
๐))) โ ๐ โ
โ) |
4 | 3 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ ๐ โ โ) |
5 | 4 | nnrpd 12960 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ ๐ โ โ+) |
6 | 5 | relogcld 25994 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ (logโ๐) โ โ) |
7 | 6, 4 | nndivred 12212 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ ((logโ๐) / ๐) โ โ) |
8 | 2, 7 | fsumrecl 15624 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (1...(โโ(๐ / ๐)))((logโ๐) / ๐) โ โ) |
9 | | remulcl 11141 |
. . . . 5
โข ((2
โ โ โง ฮฃ๐ โ (1...(โโ(๐ / ๐)))((logโ๐) / ๐) โ โ) โ (2 ยท
ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)) โ โ) |
10 | 1, 8, 9 | sylancr 588 |
. . . 4
โข (๐ โ (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)) โ โ) |
11 | | pntlem1.r |
. . . . . . . . 9
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
12 | | pntlem1.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ
โ+) |
13 | | pntlem1.b |
. . . . . . . . 9
โข (๐ โ ๐ต โ
โ+) |
14 | | pntlem1.l |
. . . . . . . . 9
โข (๐ โ ๐ฟ โ (0(,)1)) |
15 | | pntlem1.d |
. . . . . . . . 9
โข ๐ท = (๐ด + 1) |
16 | | pntlem1.f |
. . . . . . . . 9
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
17 | | pntlem1.u |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ+) |
18 | | pntlem1.u2 |
. . . . . . . . 9
โข (๐ โ ๐ โค ๐ด) |
19 | | pntlem1.e |
. . . . . . . . 9
โข ๐ธ = (๐ / ๐ท) |
20 | | pntlem1.k |
. . . . . . . . 9
โข ๐พ = (expโ(๐ต / ๐ธ)) |
21 | | pntlem1.y |
. . . . . . . . 9
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
22 | | pntlem1.x |
. . . . . . . . 9
โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) |
23 | | pntlem1.c |
. . . . . . . . 9
โข (๐ โ ๐ถ โ
โ+) |
24 | | pntlem1.w |
. . . . . . . . 9
โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
25 | | pntlem1.z |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐[,)+โ)) |
26 | 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25 | pntlemb 26961 |
. . . . . . . 8
โข (๐ โ (๐ โ โ+ โง (1 <
๐ โง e โค
(โโ๐) โง
(โโ๐) โค
(๐ / ๐)) โง ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐))))) |
27 | 26 | simp1d 1143 |
. . . . . . 7
โข (๐ โ ๐ โ
โ+) |
28 | 27 | relogcld 25994 |
. . . . . 6
โข (๐ โ (logโ๐) โ
โ) |
29 | | peano2re 11333 |
. . . . . 6
โข
((logโ๐)
โ โ โ ((logโ๐) + 1) โ โ) |
30 | 28, 29 | syl 17 |
. . . . 5
โข (๐ โ ((logโ๐) + 1) โ
โ) |
31 | 30 | resqcld 14036 |
. . . 4
โข (๐ โ (((logโ๐) + 1)โ2) โ
โ) |
32 | | 3re 12238 |
. . . . . 6
โข 3 โ
โ |
33 | | readdcl 11139 |
. . . . . 6
โข
(((logโ๐)
โ โ โง 3 โ โ) โ ((logโ๐) + 3) โ โ) |
34 | 28, 32, 33 | sylancl 587 |
. . . . 5
โข (๐ โ ((logโ๐) + 3) โ
โ) |
35 | 34, 28 | remulcld 11190 |
. . . 4
โข (๐ โ (((logโ๐) + 3) ยท (logโ๐)) โ
โ) |
36 | 27 | rpred 12962 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
37 | 21 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ+) |
38 | 36, 37 | rerpdivcld 12993 |
. . . . . . . . . 10
โข (๐ โ (๐ / ๐) โ โ) |
39 | | 1red 11161 |
. . . . . . . . . . 11
โข (๐ โ 1 โ
โ) |
40 | 27 | rpsqrtcld 15302 |
. . . . . . . . . . . 12
โข (๐ โ (โโ๐) โ
โ+) |
41 | 40 | rpred 12962 |
. . . . . . . . . . 11
โข (๐ โ (โโ๐) โ
โ) |
42 | | ere 15976 |
. . . . . . . . . . . . 13
โข e โ
โ |
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ e โ
โ) |
44 | | 1re 11160 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
45 | | 1lt2 12329 |
. . . . . . . . . . . . . . 15
โข 1 <
2 |
46 | | egt2lt3 16093 |
. . . . . . . . . . . . . . . 16
โข (2 < e
โง e < 3) |
47 | 46 | simpli 485 |
. . . . . . . . . . . . . . 15
โข 2 <
e |
48 | 44, 1, 42 | lttri 11286 |
. . . . . . . . . . . . . . 15
โข ((1 <
2 โง 2 < e) โ 1 < e) |
49 | 45, 47, 48 | mp2an 691 |
. . . . . . . . . . . . . 14
โข 1 <
e |
50 | 44, 42, 49 | ltleii 11283 |
. . . . . . . . . . . . 13
โข 1 โค
e |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 1 โค e) |
52 | 26 | simp2d 1144 |
. . . . . . . . . . . . 13
โข (๐ โ (1 < ๐ โง e โค (โโ๐) โง (โโ๐) โค (๐ / ๐))) |
53 | 52 | simp2d 1144 |
. . . . . . . . . . . 12
โข (๐ โ e โค
(โโ๐)) |
54 | 39, 43, 41, 51, 53 | letrd 11317 |
. . . . . . . . . . 11
โข (๐ โ 1 โค
(โโ๐)) |
55 | 52 | simp3d 1145 |
. . . . . . . . . . 11
โข (๐ โ (โโ๐) โค (๐ / ๐)) |
56 | 39, 41, 38, 54, 55 | letrd 11317 |
. . . . . . . . . 10
โข (๐ โ 1 โค (๐ / ๐)) |
57 | | flge1nn 13732 |
. . . . . . . . . 10
โข (((๐ / ๐) โ โ โง 1 โค (๐ / ๐)) โ (โโ(๐ / ๐)) โ โ) |
58 | 38, 56, 57 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (โโ(๐ / ๐)) โ โ) |
59 | 58 | nnrpd 12960 |
. . . . . . . 8
โข (๐ โ (โโ(๐ / ๐)) โ
โ+) |
60 | 59 | relogcld 25994 |
. . . . . . 7
โข (๐ โ
(logโ(โโ(๐ / ๐))) โ โ) |
61 | 60, 39 | readdcld 11189 |
. . . . . 6
โข (๐ โ
((logโ(โโ(๐ / ๐))) + 1) โ โ) |
62 | 61 | resqcld 14036 |
. . . . 5
โข (๐ โ
(((logโ(โโ(๐ / ๐))) + 1)โ2) โ
โ) |
63 | | logdivbnd 26920 |
. . . . . . 7
โข
((โโ(๐ /
๐)) โ โ โ
ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐) โค ((((logโ(โโ(๐ / ๐))) + 1)โ2) / 2)) |
64 | 58, 63 | syl 17 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (1...(โโ(๐ / ๐)))((logโ๐) / ๐) โค ((((logโ(โโ(๐ / ๐))) + 1)โ2) / 2)) |
65 | 1 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ
โ) |
66 | | 2pos 12261 |
. . . . . . . 8
โข 0 <
2 |
67 | 66 | a1i 11 |
. . . . . . 7
โข (๐ โ 0 < 2) |
68 | | lemuldiv2 12041 |
. . . . . . 7
โข
((ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐) โ โ โง
(((logโ(โโ(๐ / ๐))) + 1)โ2) โ โ โง (2
โ โ โง 0 < 2)) โ ((2 ยท ฮฃ๐ โ (1...(โโ(๐ / ๐)))((logโ๐) / ๐)) โค (((logโ(โโ(๐ / ๐))) + 1)โ2) โ ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐) โค ((((logโ(โโ(๐ / ๐))) + 1)โ2) / 2))) |
69 | 8, 62, 65, 67, 68 | syl112anc 1375 |
. . . . . 6
โข (๐ โ ((2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)) โค (((logโ(โโ(๐ / ๐))) + 1)โ2) โ ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐) โค ((((logโ(โโ(๐ / ๐))) + 1)โ2) / 2))) |
70 | 64, 69 | mpbird 257 |
. . . . 5
โข (๐ โ (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)) โค (((logโ(โโ(๐ / ๐))) + 1)โ2)) |
71 | | reflcl 13707 |
. . . . . . . . . 10
โข ((๐ / ๐) โ โ โ
(โโ(๐ / ๐)) โ
โ) |
72 | 38, 71 | syl 17 |
. . . . . . . . 9
โข (๐ โ (โโ(๐ / ๐)) โ โ) |
73 | | flle 13710 |
. . . . . . . . . 10
โข ((๐ / ๐) โ โ โ
(โโ(๐ / ๐)) โค (๐ / ๐)) |
74 | 38, 73 | syl 17 |
. . . . . . . . 9
โข (๐ โ (โโ(๐ / ๐)) โค (๐ / ๐)) |
75 | 21 | simprd 497 |
. . . . . . . . . . 11
โข (๐ โ 1 โค ๐) |
76 | | 1rp 12924 |
. . . . . . . . . . . . 13
โข 1 โ
โ+ |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ
โ+) |
78 | 77, 37, 27 | lediv2d 12986 |
. . . . . . . . . . 11
โข (๐ โ (1 โค ๐ โ (๐ / ๐) โค (๐ / 1))) |
79 | 75, 78 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (๐ / ๐) โค (๐ / 1)) |
80 | 36 | recnd 11188 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
81 | 80 | div1d 11928 |
. . . . . . . . . 10
โข (๐ โ (๐ / 1) = ๐) |
82 | 79, 81 | breqtrd 5132 |
. . . . . . . . 9
โข (๐ โ (๐ / ๐) โค ๐) |
83 | 72, 38, 36, 74, 82 | letrd 11317 |
. . . . . . . 8
โข (๐ โ (โโ(๐ / ๐)) โค ๐) |
84 | 59, 27 | logled 25998 |
. . . . . . . 8
โข (๐ โ ((โโ(๐ / ๐)) โค ๐ โ (logโ(โโ(๐ / ๐))) โค (logโ๐))) |
85 | 83, 84 | mpbid 231 |
. . . . . . 7
โข (๐ โ
(logโ(โโ(๐ / ๐))) โค (logโ๐)) |
86 | 60, 28, 39, 85 | leadd1dd 11774 |
. . . . . 6
โข (๐ โ
((logโ(โโ(๐ / ๐))) + 1) โค ((logโ๐) + 1)) |
87 | | 0red 11163 |
. . . . . . . 8
โข (๐ โ 0 โ
โ) |
88 | | log1 25957 |
. . . . . . . . 9
โข
(logโ1) = 0 |
89 | 58 | nnge1d 12206 |
. . . . . . . . . 10
โข (๐ โ 1 โค
(โโ(๐ / ๐))) |
90 | | logleb 25974 |
. . . . . . . . . . 11
โข ((1
โ โ+ โง (โโ(๐ / ๐)) โ โ+) โ (1
โค (โโ(๐ /
๐)) โ (logโ1)
โค (logโ(โโ(๐ / ๐))))) |
91 | 76, 59, 90 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (1 โค
(โโ(๐ / ๐)) โ (logโ1) โค
(logโ(โโ(๐ / ๐))))) |
92 | 89, 91 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (logโ1) โค
(logโ(โโ(๐ / ๐)))) |
93 | 88, 92 | eqbrtrrid 5142 |
. . . . . . . 8
โข (๐ โ 0 โค
(logโ(โโ(๐ / ๐)))) |
94 | 60 | lep1d 12091 |
. . . . . . . 8
โข (๐ โ
(logโ(โโ(๐ / ๐))) โค ((logโ(โโ(๐ / ๐))) + 1)) |
95 | 87, 60, 61, 93, 94 | letrd 11317 |
. . . . . . 7
โข (๐ โ 0 โค
((logโ(โโ(๐ / ๐))) + 1)) |
96 | 87, 61, 30, 95, 86 | letrd 11317 |
. . . . . . 7
โข (๐ โ 0 โค ((logโ๐) + 1)) |
97 | 61, 30, 95, 96 | le2sqd 14166 |
. . . . . 6
โข (๐ โ
(((logโ(โโ(๐ / ๐))) + 1) โค ((logโ๐) + 1) โ
(((logโ(โโ(๐ / ๐))) + 1)โ2) โค (((logโ๐) +
1)โ2))) |
98 | 86, 97 | mpbid 231 |
. . . . 5
โข (๐ โ
(((logโ(โโ(๐ / ๐))) + 1)โ2) โค (((logโ๐) + 1)โ2)) |
99 | 10, 62, 31, 70, 98 | letrd 11317 |
. . . 4
โข (๐ โ (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)) โค (((logโ๐) + 1)โ2)) |
100 | 28 | resqcld 14036 |
. . . . . . 7
โข (๐ โ ((logโ๐)โ2) โ
โ) |
101 | 65, 28 | remulcld 11190 |
. . . . . . 7
โข (๐ โ (2 ยท
(logโ๐)) โ
โ) |
102 | 100, 101 | readdcld 11189 |
. . . . . 6
โข (๐ โ (((logโ๐)โ2) + (2 ยท
(logโ๐))) โ
โ) |
103 | | loge 25958 |
. . . . . . 7
โข
(logโe) = 1 |
104 | 40 | rpge0d 12966 |
. . . . . . . . . . 11
โข (๐ โ 0 โค
(โโ๐)) |
105 | 41, 41, 104, 54 | lemulge12d 12098 |
. . . . . . . . . 10
โข (๐ โ (โโ๐) โค ((โโ๐) ยท (โโ๐))) |
106 | 27 | rprege0d 12969 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โ โง 0 โค ๐)) |
107 | | remsqsqrt 15147 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 0 โค
๐) โ
((โโ๐) ยท
(โโ๐)) = ๐) |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((โโ๐) ยท (โโ๐)) = ๐) |
109 | 105, 108 | breqtrd 5132 |
. . . . . . . . 9
โข (๐ โ (โโ๐) โค ๐) |
110 | 43, 41, 36, 53, 109 | letrd 11317 |
. . . . . . . 8
โข (๐ โ e โค ๐) |
111 | | epr 16095 |
. . . . . . . . 9
โข e โ
โ+ |
112 | | logleb 25974 |
. . . . . . . . 9
โข ((e
โ โ+ โง ๐ โ โ+) โ (e โค
๐ โ (logโe) โค
(logโ๐))) |
113 | 111, 27, 112 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (e โค ๐ โ (logโe) โค (logโ๐))) |
114 | 110, 113 | mpbid 231 |
. . . . . . 7
โข (๐ โ (logโe) โค
(logโ๐)) |
115 | 103, 114 | eqbrtrrid 5142 |
. . . . . 6
โข (๐ โ 1 โค (logโ๐)) |
116 | 39, 28, 102, 115 | leadd2dd 11775 |
. . . . 5
โข (๐ โ ((((logโ๐)โ2) + (2 ยท
(logโ๐))) + 1) โค
((((logโ๐)โ2) +
(2 ยท (logโ๐)))
+ (logโ๐))) |
117 | 28 | recnd 11188 |
. . . . . 6
โข (๐ โ (logโ๐) โ
โ) |
118 | | binom21 14128 |
. . . . . 6
โข
((logโ๐)
โ โ โ (((logโ๐) + 1)โ2) = ((((logโ๐)โ2) + (2 ยท
(logโ๐))) +
1)) |
119 | 117, 118 | syl 17 |
. . . . 5
โข (๐ โ (((logโ๐) + 1)โ2) =
((((logโ๐)โ2) +
(2 ยท (logโ๐)))
+ 1)) |
120 | 117 | sqvald 14054 |
. . . . . . 7
โข (๐ โ ((logโ๐)โ2) = ((logโ๐) ยท (logโ๐))) |
121 | | df-3 12222 |
. . . . . . . . . 10
โข 3 = (2 +
1) |
122 | 121 | oveq1i 7368 |
. . . . . . . . 9
โข (3
ยท (logโ๐)) =
((2 + 1) ยท (logโ๐)) |
123 | | 2cnd 12236 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
124 | | 1cnd 11155 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
125 | 123, 124,
117 | adddird 11185 |
. . . . . . . . 9
โข (๐ โ ((2 + 1) ยท
(logโ๐)) = ((2
ยท (logโ๐)) +
(1 ยท (logโ๐)))) |
126 | 122, 125 | eqtrid 2785 |
. . . . . . . 8
โข (๐ โ (3 ยท
(logโ๐)) = ((2
ยท (logโ๐)) +
(1 ยท (logโ๐)))) |
127 | 117 | mulid2d 11178 |
. . . . . . . . 9
โข (๐ โ (1 ยท
(logโ๐)) =
(logโ๐)) |
128 | 127 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ ((2 ยท
(logโ๐)) + (1
ยท (logโ๐))) =
((2 ยท (logโ๐))
+ (logโ๐))) |
129 | 126, 128 | eqtr2d 2774 |
. . . . . . 7
โข (๐ โ ((2 ยท
(logโ๐)) +
(logโ๐)) = (3
ยท (logโ๐))) |
130 | 120, 129 | oveq12d 7376 |
. . . . . 6
โข (๐ โ (((logโ๐)โ2) + ((2 ยท
(logโ๐)) +
(logโ๐))) =
(((logโ๐) ยท
(logโ๐)) + (3
ยท (logโ๐)))) |
131 | 117 | sqcld 14055 |
. . . . . . 7
โข (๐ โ ((logโ๐)โ2) โ
โ) |
132 | | 2cn 12233 |
. . . . . . . 8
โข 2 โ
โ |
133 | | mulcl 11140 |
. . . . . . . 8
โข ((2
โ โ โง (logโ๐) โ โ) โ (2 ยท
(logโ๐)) โ
โ) |
134 | 132, 117,
133 | sylancr 588 |
. . . . . . 7
โข (๐ โ (2 ยท
(logโ๐)) โ
โ) |
135 | 131, 134,
117 | addassd 11182 |
. . . . . 6
โข (๐ โ ((((logโ๐)โ2) + (2 ยท
(logโ๐))) +
(logโ๐)) =
(((logโ๐)โ2) +
((2 ยท (logโ๐))
+ (logโ๐)))) |
136 | | 3cn 12239 |
. . . . . . . 8
โข 3 โ
โ |
137 | 136 | a1i 11 |
. . . . . . 7
โข (๐ โ 3 โ
โ) |
138 | 117, 137,
117 | adddird 11185 |
. . . . . 6
โข (๐ โ (((logโ๐) + 3) ยท (logโ๐)) = (((logโ๐) ยท (logโ๐)) + (3 ยท
(logโ๐)))) |
139 | 130, 135,
138 | 3eqtr4rd 2784 |
. . . . 5
โข (๐ โ (((logโ๐) + 3) ยท (logโ๐)) = ((((logโ๐)โ2) + (2 ยท
(logโ๐))) +
(logโ๐))) |
140 | 116, 119,
139 | 3brtr4d 5138 |
. . . 4
โข (๐ โ (((logโ๐) + 1)โ2) โค
(((logโ๐) + 3)
ยท (logโ๐))) |
141 | 10, 31, 35, 99, 140 | letrd 11317 |
. . 3
โข (๐ โ (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)) โค (((logโ๐) + 3) ยท (logโ๐))) |
142 | 10, 35, 17 | lemul2d 13006 |
. . 3
โข (๐ โ ((2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)) โค (((logโ๐) + 3) ยท (logโ๐)) โ (๐ ยท (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐))) โค (๐ ยท (((logโ๐) + 3) ยท (logโ๐))))) |
143 | 141, 142 | mpbid 231 |
. 2
โข (๐ โ (๐ ยท (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐))) โค (๐ ยท (((logโ๐) + 3) ยท (logโ๐)))) |
144 | 17 | rpred 12962 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
145 | 144 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ ๐ โ โ) |
146 | 145 | recnd 11188 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ ๐ โ โ) |
147 | 6 | recnd 11188 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ (logโ๐) โ โ) |
148 | 5 | rpcnne0d 12971 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ (๐ โ โ โง ๐ โ 0)) |
149 | | div23 11837 |
. . . . . . . 8
โข ((๐ โ โ โง
(logโ๐) โ
โ โง (๐ โ
โ โง ๐ โ 0))
โ ((๐ ยท
(logโ๐)) / ๐) = ((๐ / ๐) ยท (logโ๐))) |
150 | | divass 11836 |
. . . . . . . 8
โข ((๐ โ โ โง
(logโ๐) โ
โ โง (๐ โ
โ โง ๐ โ 0))
โ ((๐ ยท
(logโ๐)) / ๐) = (๐ ยท ((logโ๐) / ๐))) |
151 | 149, 150 | eqtr3d 2775 |
. . . . . . 7
โข ((๐ โ โ โง
(logโ๐) โ
โ โง (๐ โ
โ โง ๐ โ 0))
โ ((๐ / ๐) ยท (logโ๐)) = (๐ ยท ((logโ๐) / ๐))) |
152 | 146, 147,
148, 151 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ ((๐ / ๐) ยท (logโ๐)) = (๐ ยท ((logโ๐) / ๐))) |
153 | 152 | sumeq2dv 15593 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (1...(โโ(๐ / ๐)))((๐ / ๐) ยท (logโ๐)) = ฮฃ๐ โ (1...(โโ(๐ / ๐)))(๐ ยท ((logโ๐) / ๐))) |
154 | 144 | recnd 11188 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
155 | 7 | recnd 11188 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ(๐ / ๐)))) โ ((logโ๐) / ๐) โ โ) |
156 | 2, 154, 155 | fsummulc2 15674 |
. . . . 5
โข (๐ โ (๐ ยท ฮฃ๐ โ (1...(โโ(๐ / ๐)))((logโ๐) / ๐)) = ฮฃ๐ โ (1...(โโ(๐ / ๐)))(๐ ยท ((logโ๐) / ๐))) |
157 | 153, 156 | eqtr4d 2776 |
. . . 4
โข (๐ โ ฮฃ๐ โ (1...(โโ(๐ / ๐)))((๐ / ๐) ยท (logโ๐)) = (๐ ยท ฮฃ๐ โ (1...(โโ(๐ / ๐)))((logโ๐) / ๐))) |
158 | 157 | oveq2d 7374 |
. . 3
โข (๐ โ (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((๐ / ๐) ยท (logโ๐))) = (2 ยท (๐ ยท ฮฃ๐ โ (1...(โโ(๐ / ๐)))((logโ๐) / ๐)))) |
159 | 8 | recnd 11188 |
. . . 4
โข (๐ โ ฮฃ๐ โ (1...(โโ(๐ / ๐)))((logโ๐) / ๐) โ โ) |
160 | 123, 154,
159 | mul12d 11369 |
. . 3
โข (๐ โ (2 ยท (๐ ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐))) = (๐ ยท (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)))) |
161 | 158, 160 | eqtrd 2773 |
. 2
โข (๐ โ (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((๐ / ๐) ยท (logโ๐))) = (๐ ยท (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((logโ๐) / ๐)))) |
162 | 34 | recnd 11188 |
. . 3
โข (๐ โ ((logโ๐) + 3) โ
โ) |
163 | 154, 162,
117 | mulassd 11183 |
. 2
โข (๐ โ ((๐ ยท ((logโ๐) + 3)) ยท (logโ๐)) = (๐ ยท (((logโ๐) + 3) ยท (logโ๐)))) |
164 | 143, 161,
163 | 3brtr4d 5138 |
1
โข (๐ โ (2 ยท ฮฃ๐ โ
(1...(โโ(๐ /
๐)))((๐ / ๐) ยท (logโ๐))) โค ((๐ ยท ((logโ๐) + 3)) ยท (logโ๐))) |