Step |
Hyp |
Ref |
Expression |
1 |
|
pntpbnd.r |
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) ) |
2 |
|
ioossre |
|- ( 1 (,) +oo ) C_ RR |
3 |
2
|
a1i |
|- ( ( A e. RR /\ 1 <_ A ) -> ( 1 (,) +oo ) C_ RR ) |
4 |
|
1red |
|- ( ( A e. RR /\ 1 <_ A ) -> 1 e. RR ) |
5 |
3
|
sselda |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> x e. RR ) |
6 |
|
1rp |
|- 1 e. RR+ |
7 |
6
|
a1i |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ ) |
8 |
|
1red |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR ) |
9 |
|
eliooord |
|- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) ) |
10 |
9
|
adantl |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) ) |
11 |
10
|
simpld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> 1 < x ) |
12 |
8 5 11
|
ltled |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x ) |
13 |
5 7 12
|
rpgecld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ ) |
14 |
1
|
pntrf |
|- R : RR+ --> RR |
15 |
14
|
ffvelrni |
|- ( x e. RR+ -> ( R ` x ) e. RR ) |
16 |
13 15
|
syl |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR ) |
17 |
16
|
recnd |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC ) |
18 |
17
|
abscld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR ) |
19 |
13
|
relogcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR ) |
20 |
18 19
|
remulcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR ) |
21 |
|
2re |
|- 2 e. RR |
22 |
21
|
a1i |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR ) |
23 |
5 11
|
rplogcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ ) |
24 |
22 23
|
rerpdivcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR ) |
25 |
|
fzfid |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` ( x / A ) ) ) e. Fin ) |
26 |
13
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> x e. RR+ ) |
27 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` ( x / A ) ) ) -> n e. NN ) |
28 |
27
|
adantl |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> n e. NN ) |
29 |
28
|
nnrpd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> n e. RR+ ) |
30 |
26 29
|
rpdivcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( x / n ) e. RR+ ) |
31 |
14
|
ffvelrni |
|- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR ) |
32 |
30 31
|
syl |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( R ` ( x / n ) ) e. RR ) |
33 |
32
|
recnd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( R ` ( x / n ) ) e. CC ) |
34 |
33
|
abscld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR ) |
35 |
29
|
relogcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( log ` n ) e. RR ) |
36 |
34 35
|
remulcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR ) |
37 |
25 36
|
fsumrecl |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR ) |
38 |
24 37
|
remulcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) e. RR ) |
39 |
20 38
|
resubcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) e. RR ) |
40 |
39 13
|
rerpdivcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) e. RR ) |
41 |
1
|
pntrmax |
|- E. c e. RR+ A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ c |
42 |
|
eqid |
|- ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) ) = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) ) |
43 |
|
eqid |
|- ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) ) = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) ) |
44 |
|
simprl |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( c e. RR+ /\ A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ c ) ) -> c e. RR+ ) |
45 |
|
simprr |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( c e. RR+ /\ A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ c ) ) -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ c ) |
46 |
|
simpll |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( c e. RR+ /\ A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ c ) ) -> A e. RR ) |
47 |
|
simplr |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( c e. RR+ /\ A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ c ) ) -> 1 <_ A ) |
48 |
42 1 43 44 45 46 47
|
pntrlog2bndlem6 |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( c e. RR+ /\ A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ c ) ) -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. <_O(1) ) |
49 |
48
|
rexlimdvaa |
|- ( ( A e. RR /\ 1 <_ A ) -> ( E. c e. RR+ A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ c -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. <_O(1) ) ) |
50 |
41 49
|
mpi |
|- ( ( A e. RR /\ 1 <_ A ) -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. <_O(1) ) |
51 |
|
simprl |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( y e. RR /\ 1 <_ y ) ) -> y e. RR ) |
52 |
|
chpcl |
|- ( y e. RR -> ( psi ` y ) e. RR ) |
53 |
51 52
|
syl |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( y e. RR /\ 1 <_ y ) ) -> ( psi ` y ) e. RR ) |
54 |
53 51
|
readdcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( y e. RR /\ 1 <_ y ) ) -> ( ( psi ` y ) + y ) e. RR ) |
55 |
6
|
a1i |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( y e. RR /\ 1 <_ y ) ) -> 1 e. RR+ ) |
56 |
|
simprr |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( y e. RR /\ 1 <_ y ) ) -> 1 <_ y ) |
57 |
51 55 56
|
rpgecld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( y e. RR /\ 1 <_ y ) ) -> y e. RR+ ) |
58 |
57
|
relogcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( y e. RR /\ 1 <_ y ) ) -> ( log ` y ) e. RR ) |
59 |
54 58
|
remulcld |
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( y e. RR /\ 1 <_ y ) ) -> ( ( ( psi ` y ) + y ) x. ( log ` y ) ) e. RR ) |
60 |
40
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) e. RR ) |
61 |
53
|
ad2ant2r |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` y ) e. RR ) |
62 |
|
simprll |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR ) |
63 |
61 62
|
readdcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` y ) + y ) e. RR ) |
64 |
57
|
ad2ant2r |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR+ ) |
65 |
64
|
relogcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` y ) e. RR ) |
66 |
63 65
|
remulcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( psi ` y ) + y ) x. ( log ` y ) ) e. RR ) |
67 |
13
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR+ ) |
68 |
66 67
|
rerpdivcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` y ) + y ) x. ( log ` y ) ) / x ) e. RR ) |
69 |
16
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( R ` x ) e. RR ) |
70 |
69
|
recnd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( R ` x ) e. CC ) |
71 |
70
|
abscld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( R ` x ) ) e. RR ) |
72 |
67
|
relogcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. RR ) |
73 |
71 72
|
remulcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR ) |
74 |
24
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 2 / ( log ` x ) ) e. RR ) |
75 |
37
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR ) |
76 |
74 75
|
remulcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) e. RR ) |
77 |
73 76
|
resubcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) e. RR ) |
78 |
21
|
a1i |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 2 e. RR ) |
79 |
5
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR ) |
80 |
11
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 1 < x ) |
81 |
79 80
|
rplogcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. RR+ ) |
82 |
|
2rp |
|- 2 e. RR+ |
83 |
82
|
a1i |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 2 e. RR+ ) |
84 |
83
|
rpge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ 2 ) |
85 |
78 81 84
|
divge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( 2 / ( log ` x ) ) ) |
86 |
|
fzfid |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 1 ... ( |_ ` ( x / A ) ) ) e. Fin ) |
87 |
36
|
adantlr |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR ) |
88 |
33
|
adantlr |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( R ` ( x / n ) ) e. CC ) |
89 |
88
|
abscld |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR ) |
90 |
29
|
adantlr |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> n e. RR+ ) |
91 |
90
|
relogcld |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> ( log ` n ) e. RR ) |
92 |
88
|
absge0d |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> 0 <_ ( abs ` ( R ` ( x / n ) ) ) ) |
93 |
90
|
rpred |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> n e. RR ) |
94 |
27
|
adantl |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> n e. NN ) |
95 |
94
|
nnge1d |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> 1 <_ n ) |
96 |
93 95
|
logge0d |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> 0 <_ ( log ` n ) ) |
97 |
89 91 92 96
|
mulge0d |
|- ( ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ) -> 0 <_ ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) |
98 |
86 87 97
|
fsumge0 |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) |
99 |
74 75 85 98
|
mulge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) |
100 |
73 76
|
subge02d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 0 <_ ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) <-> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) <_ ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) ) ) |
101 |
99 100
|
mpbid |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) <_ ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) ) |
102 |
70
|
absge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( abs ` ( R ` x ) ) ) |
103 |
81
|
rpge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( log ` x ) ) |
104 |
|
chpcl |
|- ( x e. RR -> ( psi ` x ) e. RR ) |
105 |
79 104
|
syl |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` x ) e. RR ) |
106 |
105 79
|
readdcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` x ) + x ) e. RR ) |
107 |
1
|
pntrval |
|- ( x e. RR+ -> ( R ` x ) = ( ( psi ` x ) - x ) ) |
108 |
67 107
|
syl |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( R ` x ) = ( ( psi ` x ) - x ) ) |
109 |
108
|
fveq2d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( R ` x ) ) = ( abs ` ( ( psi ` x ) - x ) ) ) |
110 |
105
|
recnd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` x ) e. CC ) |
111 |
79
|
recnd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. CC ) |
112 |
110 111
|
abs2dif2d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( psi ` x ) - x ) ) <_ ( ( abs ` ( psi ` x ) ) + ( abs ` x ) ) ) |
113 |
|
chpge0 |
|- ( x e. RR -> 0 <_ ( psi ` x ) ) |
114 |
79 113
|
syl |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( psi ` x ) ) |
115 |
105 114
|
absidd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( psi ` x ) ) = ( psi ` x ) ) |
116 |
67
|
rpge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ x ) |
117 |
79 116
|
absidd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` x ) = x ) |
118 |
115 117
|
oveq12d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( abs ` ( psi ` x ) ) + ( abs ` x ) ) = ( ( psi ` x ) + x ) ) |
119 |
112 118
|
breqtrd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( psi ` x ) - x ) ) <_ ( ( psi ` x ) + x ) ) |
120 |
109 119
|
eqbrtrd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( R ` x ) ) <_ ( ( psi ` x ) + x ) ) |
121 |
|
simprr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x < y ) |
122 |
79 62 121
|
ltled |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x <_ y ) |
123 |
|
chpwordi |
|- ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( psi ` x ) <_ ( psi ` y ) ) |
124 |
79 62 122 123
|
syl3anc |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` x ) <_ ( psi ` y ) ) |
125 |
105 79 61 62 124 122
|
le2addd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` x ) + x ) <_ ( ( psi ` y ) + y ) ) |
126 |
71 106 63 120 125
|
letrd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( R ` x ) ) <_ ( ( psi ` y ) + y ) ) |
127 |
67 64
|
logled |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( x <_ y <-> ( log ` x ) <_ ( log ` y ) ) ) |
128 |
122 127
|
mpbid |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) <_ ( log ` y ) ) |
129 |
71 63 72 65 102 103 126 128
|
lemul12ad |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) <_ ( ( ( psi ` y ) + y ) x. ( log ` y ) ) ) |
130 |
77 73 66 101 129
|
letrd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) <_ ( ( ( psi ` y ) + y ) x. ( log ` y ) ) ) |
131 |
77 66 67 130
|
lediv1dd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) <_ ( ( ( ( psi ` y ) + y ) x. ( log ` y ) ) / x ) ) |
132 |
6
|
a1i |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 1 e. RR+ ) |
133 |
|
chpge0 |
|- ( y e. RR -> 0 <_ ( psi ` y ) ) |
134 |
62 133
|
syl |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( psi ` y ) ) |
135 |
64
|
rpge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ y ) |
136 |
61 62 134 135
|
addge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( ( psi ` y ) + y ) ) |
137 |
|
simprlr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 1 <_ y ) |
138 |
62 137
|
logge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( log ` y ) ) |
139 |
63 65 136 138
|
mulge0d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( ( ( psi ` y ) + y ) x. ( log ` y ) ) ) |
140 |
12
|
adantr |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 1 <_ x ) |
141 |
132 67 66 139 140
|
lediv2ad |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` y ) + y ) x. ( log ` y ) ) / x ) <_ ( ( ( ( psi ` y ) + y ) x. ( log ` y ) ) / 1 ) ) |
142 |
61
|
recnd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` y ) e. CC ) |
143 |
62
|
recnd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. CC ) |
144 |
142 143
|
addcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` y ) + y ) e. CC ) |
145 |
65
|
recnd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` y ) e. CC ) |
146 |
144 145
|
mulcld |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( psi ` y ) + y ) x. ( log ` y ) ) e. CC ) |
147 |
146
|
div1d |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` y ) + y ) x. ( log ` y ) ) / 1 ) = ( ( ( psi ` y ) + y ) x. ( log ` y ) ) ) |
148 |
141 147
|
breqtrd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` y ) + y ) x. ( log ` y ) ) / x ) <_ ( ( ( psi ` y ) + y ) x. ( log ` y ) ) ) |
149 |
60 68 66 131 148
|
letrd |
|- ( ( ( ( A e. RR /\ 1 <_ A ) /\ x e. ( 1 (,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) <_ ( ( ( psi ` y ) + y ) x. ( log ` y ) ) ) |
150 |
3 4 40 50 59 149
|
lo1bddrp |
|- ( ( A e. RR /\ 1 <_ A ) -> E. c e. RR+ A. x e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) <_ c ) |