Step |
Hyp |
Ref |
Expression |
1 |
|
logdivsum.1 |
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) |
2 |
|
ioorp |
|- ( 0 (,) +oo ) = RR+ |
3 |
2
|
eqcomi |
|- RR+ = ( 0 (,) +oo ) |
4 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
5 |
|
1zzd |
|- ( T. -> 1 e. ZZ ) |
6 |
|
ere |
|- _e e. RR |
7 |
6
|
a1i |
|- ( T. -> _e e. RR ) |
8 |
|
0re |
|- 0 e. RR |
9 |
|
epos |
|- 0 < _e |
10 |
8 6 9
|
ltleii |
|- 0 <_ _e |
11 |
10
|
a1i |
|- ( T. -> 0 <_ _e ) |
12 |
|
1re |
|- 1 e. RR |
13 |
|
addge02 |
|- ( ( 1 e. RR /\ _e e. RR ) -> ( 0 <_ _e <-> 1 <_ ( _e + 1 ) ) ) |
14 |
12 6 13
|
mp2an |
|- ( 0 <_ _e <-> 1 <_ ( _e + 1 ) ) |
15 |
11 14
|
sylib |
|- ( T. -> 1 <_ ( _e + 1 ) ) |
16 |
8
|
a1i |
|- ( T. -> 0 e. RR ) |
17 |
|
relogcl |
|- ( y e. RR+ -> ( log ` y ) e. RR ) |
18 |
17
|
adantl |
|- ( ( T. /\ y e. RR+ ) -> ( log ` y ) e. RR ) |
19 |
18
|
resqcld |
|- ( ( T. /\ y e. RR+ ) -> ( ( log ` y ) ^ 2 ) e. RR ) |
20 |
19
|
rehalfcld |
|- ( ( T. /\ y e. RR+ ) -> ( ( ( log ` y ) ^ 2 ) / 2 ) e. RR ) |
21 |
|
rerpdivcl |
|- ( ( ( log ` y ) e. RR /\ y e. RR+ ) -> ( ( log ` y ) / y ) e. RR ) |
22 |
17 21
|
mpancom |
|- ( y e. RR+ -> ( ( log ` y ) / y ) e. RR ) |
23 |
22
|
adantl |
|- ( ( T. /\ y e. RR+ ) -> ( ( log ` y ) / y ) e. RR ) |
24 |
|
nnrp |
|- ( y e. NN -> y e. RR+ ) |
25 |
24 23
|
sylan2 |
|- ( ( T. /\ y e. NN ) -> ( ( log ` y ) / y ) e. RR ) |
26 |
|
reelprrecn |
|- RR e. { RR , CC } |
27 |
26
|
a1i |
|- ( T. -> RR e. { RR , CC } ) |
28 |
|
cnelprrecn |
|- CC e. { RR , CC } |
29 |
28
|
a1i |
|- ( T. -> CC e. { RR , CC } ) |
30 |
18
|
recnd |
|- ( ( T. /\ y e. RR+ ) -> ( log ` y ) e. CC ) |
31 |
|
ovexd |
|- ( ( T. /\ y e. RR+ ) -> ( 1 / y ) e. _V ) |
32 |
|
sqcl |
|- ( x e. CC -> ( x ^ 2 ) e. CC ) |
33 |
32
|
adantl |
|- ( ( T. /\ x e. CC ) -> ( x ^ 2 ) e. CC ) |
34 |
33
|
halfcld |
|- ( ( T. /\ x e. CC ) -> ( ( x ^ 2 ) / 2 ) e. CC ) |
35 |
|
simpr |
|- ( ( T. /\ x e. CC ) -> x e. CC ) |
36 |
|
relogf1o |
|- ( log |` RR+ ) : RR+ -1-1-onto-> RR |
37 |
|
f1of |
|- ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR ) |
38 |
36 37
|
mp1i |
|- ( T. -> ( log |` RR+ ) : RR+ --> RR ) |
39 |
38
|
feqmptd |
|- ( T. -> ( log |` RR+ ) = ( y e. RR+ |-> ( ( log |` RR+ ) ` y ) ) ) |
40 |
|
fvres |
|- ( y e. RR+ -> ( ( log |` RR+ ) ` y ) = ( log ` y ) ) |
41 |
40
|
mpteq2ia |
|- ( y e. RR+ |-> ( ( log |` RR+ ) ` y ) ) = ( y e. RR+ |-> ( log ` y ) ) |
42 |
39 41
|
eqtrdi |
|- ( T. -> ( log |` RR+ ) = ( y e. RR+ |-> ( log ` y ) ) ) |
43 |
42
|
oveq2d |
|- ( T. -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( y e. RR+ |-> ( log ` y ) ) ) ) |
44 |
|
dvrelog |
|- ( RR _D ( log |` RR+ ) ) = ( y e. RR+ |-> ( 1 / y ) ) |
45 |
43 44
|
eqtr3di |
|- ( T. -> ( RR _D ( y e. RR+ |-> ( log ` y ) ) ) = ( y e. RR+ |-> ( 1 / y ) ) ) |
46 |
|
ovexd |
|- ( ( T. /\ x e. CC ) -> ( 2 x. x ) e. _V ) |
47 |
|
2nn |
|- 2 e. NN |
48 |
|
dvexp |
|- ( 2 e. NN -> ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) ) ) |
49 |
47 48
|
mp1i |
|- ( T. -> ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) ) ) |
50 |
|
2m1e1 |
|- ( 2 - 1 ) = 1 |
51 |
50
|
oveq2i |
|- ( x ^ ( 2 - 1 ) ) = ( x ^ 1 ) |
52 |
|
exp1 |
|- ( x e. CC -> ( x ^ 1 ) = x ) |
53 |
52
|
adantl |
|- ( ( T. /\ x e. CC ) -> ( x ^ 1 ) = x ) |
54 |
51 53
|
syl5eq |
|- ( ( T. /\ x e. CC ) -> ( x ^ ( 2 - 1 ) ) = x ) |
55 |
54
|
oveq2d |
|- ( ( T. /\ x e. CC ) -> ( 2 x. ( x ^ ( 2 - 1 ) ) ) = ( 2 x. x ) ) |
56 |
55
|
mpteq2dva |
|- ( T. -> ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) ) = ( x e. CC |-> ( 2 x. x ) ) ) |
57 |
49 56
|
eqtrd |
|- ( T. -> ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. x ) ) ) |
58 |
|
2cnd |
|- ( T. -> 2 e. CC ) |
59 |
|
2ne0 |
|- 2 =/= 0 |
60 |
59
|
a1i |
|- ( T. -> 2 =/= 0 ) |
61 |
29 33 46 57 58 60
|
dvmptdivc |
|- ( T. -> ( CC _D ( x e. CC |-> ( ( x ^ 2 ) / 2 ) ) ) = ( x e. CC |-> ( ( 2 x. x ) / 2 ) ) ) |
62 |
|
2cn |
|- 2 e. CC |
63 |
|
divcan3 |
|- ( ( x e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. x ) / 2 ) = x ) |
64 |
62 59 63
|
mp3an23 |
|- ( x e. CC -> ( ( 2 x. x ) / 2 ) = x ) |
65 |
64
|
adantl |
|- ( ( T. /\ x e. CC ) -> ( ( 2 x. x ) / 2 ) = x ) |
66 |
65
|
mpteq2dva |
|- ( T. -> ( x e. CC |-> ( ( 2 x. x ) / 2 ) ) = ( x e. CC |-> x ) ) |
67 |
61 66
|
eqtrd |
|- ( T. -> ( CC _D ( x e. CC |-> ( ( x ^ 2 ) / 2 ) ) ) = ( x e. CC |-> x ) ) |
68 |
|
oveq1 |
|- ( x = ( log ` y ) -> ( x ^ 2 ) = ( ( log ` y ) ^ 2 ) ) |
69 |
68
|
oveq1d |
|- ( x = ( log ` y ) -> ( ( x ^ 2 ) / 2 ) = ( ( ( log ` y ) ^ 2 ) / 2 ) ) |
70 |
|
id |
|- ( x = ( log ` y ) -> x = ( log ` y ) ) |
71 |
27 29 30 31 34 35 45 67 69 70
|
dvmptco |
|- ( T. -> ( RR _D ( y e. RR+ |-> ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) = ( y e. RR+ |-> ( ( log ` y ) x. ( 1 / y ) ) ) ) |
72 |
|
rpcn |
|- ( y e. RR+ -> y e. CC ) |
73 |
72
|
adantl |
|- ( ( T. /\ y e. RR+ ) -> y e. CC ) |
74 |
|
rpne0 |
|- ( y e. RR+ -> y =/= 0 ) |
75 |
74
|
adantl |
|- ( ( T. /\ y e. RR+ ) -> y =/= 0 ) |
76 |
30 73 75
|
divrecd |
|- ( ( T. /\ y e. RR+ ) -> ( ( log ` y ) / y ) = ( ( log ` y ) x. ( 1 / y ) ) ) |
77 |
76
|
mpteq2dva |
|- ( T. -> ( y e. RR+ |-> ( ( log ` y ) / y ) ) = ( y e. RR+ |-> ( ( log ` y ) x. ( 1 / y ) ) ) ) |
78 |
71 77
|
eqtr4d |
|- ( T. -> ( RR _D ( y e. RR+ |-> ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) = ( y e. RR+ |-> ( ( log ` y ) / y ) ) ) |
79 |
|
fveq2 |
|- ( y = i -> ( log ` y ) = ( log ` i ) ) |
80 |
|
id |
|- ( y = i -> y = i ) |
81 |
79 80
|
oveq12d |
|- ( y = i -> ( ( log ` y ) / y ) = ( ( log ` i ) / i ) ) |
82 |
|
simp3r |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> y <_ i ) |
83 |
|
simp2l |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> y e. RR+ ) |
84 |
83
|
rpred |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> y e. RR ) |
85 |
|
simp3l |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> _e <_ y ) |
86 |
|
simp2r |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> i e. RR+ ) |
87 |
86
|
rpred |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> i e. RR ) |
88 |
6
|
a1i |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> _e e. RR ) |
89 |
88 84 87 85 82
|
letrd |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> _e <_ i ) |
90 |
|
logdivle |
|- ( ( ( y e. RR /\ _e <_ y ) /\ ( i e. RR /\ _e <_ i ) ) -> ( y <_ i <-> ( ( log ` i ) / i ) <_ ( ( log ` y ) / y ) ) ) |
91 |
84 85 87 89 90
|
syl22anc |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> ( y <_ i <-> ( ( log ` i ) / i ) <_ ( ( log ` y ) / y ) ) ) |
92 |
82 91
|
mpbid |
|- ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> ( ( log ` i ) / i ) <_ ( ( log ` y ) / y ) ) |
93 |
72
|
cxp1d |
|- ( y e. RR+ -> ( y ^c 1 ) = y ) |
94 |
93
|
oveq2d |
|- ( y e. RR+ -> ( ( log ` y ) / ( y ^c 1 ) ) = ( ( log ` y ) / y ) ) |
95 |
94
|
mpteq2ia |
|- ( y e. RR+ |-> ( ( log ` y ) / ( y ^c 1 ) ) ) = ( y e. RR+ |-> ( ( log ` y ) / y ) ) |
96 |
|
1rp |
|- 1 e. RR+ |
97 |
|
cxploglim |
|- ( 1 e. RR+ -> ( y e. RR+ |-> ( ( log ` y ) / ( y ^c 1 ) ) ) ~~>r 0 ) |
98 |
96 97
|
mp1i |
|- ( T. -> ( y e. RR+ |-> ( ( log ` y ) / ( y ^c 1 ) ) ) ~~>r 0 ) |
99 |
95 98
|
eqbrtrrid |
|- ( T. -> ( y e. RR+ |-> ( ( log ` y ) / y ) ) ~~>r 0 ) |
100 |
|
fveq2 |
|- ( y = A -> ( log ` y ) = ( log ` A ) ) |
101 |
|
id |
|- ( y = A -> y = A ) |
102 |
100 101
|
oveq12d |
|- ( y = A -> ( ( log ` y ) / y ) = ( ( log ` A ) / A ) ) |
103 |
3 4 5 7 15 16 20 23 25 78 81 92 1 99 102
|
dvfsumrlim3 |
|- ( T. -> ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ /\ _e <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) ) ) ) |
104 |
103
|
mptru |
|- ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ /\ _e <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) ) ) |