Metamath Proof Explorer


Theorem pntrlog2bnd

Description: A bound on R ( x ) log ^ 2 ( x ) . Equation 10.6.15 of Shapiro, p. 431. (Contributed by Mario Carneiro, 1-Jun-2016)

Ref Expression
Hypothesis pntpbnd.r
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion pntrlog2bnd
|- ( ( 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 )

Proof

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 )