Step | Hyp | Ref
| Expression |
1 | | 2cnd 12238 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 2 โ
โ) |
2 | | fzfid 13885 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(1...(โโ๐ฅ))
โ Fin) |
3 | | elfznn 13477 |
. . . . . . . . . . . . 13
โข (๐ โ
(1...(โโ๐ฅ))
โ ๐ โ
โ) |
4 | 3 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ) |
5 | | vmacl 26483 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮโ๐)
โ โ) |
7 | 6, 4 | nndivred 12214 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
/ ๐) โ
โ) |
8 | | elioore 13301 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ (1(,)+โ) โ
๐ฅ โ
โ) |
9 | 8 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ฅ โ
โ) |
10 | | 1rp 12926 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ+ |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 โ
โ+) |
12 | | 1red 11163 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 โ
โ) |
13 | | eliooord 13330 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ (1(,)+โ) โ (1
< ๐ฅ โง ๐ฅ <
+โ)) |
14 | 13 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (1 < ๐ฅ โง ๐ฅ < +โ)) |
15 | 14 | simpld 496 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 < ๐ฅ) |
16 | 12, 9, 15 | ltled 11310 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 โค ๐ฅ) |
17 | 9, 11, 16 | rpgecld 13003 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ฅ โ
โ+) |
18 | 17 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ฅ โ
โ+) |
19 | 4 | nnrpd 12962 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ+) |
20 | 18, 19 | rpdivcld 12981 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ฅ / ๐) โ
โ+) |
21 | 20 | relogcld 25994 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (logโ(๐ฅ /
๐)) โ
โ) |
22 | 7, 21 | remulcld 11192 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท
(logโ(๐ฅ / ๐))) โ
โ) |
23 | 2, 22 | fsumrecl 15626 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) โ โ) |
24 | 9, 15 | rplogcld 26000 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(logโ๐ฅ) โ
โ+) |
25 | 23, 24 | rerpdivcld 12995 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ โ) |
26 | 25 | recnd 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ โ) |
27 | 17 | relogcld 25994 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(logโ๐ฅ) โ
โ) |
28 | 27 | rehalfcld 12407 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((logโ๐ฅ) / 2) โ
โ) |
29 | 28 | recnd 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((logโ๐ฅ) / 2) โ
โ) |
30 | 1, 26, 29 | subdid 11618 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (2 ยท
((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) = ((2 ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (2 ยท ((logโ๐ฅ) / 2)))) |
31 | 27 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(logโ๐ฅ) โ
โ) |
32 | | 2ne0 12264 |
. . . . . . . 8
โข 2 โ
0 |
33 | 32 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 2 โ
0) |
34 | 31, 1, 33 | divcan2d 11940 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (2 ยท
((logโ๐ฅ) / 2)) =
(logโ๐ฅ)) |
35 | 34 | oveq2d 7378 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((2 ยท
(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (2 ยท ((logโ๐ฅ) / 2))) = ((2 ยท
(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ))) |
36 | 30, 35 | eqtrd 2777 |
. . . 4
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (2 ยท
((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) = ((2 ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ))) |
37 | 36 | mpteq2dva 5210 |
. . 3
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (2 ยท
((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)))) = (๐ฅ โ (1(,)+โ) โฆ ((2 ยท
(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ)))) |
38 | | 2re 12234 |
. . . . 5
โข 2 โ
โ |
39 | 38 | a1i 11 |
. . . 4
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 2 โ
โ) |
40 | 25, 28 | resubcld 11590 |
. . . 4
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)) โ โ) |
41 | | ioossre 13332 |
. . . . . 6
โข
(1(,)+โ) โ โ |
42 | | 2cn 12235 |
. . . . . 6
โข 2 โ
โ |
43 | | o1const 15509 |
. . . . . 6
โข
(((1(,)+โ) โ โ โง 2 โ โ) โ (๐ฅ โ (1(,)+โ) โฆ
2) โ ๐(1)) |
44 | 41, 42, 43 | mp2an 691 |
. . . . 5
โข (๐ฅ โ (1(,)+โ) โฆ
2) โ ๐(1) |
45 | 44 | a1i 11 |
. . . 4
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ 2) โ
๐(1)) |
46 | | vmalogdivsum2 26902 |
. . . . 5
โข (๐ฅ โ (1(,)+โ) โฆ
((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) โ ๐(1) |
47 | 46 | a1i 11 |
. . . 4
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2))) โ
๐(1)) |
48 | 39, 40, 45, 47 | o1mul2 15514 |
. . 3
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (2 ยท
((ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ ((logโ๐ฅ) / 2)))) โ
๐(1)) |
49 | 37, 48 | eqeltrrd 2839 |
. 2
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((2 ยท
(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ))) โ ๐(1)) |
50 | | fzfid 13885 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (1...(โโ(๐ฅ / ๐))) โ Fin) |
51 | | elfznn 13477 |
. . . . . . . . . . . 12
โข (๐ โ
(1...(โโ(๐ฅ /
๐))) โ ๐ โ
โ) |
52 | 51 | adantl 483 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ ๐ โ
โ) |
53 | | vmacl 26483 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
54 | 52, 53 | syl 17 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ
(ฮโ๐) โ
โ) |
55 | 52 | nnrpd 12962 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ ๐ โ
โ+) |
56 | 55 | relogcld 25994 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ
(logโ๐) โ
โ) |
57 | 9 | adantr 482 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ฅ โ
โ) |
58 | 57, 4 | nndivred 12214 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ฅ / ๐) โ
โ) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ (๐ฅ / ๐) โ โ) |
60 | 59, 52 | nndivred 12214 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ ((๐ฅ / ๐) / ๐) โ โ) |
61 | | chpcl 26489 |
. . . . . . . . . . . 12
โข (((๐ฅ / ๐) / ๐) โ โ โ (ฯโ((๐ฅ / ๐) / ๐)) โ โ) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ
(ฯโ((๐ฅ / ๐) / ๐)) โ โ) |
63 | 56, 62 | readdcld 11191 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ
((logโ๐) +
(ฯโ((๐ฅ / ๐) / ๐))) โ โ) |
64 | 54, 63 | remulcld 11192 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โง ๐ โ
(1...(โโ(๐ฅ /
๐)))) โ
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ((๐ฅ / ๐) / ๐)))) โ โ) |
65 | 50, 64 | fsumrecl 15626 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) โ โ) |
66 | 6, 65 | remulcld 11192 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) โ โ) |
67 | 2, 66 | fsumrecl 15626 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) โ โ) |
68 | 17, 24 | rpmulcld 12980 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (๐ฅ ยท (logโ๐ฅ)) โ
โ+) |
69 | 67, 68 | rerpdivcld 12995 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ โ) |
70 | 69, 27 | resubcld 11590 |
. . . 4
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (logโ๐ฅ)) โ โ) |
71 | 70 | recnd 11190 |
. . 3
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (logโ๐ฅ)) โ โ) |
72 | 23 | recnd 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) โ โ) |
73 | 24 | rpne0d 12969 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(logโ๐ฅ) โ
0) |
74 | 72, 31, 73 | divcld 11938 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)) โ โ) |
75 | 1, 74 | mulcld 11182 |
. . . 4
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (2 ยท
(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ โ) |
76 | 75, 31 | subcld 11519 |
. . 3
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((2 ยท
(ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ)) โ โ) |
77 | 69 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ โ) |
78 | 77, 75, 31 | nnncan2d 11554 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (logโ๐ฅ)) โ ((2 ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ))) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (2 ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))))) |
79 | 67 | recnd 11190 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) โ โ) |
80 | 9 | recnd 11190 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ฅ โ
โ) |
81 | 17 | rpne0d 12969 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ฅ โ 0) |
82 | 79, 80, 31, 81, 73 | divdiv1d 11969 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) / (logโ๐ฅ)) = (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ)))) |
83 | 1, 72, 31, 73 | divassd 11973 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((2 ยท
ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) / (logโ๐ฅ)) = (2 ยท (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ)))) |
84 | 82, 83 | oveq12d 7380 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) / (logโ๐ฅ)) โ ((2 ยท ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (2 ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))))) |
85 | 67, 17 | rerpdivcld 12995 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ โ) |
86 | 85 | recnd 11190 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ โ) |
87 | 1, 72 | mulcld 11182 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (2 ยท
ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) โ โ) |
88 | 86, 87, 31, 73 | divsubdird 11977 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ (2 ยท ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) / (logโ๐ฅ)) = (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) / (logโ๐ฅ)) โ ((2 ยท ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) / (logโ๐ฅ)))) |
89 | 81 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ฅ โ
0) |
90 | 66, 57, 89 | redivcld 11990 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ โ) |
91 | 90 | recnd 11190 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ โ) |
92 | 38 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 2 โ โ) |
93 | 92, 22 | remulcld 11192 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) โ โ) |
94 | 93 | recnd 11190 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) โ โ) |
95 | 2, 91, 94 | fsumsub 15680 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ (2 ยท (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) = (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ ฮฃ๐ โ (1...(โโ๐ฅ))(2 ยท
(((ฮโ๐) /
๐) ยท
(logโ(๐ฅ / ๐)))))) |
96 | 6 | recnd 11190 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮโ๐)
โ โ) |
97 | 65, 57, 89 | redivcld 11990 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ โ) |
98 | 97 | recnd 11190 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ โ) |
99 | | 2cnd 12238 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 2 โ โ) |
100 | 21 | recnd 11190 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (logโ(๐ฅ /
๐)) โ
โ) |
101 | 4 | nncnd 12176 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ) |
102 | 4 | nnne0d 12210 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
0) |
103 | 100, 101,
102 | divcld 11938 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((logโ(๐ฅ /
๐)) / ๐) โ โ) |
104 | 99, 103 | mulcld 11182 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)) โ โ) |
105 | 96, 98, 104 | subdid 11618 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) = (((ฮโ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ)) โ ((ฮโ๐) ยท (2 ยท
((logโ(๐ฅ / ๐)) / ๐))))) |
106 | 65 | recnd 11190 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) โ โ) |
107 | 80 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ฅ โ
โ) |
108 | 96, 106, 107, 89 | divassd 11973 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) = ((ฮโ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ))) |
109 | 96, 101, 100, 102 | div32d 11961 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท
(logโ(๐ฅ / ๐))) = ((ฮโ๐) ยท ((logโ(๐ฅ / ๐)) / ๐))) |
110 | 109 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) = (2 ยท ((ฮโ๐) ยท ((logโ(๐ฅ / ๐)) / ๐)))) |
111 | 99, 96, 103 | mul12d 11371 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท ((ฮโ๐) ยท ((logโ(๐ฅ / ๐)) / ๐))) = ((ฮโ๐) ยท (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) |
112 | 110, 111 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) = ((ฮโ๐) ยท (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) |
113 | 108, 112 | oveq12d 7380 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ (2 ยท (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) = (((ฮโ๐) ยท (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ)) โ ((ฮโ๐) ยท (2 ยท
((logโ(๐ฅ / ๐)) / ๐))))) |
114 | 105, 113 | eqtr4d 2780 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) = ((((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ (2 ยท (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))))) |
115 | 114 | sumeq2dv 15595 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) = ฮฃ๐ โ (1...(โโ๐ฅ))((((ฮโ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ (2 ยท (((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))))) |
116 | 66 | recnd 11190 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) โ โ) |
117 | 2, 80, 116, 81 | fsumdivc 15678 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) = ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ)) |
118 | 22 | recnd 11190 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท
(logโ(๐ฅ / ๐))) โ
โ) |
119 | 2, 1, 118 | fsummulc2 15676 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (2 ยท
ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) = ฮฃ๐ โ (1...(โโ๐ฅ))(2 ยท
(((ฮโ๐) /
๐) ยท
(logโ(๐ฅ / ๐))))) |
120 | 117, 119 | oveq12d 7380 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ (2 ยท ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) = (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) ยท ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ ฮฃ๐ โ (1...(โโ๐ฅ))(2 ยท
(((ฮโ๐) /
๐) ยท
(logโ(๐ฅ / ๐)))))) |
121 | 95, 115, 120 | 3eqtr4rd 2788 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ (2 ยท ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) = ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) |
122 | 121 | oveq1d 7377 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) โ (2 ยท ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))))) / (logโ๐ฅ)) = (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ))) |
123 | 88, 122 | eqtr3d 2779 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / ๐ฅ) / (logโ๐ฅ)) โ ((2 ยท ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐)))) / (logโ๐ฅ))) = (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ))) |
124 | 78, 84, 123 | 3eqtr2d 2783 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (logโ๐ฅ)) โ ((2 ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ))) = (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ))) |
125 | 124 | mpteq2dva 5210 |
. . . 4
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (logโ๐ฅ)) โ ((2 ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ)))) = (๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ)))) |
126 | | 1red 11163 |
. . . . 5
โข (๐ โ 1 โ
โ) |
127 | | selberg4lem1.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ
โ+) |
128 | 127 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ด โ
โ+) |
129 | 128 | rpred 12964 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ด โ
โ) |
130 | 2, 7 | fsumrecl 15626 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ โ) |
131 | 130, 24 | rerpdivcld 12995 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ โ) |
132 | 127 | rpcnd 12966 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
133 | | o1const 15509 |
. . . . . . 7
โข
(((1(,)+โ) โ โ โง ๐ด โ โ) โ (๐ฅ โ (1(,)+โ) โฆ ๐ด) โ
๐(1)) |
134 | 41, 132, 133 | sylancr 588 |
. . . . . 6
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ๐ด) โ
๐(1)) |
135 | | 1cnd 11157 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
136 | | o1const 15509 |
. . . . . . . 8
โข
(((1(,)+โ) โ โ โง 1 โ โ) โ (๐ฅ โ (1(,)+โ) โฆ
1) โ ๐(1)) |
137 | 41, 135, 136 | sylancr 588 |
. . . . . . 7
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ 1) โ
๐(1)) |
138 | 131 | recnd 11190 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ โ) |
139 | | 1cnd 11157 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 1 โ
โ) |
140 | 130 | recnd 11190 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ โ) |
141 | 140, 31, 31, 73 | divsubdird 11977 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) / (logโ๐ฅ)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ ((logโ๐ฅ) / (logโ๐ฅ)))) |
142 | 140, 31 | subcld 11519 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) โ โ) |
143 | 142, 31, 73 | divrecd 11941 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) / (logโ๐ฅ)) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) ยท (1 / (logโ๐ฅ)))) |
144 | 31, 73 | dividd 11936 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((logโ๐ฅ) /
(logโ๐ฅ)) =
1) |
145 | 144 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ ((logโ๐ฅ) / (logโ๐ฅ))) = ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ 1)) |
146 | 141, 143,
145 | 3eqtr3d 2785 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) ยท (1 / (logโ๐ฅ))) = ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ 1)) |
147 | 146 | mpteq2dva 5210 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) ยท (1 / (logโ๐ฅ)))) = (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ 1))) |
148 | 130, 27 | resubcld 11590 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) โ โ) |
149 | 12, 24 | rerpdivcld 12995 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (1 /
(logโ๐ฅ)) โ
โ) |
150 | 17 | ex 414 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ (1(,)+โ) โ ๐ฅ โ
โ+)) |
151 | 150 | ssrdv 3955 |
. . . . . . . . . . 11
โข (๐ โ (1(,)+โ) โ
โ+) |
152 | | vmadivsum 26846 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โ ๐(1) |
153 | 152 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โ ๐(1)) |
154 | 151, 153 | o1res2 15452 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โ ๐(1)) |
155 | | divlogrlim 26006 |
. . . . . . . . . . 11
โข (๐ฅ โ (1(,)+โ) โฆ
(1 / (logโ๐ฅ)))
โ๐ 0 |
156 | | rlimo1 15506 |
. . . . . . . . . . 11
โข ((๐ฅ โ (1(,)+โ) โฆ
(1 / (logโ๐ฅ)))
โ๐ 0 โ (๐ฅ โ (1(,)+โ) โฆ (1 /
(logโ๐ฅ))) โ
๐(1)) |
157 | 155, 156 | mp1i 13 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (1 /
(logโ๐ฅ))) โ
๐(1)) |
158 | 148, 149,
154, 157 | o1mul2 15514 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ)) ยท (1 / (logโ๐ฅ)))) โ
๐(1)) |
159 | 147, 158 | eqeltrrd 2839 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)) โ 1)) โ
๐(1)) |
160 | 138, 139,
159 | o1dif 15519 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))) โ ๐(1) โ (๐ฅ โ (1(,)+โ) โฆ
1) โ ๐(1))) |
161 | 137, 160 | mpbird 257 |
. . . . . 6
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))) โ ๐(1)) |
162 | 129, 131,
134, 161 | o1mul2 15514 |
. . . . 5
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (๐ด ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)))) โ ๐(1)) |
163 | 129, 131 | remulcld 11192 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (๐ด ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))) โ โ) |
164 | 21, 4 | nndivred 12214 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((logโ(๐ฅ /
๐)) / ๐) โ โ) |
165 | 92, 164 | remulcld 11192 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)) โ โ) |
166 | 97, 165 | resubcld 11590 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))) โ โ) |
167 | 6, 166 | remulcld 11192 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) โ โ) |
168 | 2, 167 | fsumrecl 15626 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) โ โ) |
169 | 168, 24 | rerpdivcld 12995 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ)) โ โ) |
170 | 169 | recnd 11190 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ)) โ โ) |
171 | 168 | recnd 11190 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) โ โ) |
172 | 171 | abscld 15328 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โ โ) |
173 | 129, 130 | remulcld 11192 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (๐ด ยท ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐)) โ โ) |
174 | 98, 104 | subcld 11519 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))) โ โ) |
175 | 96, 174 | mulcld 11182 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) โ โ) |
176 | 175 | abscld 15328 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โ โ) |
177 | 2, 176 | fsumrecl 15626 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(absโ((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โ โ) |
178 | 167 | recnd 11190 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) โ โ) |
179 | 2, 178 | fsumabs 15693 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โค ฮฃ๐ โ (1...(โโ๐ฅ))(absโ((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))))) |
180 | 129 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ด โ
โ) |
181 | 180, 7 | remulcld 11192 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ด ยท
((ฮโ๐) / ๐)) โ
โ) |
182 | 174 | abscld 15328 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) โ โ) |
183 | 180, 4 | nndivred 12214 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ด / ๐) โ
โ) |
184 | | vmage0 26486 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 0 โค
(ฮโ๐)) |
185 | 4, 184 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค (ฮโ๐)) |
186 | 106, 107,
101, 89, 102 | divdiv2d 11970 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) = ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) ยท ๐) / ๐ฅ)) |
187 | 106, 101,
107, 89 | div23d 11975 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) ยท ๐) / ๐ฅ) = ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) ยท ๐)) |
188 | 186, 187 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) = ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) ยท ๐)) |
189 | 99, 103, 101 | mulassd 11185 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((2 ยท ((logโ(๐ฅ / ๐)) / ๐)) ยท ๐) = (2 ยท (((logโ(๐ฅ / ๐)) / ๐) ยท ๐))) |
190 | 100, 101,
102 | divcan1d 11939 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((logโ(๐ฅ /
๐)) / ๐) ยท ๐) = (logโ(๐ฅ / ๐))) |
191 | 190 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท (((logโ(๐ฅ / ๐)) / ๐) ยท ๐)) = (2 ยท (logโ(๐ฅ / ๐)))) |
192 | 189, 191 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (2 ยท (logโ(๐ฅ / ๐))) = ((2 ยท ((logโ(๐ฅ / ๐)) / ๐)) ยท ๐)) |
193 | 188, 192 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) โ (2 ยท (logโ(๐ฅ / ๐)))) = (((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) ยท ๐) โ ((2 ยท ((logโ(๐ฅ / ๐)) / ๐)) ยท ๐))) |
194 | 98, 104, 101 | subdird 11619 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))) ยท ๐) = (((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) ยท ๐) โ ((2 ยท ((logโ(๐ฅ / ๐)) / ๐)) ยท ๐))) |
195 | 193, 194 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) โ (2 ยท (logโ(๐ฅ / ๐)))) = (((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))) ยท ๐)) |
196 | 195 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) โ (2 ยท (logโ(๐ฅ / ๐))))) = (absโ(((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))) ยท ๐))) |
197 | 174, 101 | absmuld 15346 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ(((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))) ยท ๐)) = ((absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) ยท (absโ๐))) |
198 | 4 | nnred 12175 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ) |
199 | 19 | rpge0d 12968 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค ๐) |
200 | 198, 199 | absidd 15314 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ๐) =
๐) |
201 | 200 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) ยท (absโ๐)) = ((absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) ยท ๐)) |
202 | 196, 197,
201 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) โ (2 ยท (logโ(๐ฅ / ๐))))) = ((absโ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) ยท ๐)) |
203 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = ๐ โ (ฮโ๐) = (ฮโ๐)) |
204 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = ๐ โ (logโ๐) = (logโ๐)) |
205 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ = ๐ โ (๐ฆ / ๐) = (๐ฆ / ๐)) |
206 | 205 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = ๐ โ (ฯโ(๐ฆ / ๐)) = (ฯโ(๐ฆ / ๐))) |
207 | 204, 206 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = ๐ โ ((logโ๐) + (ฯโ(๐ฆ / ๐))) = ((logโ๐) + (ฯโ(๐ฆ / ๐)))) |
208 | 203, 207 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = ๐ โ ((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) = ((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐))))) |
209 | 208 | cbvsumv 15588 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
ฮฃ๐ โ
(1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) = ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) |
210 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ = (๐ฅ / ๐) โ (โโ๐ฆ) = (โโ(๐ฅ / ๐))) |
211 | 210 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ = (๐ฅ / ๐) โ (1...(โโ๐ฆ)) = (1...(โโ(๐ฅ / ๐)))) |
212 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ = (๐ฅ / ๐) โ (ฯโ(๐ฆ / ๐)) = (ฯโ((๐ฅ / ๐) / ๐))) |
213 | 212 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ = (๐ฅ / ๐) โ ((logโ๐) + (ฯโ(๐ฆ / ๐))) = ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) |
214 | 213 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ = (๐ฅ / ๐) โ ((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) = ((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) |
215 | 214 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ = (๐ฅ / ๐) โง ๐ โ (1...(โโ๐ฆ))) โ
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ฆ / ๐)))) = ((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) |
216 | 211, 215 | sumeq12dv 15598 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ = (๐ฅ / ๐) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) = ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) |
217 | 209, 216 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = (๐ฅ / ๐) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) = ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) |
218 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = (๐ฅ / ๐) โ ๐ฆ = (๐ฅ / ๐)) |
219 | 217, 218 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = (๐ฅ / ๐) โ (ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) / ๐ฆ) = (ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐))) |
220 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = (๐ฅ / ๐) โ (logโ๐ฆ) = (logโ(๐ฅ / ๐))) |
221 | 220 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = (๐ฅ / ๐) โ (2 ยท (logโ๐ฆ)) = (2 ยท
(logโ(๐ฅ / ๐)))) |
222 | 219, 221 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ = (๐ฅ / ๐) โ ((ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) / ๐ฆ) โ (2 ยท (logโ๐ฆ))) = ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) โ (2 ยท (logโ(๐ฅ / ๐))))) |
223 | 222 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ = (๐ฅ / ๐) โ (absโ((ฮฃ๐ โ
(1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) / ๐ฆ) โ (2 ยท (logโ๐ฆ)))) = (absโ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) โ (2 ยท (logโ(๐ฅ / ๐)))))) |
224 | 223 | breq1d 5120 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ = (๐ฅ / ๐) โ ((absโ((ฮฃ๐ โ
(1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) / ๐ฆ) โ (2 ยท (logโ๐ฆ)))) โค ๐ด โ (absโ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) โ (2 ยท (logโ(๐ฅ / ๐))))) โค ๐ด)) |
225 | | selberg4lem1.2 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ๐ฆ โ
(1[,)+โ)(absโ((ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) / ๐ฆ) โ (2 ยท (logโ๐ฆ)))) โค ๐ด) |
226 | 225 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ โ๐ฆ โ
(1[,)+โ)(absโ((ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) / ๐ฆ) โ (2 ยท (logโ๐ฆ)))) โค ๐ด) |
227 | 101 | mulid2d 11180 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (1 ยท ๐) =
๐) |
228 | | fznnfl 13774 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ (๐ โ
(1...(โโ๐ฅ))
โ (๐ โ โ
โง ๐ โค ๐ฅ))) |
229 | 9, 228 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (๐ โ
(1...(โโ๐ฅ))
โ (๐ โ โ
โง ๐ โค ๐ฅ))) |
230 | 229 | simplbda 501 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โค ๐ฅ) |
231 | 227, 230 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (1 ยท ๐) โค
๐ฅ) |
232 | | 1red 11163 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 1 โ โ) |
233 | 232, 57, 19 | lemuldivd 13013 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((1 ยท ๐) โค
๐ฅ โ 1 โค (๐ฅ / ๐))) |
234 | 231, 233 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 1 โค (๐ฅ / ๐)) |
235 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โ |
236 | | elicopnf 13369 |
. . . . . . . . . . . . . . . . . . 19
โข (1 โ
โ โ ((๐ฅ / ๐) โ (1[,)+โ) โ
((๐ฅ / ๐) โ โ โง 1 โค (๐ฅ / ๐)))) |
237 | 235, 236 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ / ๐) โ (1[,)+โ) โ ((๐ฅ / ๐) โ โ โง 1 โค (๐ฅ / ๐))) |
238 | 58, 234, 237 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ฅ / ๐) โ
(1[,)+โ)) |
239 | 224, 226,
238 | rspcdva 3585 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / (๐ฅ / ๐)) โ (2 ยท (logโ(๐ฅ / ๐))))) โค ๐ด) |
240 | 202, 239 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) ยท ๐) โค ๐ด) |
241 | 182, 180,
19 | lemuldivd 13013 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (((absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) ยท ๐) โค ๐ด โ (absโ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) โค (๐ด / ๐))) |
242 | 240, 241 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) โค (๐ด / ๐)) |
243 | 182, 183,
6, 185, 242 | lemul2ad 12102 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท (absโ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โค ((ฮโ๐) ยท (๐ด / ๐))) |
244 | 96, 174 | absmuld 15346 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) = ((absโ(ฮโ๐)) ยท
(absโ((ฮฃ๐
โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))))) |
245 | 6, 185 | absidd 15314 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ(ฮโ๐)) = (ฮโ๐)) |
246 | 245 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((absโ(ฮโ๐)) ยท (absโ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) = ((ฮโ๐) ยท (absโ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))))) |
247 | 244, 246 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) = ((ฮโ๐) ยท (absโ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))))) |
248 | 132 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ด โ
โ) |
249 | 248, 96, 101, 102 | div12d 11974 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ด ยท
((ฮโ๐) / ๐)) = ((ฮโ๐) ยท (๐ด / ๐))) |
250 | 243, 247,
249 | 3brtr4d 5142 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ (absโ((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โค (๐ด ยท ((ฮโ๐) / ๐))) |
251 | 2, 176, 181, 250 | fsumle 15691 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(absโ((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โค ฮฃ๐ โ (1...(โโ๐ฅ))(๐ด ยท ((ฮโ๐) / ๐))) |
252 | 132 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ๐ด โ
โ) |
253 | 7 | recnd 11190 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
/ ๐) โ
โ) |
254 | 2, 252, 253 | fsummulc2 15676 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (๐ด ยท ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐)) = ฮฃ๐ โ (1...(โโ๐ฅ))(๐ด ยท ((ฮโ๐) / ๐))) |
255 | 251, 254 | breqtrrd 5138 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ฮฃ๐ โ
(1...(โโ๐ฅ))(absโ((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โค (๐ด ยท ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐))) |
256 | 172, 177,
173, 179, 255 | letrd 11319 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) โค (๐ด ยท ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐))) |
257 | 172, 173,
24, 256 | lediv1dd 13022 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((absโฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) / (logโ๐ฅ)) โค ((๐ด ยท ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐)) / (logโ๐ฅ))) |
258 | 252, 140,
31, 73 | divassd 11973 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ ((๐ด ยท ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐)) / (logโ๐ฅ)) = (๐ด ยท (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)))) |
259 | 257, 258 | breqtrd 5136 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((absโฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) / (logโ๐ฅ)) โค (๐ด ยท (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)))) |
260 | 171, 31, 73 | absdivd 15347 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ))) = ((absโฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) / (absโ(logโ๐ฅ)))) |
261 | 24 | rpge0d 12968 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค
(logโ๐ฅ)) |
262 | 27, 261 | absidd 15314 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(logโ๐ฅ)) =
(logโ๐ฅ)) |
263 | 262 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
((absโฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) / (absโ(logโ๐ฅ))) = ((absโฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) / (logโ๐ฅ))) |
264 | 260, 263 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ))) = ((absโฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ
(1...(โโ(๐ฅ /
๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐))))) / (logโ๐ฅ))) |
265 | 128 | rpge0d 12968 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค ๐ด) |
266 | 6, 19, 185 | divge0d 13004 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1(,)+โ)) โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค ((ฮโ๐) / ๐)) |
267 | 2, 7, 266 | fsumge0 15687 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค
ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐)) |
268 | 130, 24, 267 | divge0d 13004 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค
(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))) |
269 | 129, 131,
265, 268 | mulge0d 11739 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ 0 โค (๐ด ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)))) |
270 | 163, 269 | absidd 15314 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(๐ด ยท
(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)))) = (๐ด ยท (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ)))) |
271 | 259, 264,
270 | 3brtr4d 5142 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ))) โค (absโ(๐ด ยท (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))))) |
272 | 271 | adantrr 716 |
. . . . 5
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง 1 โค ๐ฅ)) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ))) โค (absโ(๐ด ยท (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) / (logโ๐ฅ))))) |
273 | 126, 162,
163, 170, 272 | o1le 15544 |
. . . 4
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐)))) / ๐ฅ) โ (2 ยท ((logโ(๐ฅ / ๐)) / ๐)))) / (logโ๐ฅ))) โ ๐(1)) |
274 | 125, 273 | eqeltrd 2838 |
. . 3
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (logโ๐ฅ)) โ ((2 ยท (ฮฃ๐ โ
(1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ)))) โ ๐(1)) |
275 | 71, 76, 274 | o1dif 15519 |
. 2
โข (๐ โ ((๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (logโ๐ฅ))) โ ๐(1) โ (๐ฅ โ (1(,)+โ) โฆ
((2 ยท (ฮฃ๐
โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท (logโ(๐ฅ / ๐))) / (logโ๐ฅ))) โ (logโ๐ฅ))) โ ๐(1))) |
276 | 49, 275 | mpbird 257 |
1
โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐)))((ฮโ๐) ยท ((logโ๐) + (ฯโ((๐ฅ / ๐) / ๐))))) / (๐ฅ ยท (logโ๐ฅ))) โ (logโ๐ฅ))) โ ๐(1)) |