Step |
Hyp |
Ref |
Expression |
1 |
|
1re |
|- 1 e. RR |
2 |
|
elicopnf |
|- ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) ) |
3 |
1 2
|
mp1i |
|- ( T. -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) ) |
4 |
3
|
simprbda |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> x e. RR ) |
5 |
|
1rp |
|- 1 e. RR+ |
6 |
5
|
a1i |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 1 e. RR+ ) |
7 |
3
|
simplbda |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 1 <_ x ) |
8 |
4 6 7
|
rpgecld |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> x e. RR+ ) |
9 |
8
|
ex |
|- ( T. -> ( x e. ( 1 [,) +oo ) -> x e. RR+ ) ) |
10 |
9
|
ssrdv |
|- ( T. -> ( 1 [,) +oo ) C_ RR+ ) |
11 |
|
rpssre |
|- RR+ C_ RR |
12 |
10 11
|
sstrdi |
|- ( T. -> ( 1 [,) +oo ) C_ RR ) |
13 |
1
|
a1i |
|- ( T. -> 1 e. RR ) |
14 |
|
fzfid |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
15 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN ) |
16 |
15
|
adantl |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN ) |
17 |
|
vmacl |
|- ( n e. NN -> ( Lam ` n ) e. RR ) |
18 |
16 17
|
syl |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR ) |
19 |
18 16
|
nndivred |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR ) |
20 |
14 19
|
fsumrecl |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR ) |
21 |
8
|
relogcld |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( log ` x ) e. RR ) |
22 |
20 21
|
resubcld |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR ) |
23 |
22
|
recnd |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC ) |
24 |
|
vmadivsum |
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) |
25 |
24
|
a1i |
|- ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) ) |
26 |
10 25
|
o1res2 |
|- ( T. -> ( x e. ( 1 [,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) ) |
27 |
|
fzfid |
|- ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( 1 ... ( |_ ` y ) ) e. Fin ) |
28 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` y ) ) -> n e. NN ) |
29 |
28
|
adantl |
|- ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. NN ) |
30 |
29 17
|
syl |
|- ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( Lam ` n ) e. RR ) |
31 |
30 29
|
nndivred |
|- ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` n ) / n ) e. RR ) |
32 |
27 31
|
fsumrecl |
|- ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) e. RR ) |
33 |
|
simprl |
|- ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> y e. RR ) |
34 |
5
|
a1i |
|- ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> 1 e. RR+ ) |
35 |
|
simprr |
|- ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> 1 <_ y ) |
36 |
33 34 35
|
rpgecld |
|- ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> y e. RR+ ) |
37 |
36
|
relogcld |
|- ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( log ` y ) e. RR ) |
38 |
32 37
|
readdcld |
|- ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) + ( log ` y ) ) e. RR ) |
39 |
22
|
adantr |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR ) |
40 |
39
|
recnd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC ) |
41 |
40
|
abscld |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. RR ) |
42 |
20
|
adantr |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR ) |
43 |
8
|
adantr |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR+ ) |
44 |
43
|
relogcld |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. RR ) |
45 |
42 44
|
readdcld |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) + ( log ` x ) ) e. RR ) |
46 |
38
|
ad2ant2r |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) + ( log ` y ) ) e. RR ) |
47 |
42
|
recnd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC ) |
48 |
44
|
recnd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. CC ) |
49 |
47 48
|
abs2dif2d |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) + ( abs ` ( log ` x ) ) ) ) |
50 |
16
|
nnrpd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ ) |
51 |
|
vmage0 |
|- ( n e. NN -> 0 <_ ( Lam ` n ) ) |
52 |
16 51
|
syl |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) ) |
53 |
18 50 52
|
divge0d |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) ) |
54 |
14 19 53
|
fsumge0 |
|- ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) |
55 |
54
|
adantr |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) |
56 |
42 55
|
absidd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) |
57 |
21
|
adantr |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. RR ) |
58 |
4
|
adantr |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR ) |
59 |
7
|
adantr |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 1 <_ x ) |
60 |
58 59
|
logge0d |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( log ` x ) ) |
61 |
57 60
|
absidd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( log ` x ) ) = ( log ` x ) ) |
62 |
56 61
|
oveq12d |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) + ( abs ` ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) + ( log ` x ) ) ) |
63 |
49 62
|
breqtrd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) + ( log ` x ) ) ) |
64 |
32
|
ad2ant2r |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) e. RR ) |
65 |
36
|
ad2ant2r |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR+ ) |
66 |
65
|
relogcld |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` y ) e. RR ) |
67 |
|
fzfid |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 1 ... ( |_ ` y ) ) e. Fin ) |
68 |
28
|
adantl |
|- ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. NN ) |
69 |
68 17
|
syl |
|- ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( Lam ` n ) e. RR ) |
70 |
69 68
|
nndivred |
|- ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` n ) / n ) e. RR ) |
71 |
68
|
nnrpd |
|- ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. RR+ ) |
72 |
68 51
|
syl |
|- ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> 0 <_ ( Lam ` n ) ) |
73 |
69 71 72
|
divge0d |
|- ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) ) |
74 |
|
simprll |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR ) |
75 |
|
simprr |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x < y ) |
76 |
58 74 75
|
ltled |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x <_ y ) |
77 |
|
flword2 |
|- ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) ) |
78 |
58 74 76 77
|
syl3anc |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) ) |
79 |
|
fzss2 |
|- ( ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) -> ( 1 ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` y ) ) ) |
80 |
78 79
|
syl |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 1 ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` y ) ) ) |
81 |
67 70 73 80
|
fsumless |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) <_ sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) ) |
82 |
74 43 76
|
rpgecld |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR+ ) |
83 |
43 82
|
logled |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( x <_ y <-> ( log ` x ) <_ ( log ` y ) ) ) |
84 |
76 83
|
mpbid |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) <_ ( log ` y ) ) |
85 |
42 44 64 66 81 84
|
le2addd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) + ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) + ( log ` y ) ) ) |
86 |
41 45 46 63 85
|
letrd |
|- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) / n ) + ( log ` y ) ) ) |
87 |
12 13 23 26 38 86
|
o1bddrp |
|- ( T. -> E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ c ) |
88 |
87
|
mptru |
|- E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) <_ c |