Step | Hyp | Ref
| Expression |
1 | | vmalogdivsum2 26902 |
. . 3
โข (๐ฅ โ (1(,)+โ) โฆ
((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) โ ๐(1) |
2 | 1 | a1i 11 |
. 2
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) โ
๐(1)) |
3 | | fzfid 13885 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(1...(โโ๐ฅ))
โ Fin) |
4 | | elfznn 13477 |
. . . . . . . . . . 11
โข (๐ โ
(1...(โโ๐ฅ))
โ ๐ โ
โ) |
5 | 4 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ) |
6 | | vmacl 26483 |
. . . . . . . . . 10
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮโ๐)
โ โ) |
8 | 7, 5 | nndivred 12214 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
/ ๐) โ
โ) |
9 | | fzfid 13885 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (1...(โโ(๐ฅ / ๐))) โ Fin) |
10 | | elfznn 13477 |
. . . . . . . . . . . 12
โข (๐ โ
(1...(โโ(๐ฅ /
๐))) โ ๐ โ
โ) |
11 | 10 | adantl 483 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ ๐ โ
โ) |
12 | | vmacl 26483 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ
(ฮโ๐) โ
โ) |
14 | 13, 11 | nndivred 12214 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ
((ฮโ๐) / ๐) โ
โ) |
15 | 9, 14 | fsumrecl 15626 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ โ) |
16 | 8, 15 | remulcld 11192 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐)) โ โ) |
17 | 3, 16 | fsumrecl 15626 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ โ) |
18 | | elioore 13301 |
. . . . . . . 8
โข (๐ฅ โ (1(,)+โ) โ
๐ฅ โ
โ) |
19 | 18 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ฅ โ
โ) |
20 | | eliooord 13330 |
. . . . . . . . 9
โข (๐ฅ โ (1(,)+โ) โ (1
< ๐ฅ โง ๐ฅ <
+โ)) |
21 | 20 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (1 < ๐ฅ โง ๐ฅ < +โ)) |
22 | 21 | simpld 496 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 < ๐ฅ) |
23 | 19, 22 | rplogcld 26000 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(logโ๐ฅ) โ
โ+) |
24 | 17, 23 | rerpdivcld 12995 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ โ) |
25 | | 1rp 12926 |
. . . . . . . . 9
โข 1 โ
โ+ |
26 | 25 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 โ
โ+) |
27 | | 1red 11163 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 โ
โ) |
28 | 27, 19, 22 | ltled 11310 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 โค ๐ฅ) |
29 | 19, 26, 28 | rpgecld 13003 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ฅ โ
โ+) |
30 | 29 | relogcld 25994 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(logโ๐ฅ) โ
โ) |
31 | 30 | rehalfcld 12407 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((logโ๐ฅ) / 2) โ
โ) |
32 | 24, 31 | resubcld 11590 |
. . . 4
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ โ) |
33 | 32 | recnd 11190 |
. . 3
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ โ) |
34 | 29 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ฅ โ
โ+) |
35 | 5 | nnrpd 12962 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ+) |
36 | 34, 35 | rpdivcld 12981 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ฅ / ๐) โ
โ+) |
37 | 36 | relogcld 25994 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (logโ(๐ฅ /
๐)) โ
โ) |
38 | 8, 37 | remulcld 11192 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท
(logโ(๐ฅ / ๐))) โ
โ) |
39 | 3, 38 | fsumrecl 15626 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) โ โ) |
40 | 39, 23 | rerpdivcld 12995 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ โ) |
41 | 40, 31 | resubcld 11590 |
. . . 4
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ โ) |
42 | 41 | recnd 11190 |
. . 3
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ โ) |
43 | 17 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ โ) |
44 | 39 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) โ โ) |
45 | 30 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(logโ๐ฅ) โ
โ) |
46 | 23 | rpne0d 12969 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(logโ๐ฅ) โ
0) |
47 | 43, 44, 45, 46 | divsubdird 11977 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) / (logโ๐ฅ)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)))) |
48 | 8 | recnd 11190 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
/ ๐) โ
โ) |
49 | 15 | recnd 11190 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ โ) |
50 | 37 | recnd 11190 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (logโ(๐ฅ /
๐)) โ
โ) |
51 | 48, 49, 50 | subdid 11618 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) = ((((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) |
52 | 51 | sumeq2dv 15595 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) = ฮฃ๐ โ (1...(โโ๐ฅ))((((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) |
53 | 16 | recnd 11190 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐)) โ โ) |
54 | 38 | recnd 11190 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท
(logโ(๐ฅ / ๐))) โ
โ) |
55 | 3, 53, 54 | fsumsub 15680 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) = (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) |
56 | 52, 55 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) = (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) |
57 | 56 | oveq1d 7377 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) โ ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) |
58 | 24 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ โ) |
59 | 40 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ โ) |
60 | 31 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((logโ๐ฅ) / 2) โ
โ) |
61 | 58, 59, 60 | nnncan2d 11554 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) = ((ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)))) |
62 | 47, 57, 61 | 3eqtr4d 2787 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ)) = (((ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)))) |
63 | 62 | mpteq2dva 5210 |
. . . 4
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) = (๐ฅ โ (1(,)+โ) โฆ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))))) |
64 | | 1red 11163 |
. . . . 5
โข (๐ โ 1 โ
โ) |
65 | 3, 8 | fsumrecl 15626 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ โ) |
66 | 65, 23 | rerpdivcld 12995 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ โ) |
67 | | 2vmadivsum.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ
โ+) |
68 | 67 | rpred 12964 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
69 | 68 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ด โ
โ) |
70 | | ioossre 13332 |
. . . . . . . 8
โข
(1(,)+โ) โ โ |
71 | | 1cnd 11157 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
72 | | o1const 15509 |
. . . . . . . 8
โข
(((1(,)+โ) โ โ โง 1 โ โ) โ (๐ฅ โ (1(,)+โ) โฆ
1) โ ๐(1)) |
73 | 70, 71, 72 | sylancr 588 |
. . . . . . 7
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ 1) โ
๐(1)) |
74 | 66 | recnd 11190 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ โ) |
75 | | 1cnd 11157 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 โ
โ) |
76 | 65 | recnd 11190 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ โ) |
77 | 76, 45, 45, 46 | divsubdird 11977 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) / (logโ๐ฅ)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ ((logโ๐ฅ) / (logโ๐ฅ)))) |
78 | 76, 45 | subcld 11519 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) โ โ) |
79 | 78, 45, 46 | divrecd 11941 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) / (logโ๐ฅ)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) ยท (1 / (logโ๐ฅ)))) |
80 | 45, 46 | dividd 11936 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((logโ๐ฅ) /
(logโ๐ฅ)) =
1) |
81 | 80 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ ((logโ๐ฅ) / (logโ๐ฅ))) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ 1)) |
82 | 77, 79, 81 | 3eqtr3d 2785 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) ยท (1 / (logโ๐ฅ))) = ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ 1)) |
83 | 82 | mpteq2dva 5210 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) ยท (1 / (logโ๐ฅ)))) = (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ 1))) |
84 | 65, 30 | resubcld 11590 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) โ โ) |
85 | 27, 23 | rerpdivcld 12995 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (1 /
(logโ๐ฅ)) โ
โ) |
86 | 29 | ex 414 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ (1(,)+โ) โ ๐ฅ โ
โ+)) |
87 | 86 | ssrdv 3955 |
. . . . . . . . . . 11
โข (๐ โ (1(,)+โ) โ
โ+) |
88 | | vmadivsum 26846 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โ ๐(1) |
89 | 88 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โ ๐(1)) |
90 | 87, 89 | o1res2 15452 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โ ๐(1)) |
91 | | divlogrlim 26006 |
. . . . . . . . . . 11
โข (๐ฅ โ (1(,)+โ) โฆ
(1 / (logโ๐ฅ)))
โ๐ 0 |
92 | | rlimo1 15506 |
. . . . . . . . . . 11
โข ((๐ฅ โ (1(,)+โ) โฆ
(1 / (logโ๐ฅ)))
โ๐ 0 โ (๐ฅ โ (1(,)+โ) โฆ (1 /
(logโ๐ฅ))) โ
๐(1)) |
93 | 91, 92 | mp1i 13 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (1 /
(logโ๐ฅ))) โ
๐(1)) |
94 | 84, 85, 90, 93 | o1mul2 15514 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) ยท (1 / (logโ๐ฅ)))) โ
๐(1)) |
95 | 83, 94 | eqeltrrd 2839 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ 1)) โ
๐(1)) |
96 | 74, 75, 95 | o1dif 15519 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))) โ ๐(1) โ (๐ฅ โ (1(,)+โ) โฆ
1) โ ๐(1))) |
97 | 73, 96 | mpbird 257 |
. . . . . 6
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))) โ ๐(1)) |
98 | 68 | recnd 11190 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
99 | | o1const 15509 |
. . . . . . 7
โข
(((1(,)+โ) โ โ โง ๐ด โ โ) โ (๐ฅ โ (1(,)+โ) โฆ ๐ด) โ
๐(1)) |
100 | 70, 98, 99 | sylancr 588 |
. . . . . 6
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ๐ด) โ
๐(1)) |
101 | 66, 69, 97, 100 | o1mul2 15514 |
. . . . 5
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด)) โ ๐(1)) |
102 | 66, 69 | remulcld 11192 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด) โ โ) |
103 | 15, 37 | resubcld 11590 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))) โ โ) |
104 | 8, 103 | remulcld 11192 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) โ โ) |
105 | 3, 104 | fsumrecl 15626 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) โ โ) |
106 | 105 | recnd 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) โ โ) |
107 | 106, 45, 46 | divcld 11938 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ)) โ โ) |
108 | 106 | abscld 15328 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โ โ) |
109 | 65, 69 | remulcld 11192 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ด) โ โ) |
110 | 104 | recnd 11190 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) โ โ) |
111 | 110 | abscld 15328 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โ โ) |
112 | 3, 111 | fsumrecl 15626 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(absโ(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โ โ) |
113 | 3, 110 | fsumabs 15693 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โค ฮฃ๐ โ (1...(โโ๐ฅ))(absโ(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))))) |
114 | 69 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ด โ
โ) |
115 | 8, 114 | remulcld 11192 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท ๐ด) โ
โ) |
116 | 103 | recnd 11190 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))) โ โ) |
117 | 48, 116 | absmuld 15346 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) = ((absโ((ฮโ๐) / ๐)) ยท (absโ(ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))))) |
118 | | vmage0 26486 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 0 โค
(ฮโ๐)) |
119 | 5, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค (ฮโ๐)) |
120 | 7, 35, 119 | divge0d 13004 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค ((ฮโ๐) / ๐)) |
121 | 8, 120 | absidd 15314 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮโ๐) / ๐)) = ((ฮโ๐) / ๐)) |
122 | 121 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((absโ((ฮโ๐) / ๐)) ยท (absโ(ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) = (((ฮโ๐) / ๐) ยท (absโ(ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))))) |
123 | 117, 122 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) = (((ฮโ๐) / ๐) ยท (absโ(ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))))) |
124 | 116 | abscld 15328 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ(ฮฃ๐
โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) โ โ) |
125 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (ฮโ๐) = (ฮโ๐)) |
126 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ ๐ = ๐) |
127 | 125, 126 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ โ ((ฮโ๐) / ๐) = ((ฮโ๐) / ๐)) |
128 | 127 | cbvsumv 15588 |
. . . . . . . . . . . . . . . . . 18
โข
ฮฃ๐ โ
(1...(โโ๐ฆ))((ฮโ๐) / ๐) = ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) / ๐) |
129 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = (๐ฅ / ๐) โ (โโ๐ฆ) = (โโ(๐ฅ / ๐))) |
130 | 129 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ = (๐ฅ / ๐) โ (1...(โโ๐ฆ)) = (1...(โโ(๐ฅ / ๐)))) |
131 | 130 | sumeq1d 15593 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ = (๐ฅ / ๐) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) / ๐) = ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) |
132 | 128, 131 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ = (๐ฅ / ๐) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) / ๐) = ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) |
133 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ = (๐ฅ / ๐) โ (logโ๐ฆ) = (logโ(๐ฅ / ๐))) |
134 | 132, 133 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = (๐ฅ / ๐) โ (ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) / ๐) โ (logโ๐ฆ)) = (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) |
135 | 134 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = (๐ฅ / ๐) โ (absโ(ฮฃ๐ โ
(1...(โโ๐ฆ))((ฮโ๐) / ๐) โ (logโ๐ฆ))) = (absโ(ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) |
136 | 135 | breq1d 5120 |
. . . . . . . . . . . . . 14
โข (๐ฆ = (๐ฅ / ๐) โ ((absโ(ฮฃ๐ โ
(1...(โโ๐ฆ))((ฮโ๐) / ๐) โ (logโ๐ฆ))) โค ๐ด โ (absโ(ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) โค ๐ด)) |
137 | | 2vmadivsum.2 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ๐ฆ โ
(1[,)+โ)(absโ(ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) / ๐) โ (logโ๐ฆ))) โค ๐ด) |
138 | 137 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ โ๐ฆ โ
(1[,)+โ)(absโ(ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) / ๐) โ (logโ๐ฆ))) โค ๐ด) |
139 | 36 | rpred 12964 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ฅ / ๐) โ
โ) |
140 | 5 | nncnd 12176 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ) |
141 | 140 | mulid2d 11180 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (1 ยท ๐) =
๐) |
142 | | fznnfl 13774 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ (๐ โ
(1...(โโ๐ฅ))
โ (๐ โ โ
โง ๐ โค ๐ฅ))) |
143 | 19, 142 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (๐ โ
(1...(โโ๐ฅ))
โ (๐ โ โ
โง ๐ โค ๐ฅ))) |
144 | 143 | simplbda 501 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โค ๐ฅ) |
145 | 141, 144 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (1 ยท ๐) โค
๐ฅ) |
146 | | 1red 11163 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 1 โ โ) |
147 | 19 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ฅ โ
โ) |
148 | 146, 147,
35 | lemuldivd 13013 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((1 ยท ๐) โค
๐ฅ โ 1 โค (๐ฅ / ๐))) |
149 | 145, 148 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 1 โค (๐ฅ / ๐)) |
150 | | 1re 11162 |
. . . . . . . . . . . . . . . 16
โข 1 โ
โ |
151 | | elicopnf 13369 |
. . . . . . . . . . . . . . . 16
โข (1 โ
โ โ ((๐ฅ / ๐) โ (1[,)+โ) โ
((๐ฅ / ๐) โ โ โง 1 โค (๐ฅ / ๐)))) |
152 | 150, 151 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ / ๐) โ (1[,)+โ) โ ((๐ฅ / ๐) โ โ โง 1 โค (๐ฅ / ๐))) |
153 | 139, 149,
152 | sylanbrc 584 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ฅ / ๐) โ
(1[,)+โ)) |
154 | 136, 138,
153 | rspcdva 3585 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ(ฮฃ๐
โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) โค ๐ด) |
155 | 124, 114,
8, 120, 154 | lemul2ad 12102 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท
(absโ(ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โค (((ฮโ๐) / ๐) ยท ๐ด)) |
156 | 123, 155 | eqbrtrd 5132 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โค (((ฮโ๐) / ๐) ยท ๐ด)) |
157 | 3, 111, 115, 156 | fsumle 15691 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(absโ(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โค ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ๐ด)) |
158 | 98 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ด โ
โ) |
159 | 3, 158, 48 | fsummulc1 15677 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ด) = ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ๐ด)) |
160 | 157, 159 | breqtrrd 5138 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(absโ(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โค (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ด)) |
161 | 108, 112,
109, 113, 160 | letrd 11319 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) โค (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ด)) |
162 | 108, 109,
23, 161 | lediv1dd 13022 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((absโฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) / (logโ๐ฅ)) โค ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ด) / (logโ๐ฅ))) |
163 | 106, 45, 46 | absdivd 15347 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) = ((absโฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) / (absโ(logโ๐ฅ)))) |
164 | 23 | rpge0d 12968 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค
(logโ๐ฅ)) |
165 | 30, 164 | absidd 15314 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(logโ๐ฅ)) =
(logโ๐ฅ)) |
166 | 165 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((absโฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) / (absโ(logโ๐ฅ))) = ((absโฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) / (logโ๐ฅ))) |
167 | 163, 166 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) = ((absโฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐))))) / (logโ๐ฅ))) |
168 | 3, 8, 120 | fsumge0 15687 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค
ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐)) |
169 | 65, 23, 168 | divge0d 13004 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค
(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))) |
170 | 67 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ด โ
โ+) |
171 | 170 | rpge0d 12968 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค ๐ด) |
172 | 66, 69, 169, 171 | mulge0d 11739 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค
((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด)) |
173 | 102, 172 | absidd 15314 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ((ฮฃ๐
โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด)) |
174 | 76, 158, 45, 46 | div23d 11975 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ด) / (logโ๐ฅ)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด)) |
175 | 173, 174 | eqtr4d 2780 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ((ฮฃ๐
โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ด) / (logโ๐ฅ))) |
176 | 162, 167,
175 | 3brtr4d 5142 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) โค (absโ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด))) |
177 | 176 | adantrr 716 |
. . . . 5
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง 1 โค ๐ฅ)) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) โค (absโ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) ยท ๐ด))) |
178 | 64, 101, 102, 107, 177 | o1le 15544 |
. . . 4
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐) โ (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) โ ๐(1)) |
179 | 63, 178 | eqeltrrd 2839 |
. . 3
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)))) โ
๐(1)) |
180 | 33, 42, 179 | o1dif 15519 |
. 2
โข (๐ โ ((๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) โ ๐(1) โ (๐ฅ โ (1(,)+โ) โฆ
((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) โ
๐(1))) |
181 | 2, 180 | mpbird 257 |
1
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) / ๐)) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) โ
๐(1)) |