Step | Hyp | Ref
| Expression |
1 | | 1re 11162 |
. . . . . . 7
โข 1 โ
โ |
2 | | elicopnf 13369 |
. . . . . . 7
โข (1 โ
โ โ (๐ฅ โ
(1[,)+โ) โ (๐ฅ
โ โ โง 1 โค ๐ฅ))) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
โข (โค
โ (๐ฅ โ
(1[,)+โ) โ (๐ฅ
โ โ โง 1 โค ๐ฅ))) |
4 | 3 | simprbda 500 |
. . . . 5
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ ๐ฅ โ โ) |
5 | 4 | ex 414 |
. . . 4
โข (โค
โ (๐ฅ โ
(1[,)+โ) โ ๐ฅ
โ โ)) |
6 | 5 | ssrdv 3955 |
. . 3
โข (โค
โ (1[,)+โ) โ โ) |
7 | 1 | a1i 11 |
. . 3
โข (โค
โ 1 โ โ) |
8 | | fzfid 13885 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ (1...(โโ๐ฅ)) โ Fin) |
9 | | elfznn 13477 |
. . . . . . . . . 10
โข (๐ โ
(1...(โโ๐ฅ))
โ ๐ โ
โ) |
10 | 9 | adantl 483 |
. . . . . . . . 9
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ ๐ โ โ) |
11 | | vmacl 26483 |
. . . . . . . . 9
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ (ฮโ๐) โ
โ) |
13 | 10 | nnrpd 12962 |
. . . . . . . . . 10
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ ๐ โ โ+) |
14 | 13 | relogcld 25994 |
. . . . . . . . 9
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ (logโ๐) โ
โ) |
15 | 4 | adantr 482 |
. . . . . . . . . . 11
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ ๐ฅ โ โ) |
16 | 15, 10 | nndivred 12214 |
. . . . . . . . . 10
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ (๐ฅ / ๐) โ โ) |
17 | | chpcl 26489 |
. . . . . . . . . 10
โข ((๐ฅ / ๐) โ โ โ (ฯโ(๐ฅ / ๐)) โ โ) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ (ฯโ(๐ฅ / ๐)) โ โ) |
19 | 14, 18 | readdcld 11191 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ ((logโ๐) + (ฯโ(๐ฅ / ๐))) โ โ) |
20 | 12, 19 | remulcld 11192 |
. . . . . . 7
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ฅ / ๐)))) โ
โ) |
21 | 8, 20 | fsumrecl 15626 |
. . . . . 6
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) โ โ) |
22 | | 1rp 12926 |
. . . . . . . 8
โข 1 โ
โ+ |
23 | 22 | a1i 11 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ 1 โ โ+) |
24 | 3 | simplbda 501 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ 1 โค ๐ฅ) |
25 | 4, 23, 24 | rpgecld 13003 |
. . . . . 6
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ ๐ฅ โ โ+) |
26 | 21, 25 | rerpdivcld 12995 |
. . . . 5
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ โ) |
27 | | 2re 12234 |
. . . . . . 7
โข 2 โ
โ |
28 | 27 | a1i 11 |
. . . . . 6
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ 2 โ โ) |
29 | 25 | relogcld 25994 |
. . . . . 6
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ (logโ๐ฅ) โ โ) |
30 | 28, 29 | remulcld 11192 |
. . . . 5
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ (2 ยท (logโ๐ฅ)) โ โ) |
31 | 26, 30 | resubcld 11590 |
. . . 4
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ))) โ
โ) |
32 | 31 | recnd 11190 |
. . 3
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ))) โ
โ) |
33 | 25 | ex 414 |
. . . . 5
โข (โค
โ (๐ฅ โ
(1[,)+โ) โ ๐ฅ
โ โ+)) |
34 | 33 | ssrdv 3955 |
. . . 4
โข (โค
โ (1[,)+โ) โ โ+) |
35 | | selberg 26912 |
. . . . 5
โข (๐ฅ โ โ+
โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โ
๐(1) |
36 | 35 | a1i 11 |
. . . 4
โข (โค
โ (๐ฅ โ
โ+ โฆ ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โ
๐(1)) |
37 | 34, 36 | o1res2 15452 |
. . 3
โข (โค
โ (๐ฅ โ
(1[,)+โ) โฆ ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โ
๐(1)) |
38 | | fzfid 13885 |
. . . . 5
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ (1...(โโ๐ฆ)) โ Fin) |
39 | | elfznn 13477 |
. . . . . . . 8
โข (๐ โ
(1...(โโ๐ฆ))
โ ๐ โ
โ) |
40 | 39 | adantl 483 |
. . . . . . 7
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ โ โ) |
41 | 40, 11 | syl 17 |
. . . . . 6
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (ฮโ๐) โ
โ) |
42 | 40 | nnrpd 12962 |
. . . . . . . 8
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ โ โ+) |
43 | 42 | relogcld 25994 |
. . . . . . 7
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (logโ๐) โ
โ) |
44 | | simprl 770 |
. . . . . . . . . 10
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ ๐ฆ โ โ) |
45 | 44 | adantr 482 |
. . . . . . . . 9
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ฆ โ โ) |
46 | 45, 40 | nndivred 12214 |
. . . . . . . 8
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (๐ฆ / ๐) โ โ) |
47 | | chpcl 26489 |
. . . . . . . 8
โข ((๐ฆ / ๐) โ โ โ (ฯโ(๐ฆ / ๐)) โ โ) |
48 | 46, 47 | syl 17 |
. . . . . . 7
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (ฯโ(๐ฆ / ๐)) โ โ) |
49 | 43, 48 | readdcld 11191 |
. . . . . 6
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ((logโ๐) + (ฯโ(๐ฆ / ๐))) โ โ) |
50 | 41, 49 | remulcld 11192 |
. . . . 5
โข
(((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ฆ / ๐)))) โ
โ) |
51 | 38, 50 | fsumrecl 15626 |
. . . 4
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) โ โ) |
52 | 27 | a1i 11 |
. . . . 5
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ 2 โ โ) |
53 | 22 | a1i 11 |
. . . . . . 7
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ 1 โ
โ+) |
54 | | simprr 772 |
. . . . . . 7
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ 1 โค ๐ฆ) |
55 | 44, 53, 54 | rpgecld 13003 |
. . . . . 6
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ ๐ฆ โ โ+) |
56 | 55 | relogcld 25994 |
. . . . 5
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ (logโ๐ฆ) โ โ) |
57 | 52, 56 | remulcld 11192 |
. . . 4
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ (2 ยท (logโ๐ฆ)) โ
โ) |
58 | 51, 57 | readdcld 11191 |
. . 3
โข
((โค โง (๐ฆ
โ โ โง 1 โค ๐ฆ)) โ (ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) + (2 ยท (logโ๐ฆ))) โ
โ) |
59 | 31 | adantr 482 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ))) โ
โ) |
60 | 59 | recnd 11190 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ))) โ
โ) |
61 | 60 | abscld 15328 |
. . . 4
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (absโ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โ
โ) |
62 | 26 | adantr 482 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ โ) |
63 | 30 | adantr 482 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (2 ยท (logโ๐ฅ)) โ
โ) |
64 | 62, 63 | readdcld 11191 |
. . . 4
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) + (2 ยท (logโ๐ฅ))) โ โ) |
65 | | fzfid 13885 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (1...(โโ๐ฆ)) โ Fin) |
66 | 39 | adantl 483 |
. . . . . . . 8
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ โ โ) |
67 | 66, 11 | syl 17 |
. . . . . . 7
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (ฮโ๐) โ
โ) |
68 | 66 | nnrpd 12962 |
. . . . . . . . 9
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ โ โ+) |
69 | 68 | relogcld 25994 |
. . . . . . . 8
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (logโ๐) โ
โ) |
70 | | simprll 778 |
. . . . . . . . . . 11
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ๐ฆ โ โ) |
71 | 70 | adantr 482 |
. . . . . . . . . 10
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ฆ โ โ) |
72 | 71, 66 | nndivred 12214 |
. . . . . . . . 9
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (๐ฆ / ๐) โ โ) |
73 | 72, 47 | syl 17 |
. . . . . . . 8
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (ฯโ(๐ฆ / ๐)) โ โ) |
74 | 69, 73 | readdcld 11191 |
. . . . . . 7
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ((logโ๐) + (ฯโ(๐ฆ / ๐))) โ โ) |
75 | 67, 74 | remulcld 11192 |
. . . . . 6
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ฆ / ๐)))) โ
โ) |
76 | 65, 75 | fsumrecl 15626 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) โ โ) |
77 | 27 | a1i 11 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ 2 โ โ) |
78 | 25 | adantr 482 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ๐ฅ โ โ+) |
79 | 4 | adantr 482 |
. . . . . . . . 9
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ๐ฅ โ โ) |
80 | | simprr 772 |
. . . . . . . . 9
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ๐ฅ < ๐ฆ) |
81 | 79, 70, 80 | ltled 11310 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ๐ฅ โค ๐ฆ) |
82 | 70, 78, 81 | rpgecld 13003 |
. . . . . . 7
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ๐ฆ โ โ+) |
83 | 82 | relogcld 25994 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (logโ๐ฆ) โ โ) |
84 | 77, 83 | remulcld 11192 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (2 ยท (logโ๐ฆ)) โ
โ) |
85 | 76, 84 | readdcld 11191 |
. . . 4
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) + (2 ยท (logโ๐ฆ))) โ
โ) |
86 | 62 | recnd 11190 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ โ) |
87 | 63 | recnd 11190 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (2 ยท (logโ๐ฅ)) โ
โ) |
88 | 86, 87 | abs2dif2d 15350 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (absโ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โค
((absโ(ฮฃ๐
โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ)) + (absโ(2 ยท (logโ๐ฅ))))) |
89 | 21 | adantr 482 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) โ โ) |
90 | | vmage0 26486 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 โค
(ฮโ๐)) |
91 | 10, 90 | syl 17 |
. . . . . . . . . . 11
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ 0 โค
(ฮโ๐)) |
92 | 10 | nnred 12175 |
. . . . . . . . . . . . 13
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ ๐ โ โ) |
93 | 10 | nnge1d 12208 |
. . . . . . . . . . . . 13
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ 1 โค ๐) |
94 | 92, 93 | logge0d 26001 |
. . . . . . . . . . . 12
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ 0 โค
(logโ๐)) |
95 | | chpge0 26491 |
. . . . . . . . . . . . 13
โข ((๐ฅ / ๐) โ โ โ 0 โค
(ฯโ(๐ฅ / ๐))) |
96 | 16, 95 | syl 17 |
. . . . . . . . . . . 12
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ 0 โค
(ฯโ(๐ฅ / ๐))) |
97 | 14, 18, 94, 96 | addge0d 11738 |
. . . . . . . . . . 11
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ 0 โค
((logโ๐) +
(ฯโ(๐ฅ / ๐)))) |
98 | 12, 19, 91, 97 | mulge0d 11739 |
. . . . . . . . . 10
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ๐ โ (1...(โโ๐ฅ))) โ 0 โค
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ฅ / ๐))))) |
99 | 8, 20, 98 | fsumge0 15687 |
. . . . . . . . 9
โข
((โค โง ๐ฅ
โ (1[,)+โ)) โ 0 โค ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐))))) |
100 | 99 | adantr 482 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ 0 โค ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐))))) |
101 | 89, 78, 100 | divge0d 13004 |
. . . . . . 7
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ 0 โค (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ)) |
102 | 62, 101 | absidd 15314 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ)) = (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ)) |
103 | 78 | relogcld 25994 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (logโ๐ฅ) โ โ) |
104 | | 2rp 12927 |
. . . . . . . . 9
โข 2 โ
โ+ |
105 | | rpge0 12935 |
. . . . . . . . 9
โข (2 โ
โ+ โ 0 โค 2) |
106 | 104, 105 | mp1i 13 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ 0 โค 2) |
107 | 24 | adantr 482 |
. . . . . . . . 9
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ 1 โค ๐ฅ) |
108 | 79, 107 | logge0d 26001 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ 0 โค (logโ๐ฅ)) |
109 | 77, 103, 106, 108 | mulge0d 11739 |
. . . . . . 7
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ 0 โค (2 ยท (logโ๐ฅ))) |
110 | 63, 109 | absidd 15314 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (absโ(2 ยท
(logโ๐ฅ))) = (2
ยท (logโ๐ฅ))) |
111 | 102, 110 | oveq12d 7380 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ((absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ)) + (absโ(2 ยท (logโ๐ฅ)))) = ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) + (2 ยท (logโ๐ฅ)))) |
112 | 88, 111 | breqtrd 5136 |
. . . 4
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (absโ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โค ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) + (2 ยท (logโ๐ฅ)))) |
113 | 22 | a1i 11 |
. . . . . . 7
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ 1 โ
โ+) |
114 | 79 | adantr 482 |
. . . . . . . . . . . . 13
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ฅ โ โ) |
115 | 114, 66 | nndivred 12214 |
. . . . . . . . . . . 12
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (๐ฅ / ๐) โ โ) |
116 | 115, 17 | syl 17 |
. . . . . . . . . . 11
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (ฯโ(๐ฅ / ๐)) โ โ) |
117 | 69, 116 | readdcld 11191 |
. . . . . . . . . 10
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ((logโ๐) + (ฯโ(๐ฅ / ๐))) โ โ) |
118 | 67, 117 | remulcld 11192 |
. . . . . . . . 9
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ฅ / ๐)))) โ
โ) |
119 | 65, 118 | fsumrecl 15626 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) โ โ) |
120 | 66, 90 | syl 17 |
. . . . . . . . . 10
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ 0 โค
(ฮโ๐)) |
121 | 66 | nnred 12175 |
. . . . . . . . . . . 12
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ โ โ) |
122 | 66 | nnge1d 12208 |
. . . . . . . . . . . 12
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ 1 โค ๐) |
123 | 121, 122 | logge0d 26001 |
. . . . . . . . . . 11
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ 0 โค
(logโ๐)) |
124 | 115, 95 | syl 17 |
. . . . . . . . . . 11
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ 0 โค
(ฯโ(๐ฅ / ๐))) |
125 | 69, 116, 123, 124 | addge0d 11738 |
. . . . . . . . . 10
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ 0 โค
((logโ๐) +
(ฯโ(๐ฅ / ๐)))) |
126 | 67, 117, 120, 125 | mulge0d 11739 |
. . . . . . . . 9
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ 0 โค
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ฅ / ๐))))) |
127 | | flword2 13725 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ โค ๐ฆ) โ (โโ๐ฆ) โ
(โคโฅโ(โโ๐ฅ))) |
128 | 79, 70, 81, 127 | syl3anc 1372 |
. . . . . . . . . 10
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (โโ๐ฆ) โ
(โคโฅโ(โโ๐ฅ))) |
129 | | fzss2 13488 |
. . . . . . . . . 10
โข
((โโ๐ฆ)
โ (โคโฅโ(โโ๐ฅ)) โ (1...(โโ๐ฅ)) โ
(1...(โโ๐ฆ))) |
130 | 128, 129 | syl 17 |
. . . . . . . . 9
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (1...(โโ๐ฅ)) โ
(1...(โโ๐ฆ))) |
131 | 65, 118, 126, 130 | fsumless 15688 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) โค ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐))))) |
132 | 81 | adantr 482 |
. . . . . . . . . . . . 13
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ๐ฅ โค ๐ฆ) |
133 | 114, 71, 68, 132 | lediv1dd 13022 |
. . . . . . . . . . . 12
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (๐ฅ / ๐) โค (๐ฆ / ๐)) |
134 | | chpwordi 26522 |
. . . . . . . . . . . 12
โข (((๐ฅ / ๐) โ โ โง (๐ฆ / ๐) โ โ โง (๐ฅ / ๐) โค (๐ฆ / ๐)) โ (ฯโ(๐ฅ / ๐)) โค (ฯโ(๐ฆ / ๐))) |
135 | 115, 72, 133, 134 | syl3anc 1372 |
. . . . . . . . . . 11
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ (ฯโ(๐ฅ / ๐)) โค (ฯโ(๐ฆ / ๐))) |
136 | 116, 73, 69, 135 | leadd2dd 11777 |
. . . . . . . . . 10
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ ((logโ๐) + (ฯโ(๐ฅ / ๐))) โค ((logโ๐) + (ฯโ(๐ฆ / ๐)))) |
137 | 117, 74, 67, 120, 136 | lemul2ad 12102 |
. . . . . . . . 9
โข
((((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โง ๐ โ (1...(โโ๐ฆ))) โ
((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ฅ / ๐)))) โค ((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐))))) |
138 | 65, 118, 75, 137 | fsumle 15691 |
. . . . . . . 8
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) โค ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐))))) |
139 | 89, 119, 76, 131, 138 | letrd 11319 |
. . . . . . 7
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) โค ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐))))) |
140 | 89, 76, 113, 79, 100, 139, 107 | lediv12ad 13023 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โค (ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) / 1)) |
141 | 76 | recnd 11190 |
. . . . . . 7
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) โ โ) |
142 | 141 | div1d 11930 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) / 1) = ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐))))) |
143 | 140, 142 | breqtrd 5136 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โค ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐))))) |
144 | 78, 82 | logled 25998 |
. . . . . . 7
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (๐ฅ โค ๐ฆ โ (logโ๐ฅ) โค (logโ๐ฆ))) |
145 | 81, 144 | mpbid 231 |
. . . . . 6
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (logโ๐ฅ) โค (logโ๐ฆ)) |
146 | 103, 83, 77, 106, 145 | lemul2ad 12102 |
. . . . 5
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (2 ยท (logโ๐ฅ)) โค (2 ยท
(logโ๐ฆ))) |
147 | 62, 63, 76, 84, 143, 146 | le2addd 11781 |
. . . 4
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) + (2 ยท (logโ๐ฅ))) โค (ฮฃ๐ โ (1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) + (2 ยท (logโ๐ฆ)))) |
148 | 61, 64, 85, 112, 147 | letrd 11319 |
. . 3
โข
(((โค โง ๐ฅ
โ (1[,)+โ)) โง ((๐ฆ โ โ โง 1 โค ๐ฆ) โง ๐ฅ < ๐ฆ)) โ (absโ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โค (ฮฃ๐ โ
(1...(โโ๐ฆ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฆ / ๐)))) + (2 ยท (logโ๐ฆ)))) |
149 | 6, 7, 32, 37, 58, 148 | o1bddrp 15431 |
. 2
โข (โค
โ โ๐ โ
โ+ โ๐ฅ โ
(1[,)+โ)(absโ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โค ๐) |
150 | 149 | mptru 1549 |
1
โข
โ๐ โ
โ+ โ๐ฅ โ
(1[,)+โ)(absโ((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ฅ / ๐)))) / ๐ฅ) โ (2 ยท (logโ๐ฅ)))) โค ๐ |