Metamath Proof Explorer

Theorem pntrlog2bndlem2

Description: Lemma for pntrlog2bnd . Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypotheses pntsval.1 
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
pntrlog2bnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntrlog2bndlem2.1 
|- ( ph -> A e. RR+ )
pntrlog2bndlem2.2 
|- ( ph -> A. y e. RR+ ( psi ` y ) <_ ( A x. y ) )
Assertion pntrlog2bndlem2 
|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 pntsval.1 
 |-  S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
2 pntrlog2bnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
3 pntrlog2bndlem2.1 
 |-  ( ph -> A e. RR+ )
4 pntrlog2bndlem2.2 
 |-  ( ph -> A. y e. RR+ ( psi ` y ) <_ ( A x. y ) )
5 1red 
 |-  ( ph -> 1 e. RR )
6 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
7 6 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
8 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
9 7 8 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( psi ` x ) e. RR )
10 9 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( psi ` x ) e. CC )
11 fzfid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
12 7 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
13 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
14 13 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
15 14 peano2nnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. NN )
16 12 15 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR )
17 chpcl 
 |-  ( ( x / ( n + 1 ) ) e. RR -> ( psi ` ( x / ( n + 1 ) ) ) e. RR )
18 16 17 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / ( n + 1 ) ) ) e. RR )
19 18 16 readdcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. RR )
20 11 19 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. RR )
21 20 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. CC )
22 7 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
23 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
24 23 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
25 24 simpld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
26 7 25 rplogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
27 26 rpcnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
28 22 27 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
29 1rp 
 |-  1 e. RR+
30 29 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
31 1red 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
32 31 7 25 ltled 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
33 7 30 32 rpgecld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
34 33 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
35 26 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
36 22 27 34 35 mulne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) =/= 0 )
37 10 21 28 36 divdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) = ( ( ( psi ` x ) / ( x x. ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) )
38 37 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( psi ` x ) / ( x x. ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) ) )
39 33 26 rpmulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR+ )
40 9 39 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) / ( x x. ( log ` x ) ) ) e. RR )
41 20 39 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
42 10 22 27 34 35 divdiv1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) / x ) / ( log ` x ) ) = ( ( psi ` x ) / ( x x. ( log ` x ) ) ) )
43 9 33 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) / x ) e. RR )
44 43 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) / x ) e. CC )
45 44 27 35 divrecd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) / x ) / ( log ` x ) ) = ( ( ( psi ` x ) / x ) x. ( 1 / ( log ` x ) ) ) )
46 42 45 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) / ( x x. ( log ` x ) ) ) = ( ( ( psi ` x ) / x ) x. ( 1 / ( log ` x ) ) ) )
47 46 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( psi ` x ) / ( x x. ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( psi ` x ) / x ) x. ( 1 / ( log ` x ) ) ) ) )
48 26 rprecred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
49 33 ex 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
50 49 ssrdv 
 |-  ( ph -> ( 1 (,) +oo ) C_ RR+ )
51 chpo1ub 
 |-  ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1)
52 51 a1i 
 |-  ( ph -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) )
53 50 52 o1res2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( psi ` x ) / x ) ) e. O(1) )
54 divlogrlim 
 |-  ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0
55 rlimo1 
 |-  ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
56 54 55 mp1i 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
57 43 48 53 56 o1mul2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( psi ` x ) / x ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) )
58 47 57 eqeltrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( psi ` x ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
59 3 rpred 
 |-  ( ph -> A e. RR )
60 59 5 readdcld 
 |-  ( ph -> ( A + 1 ) e. RR )
61 60 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A + 1 ) e. RR )
62 31 48 readdcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. RR )
63 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
64 60 recnd 
 |-  ( ph -> ( A + 1 ) e. CC )
65 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ ( A + 1 ) e. CC ) -> ( x e. ( 1 (,) +oo ) |-> ( A + 1 ) ) e. O(1) )
66 63 64 65 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( A + 1 ) ) e. O(1) )
67 1cnd 
 |-  ( ph -> 1 e. CC )
68 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
69 63 67 68 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
70 31 48 69 56 o1add2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 + ( 1 / ( log ` x ) ) ) ) e. O(1) )
71 61 62 66 70 o1mul2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) e. O(1) )
72 61 62 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) e. RR )
73 41 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
74 chpge0 
 |-  ( ( x / ( n + 1 ) ) e. RR -> 0 <_ ( psi ` ( x / ( n + 1 ) ) ) )
75 16 74 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( psi ` ( x / ( n + 1 ) ) ) )
76 14 nnrpd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
77 29 a1i 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR+ )
78 76 77 rpaddcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. RR+ )
79 33 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
80 79 rpge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ x )
81 12 78 80 divge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( x / ( n + 1 ) ) )
82 18 16 75 81 addge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
83 11 19 82 fsumge0 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
84 20 39 83 divge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) )
85 41 84 absidd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) )
86 72 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) e. CC )
87 86 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) e. RR )
88 20 33 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) e. RR )
89 33 relogcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
90 89 31 readdcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. RR )
91 61 90 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) e. RR )
92 61 7 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. x ) e. RR )
93 14 nnrecred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
94 11 93 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. RR )
95 92 94 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) e. RR )
96 92 90 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. ( ( log ` x ) + 1 ) ) e. RR )
97 59 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. RR )
98 1red 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
99 97 98 readdcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A + 1 ) e. RR )
100 99 12 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A + 1 ) x. x ) e. RR )
101 100 93 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) e. RR )
102 100 15 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) e. RR )
103 100 14 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / n ) e. RR )
104 97 16 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. ( x / ( n + 1 ) ) ) e. RR )
105 fveq2 
 |-  ( y = ( x / ( n + 1 ) ) -> ( psi ` y ) = ( psi ` ( x / ( n + 1 ) ) ) )
106 oveq2 
 |-  ( y = ( x / ( n + 1 ) ) -> ( A x. y ) = ( A x. ( x / ( n + 1 ) ) ) )
107 105 106 breq12d 
 |-  ( y = ( x / ( n + 1 ) ) -> ( ( psi ` y ) <_ ( A x. y ) <-> ( psi ` ( x / ( n + 1 ) ) ) <_ ( A x. ( x / ( n + 1 ) ) ) ) )
108 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. RR+ ( psi ` y ) <_ ( A x. y ) )
109 79 78 rpdivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR+ )
110 107 108 109 rspcdva 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / ( n + 1 ) ) ) <_ ( A x. ( x / ( n + 1 ) ) ) )
111 18 104 16 110 leadd1dd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( A x. ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
112 64 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A + 1 ) e. CC )
113 22 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
114 14 nncnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
115 1cnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
116 114 115 addcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. CC )
117 15 nnne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) =/= 0 )
118 112 113 116 117 divassd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) = ( ( A + 1 ) x. ( x / ( n + 1 ) ) ) )
119 97 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. CC )
120 113 116 117 divcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. CC )
121 119 115 120 adddird 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A + 1 ) x. ( x / ( n + 1 ) ) ) = ( ( A x. ( x / ( n + 1 ) ) ) + ( 1 x. ( x / ( n + 1 ) ) ) ) )
122 120 mulid2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( x / ( n + 1 ) ) ) = ( x / ( n + 1 ) ) )
123 122 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A x. ( x / ( n + 1 ) ) ) + ( 1 x. ( x / ( n + 1 ) ) ) ) = ( ( A x. ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
124 118 121 123 3eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) = ( ( A x. ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
125 111 124 breqtrrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) )
126 59 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR )
127 3 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR+ )
128 127 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ A )
129 30 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ 1 )
130 126 31 128 129 addge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( A + 1 ) )
131 33 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ x )
132 61 7 130 131 mulge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( ( A + 1 ) x. x ) )
133 132 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( A + 1 ) x. x ) )
134 14 nnred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
135 134 lep1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ ( n + 1 ) )
136 76 78 100 133 135 lediv2ad 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) <_ ( ( ( A + 1 ) x. x ) / n ) )
137 19 102 103 125 136 letrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) / n ) )
138 100 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A + 1 ) x. x ) e. CC )
139 14 nnne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
140 138 114 139 divrecd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / n ) = ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) )
141 137 140 breqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) )
142 11 19 101 141 fsumle 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) )
143 92 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. x ) e. CC )
144 114 139 reccld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
145 11 143 144 fsummulc2 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) )
146 142 145 breqtrrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) )
147 harmonicubnd 
 |-  ( ( x e. RR /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
148 7 32 147 syl2anc 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
149 94 90 92 132 148 lemul2ad 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) <_ ( ( ( A + 1 ) x. x ) x. ( ( log ` x ) + 1 ) ) )
150 20 95 96 146 149 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) x. ( ( log ` x ) + 1 ) ) )
151 64 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A + 1 ) e. CC )
152 90 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. CC )
153 151 22 152 mul32d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. ( ( log ` x ) + 1 ) ) = ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) x. x ) )
154 150 153 breqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) x. x ) )
155 20 91 33 ledivmul2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) <_ ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) <-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) x. x ) ) )
156 154 155 mpbird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) <_ ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) )
157 88 91 26 156 lediv1dd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) / ( log ` x ) ) <_ ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) / ( log ` x ) ) )
158 21 22 27 34 35 divdiv1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) )
159 1cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
160 27 159 addcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. CC )
161 151 160 27 35 divassd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) / ( log ` x ) ) = ( ( A + 1 ) x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
162 27 159 27 35 divdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) / ( log ` x ) ) = ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) )
163 27 35 dividd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
164 163 oveq1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) = ( 1 + ( 1 / ( log ` x ) ) ) )
165 162 164 eqtr2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) = ( ( ( log ` x ) + 1 ) / ( log ` x ) ) )
166 165 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( A + 1 ) x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
167 161 166 eqtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) / ( log ` x ) ) = ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) )
168 157 158 167 3brtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) <_ ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) )
169 72 leabsd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) <_ ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) )
170 41 72 87 168 169 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) <_ ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) )
171 85 170 eqbrtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) )
172 171 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) )
173 5 71 72 73 172 o1le 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
174 40 41 58 173 o1add2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( psi ` x ) / ( x x. ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) ) e. O(1) )
175 38 174 eqeltrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
176 9 20 readdcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) e. RR )
177 176 39 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
178 2 pntrf 
 |-  R : RR+ --> RR
179 178 ffvelrni 
 |-  ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
180 109 179 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
181 180 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. CC )
182 79 76 rpdivcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
183 178 ffvelrni 
 |-  ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
184 182 183 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
185 184 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
186 181 185 subcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) e. CC )
187 186 abscld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) e. RR )
188 134 187 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) e. RR )
189 11 188 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) e. RR )
190 189 39 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
191 190 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
192 76 rpge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ n )
193 186 absge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) )
194 134 187 192 193 mulge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) )
195 11 188 194 fsumge0 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) )
196 189 39 195 divge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
197 190 196 absidd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
198 10 21 addcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) e. CC )
199 198 28 36 divcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
200 199 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. RR )
201 12 14 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
202 chpcl 
 |-  ( ( x / n ) e. RR -> ( psi ` ( x / n ) ) e. RR )
203 201 202 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. RR )
204 203 201 readdcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / n ) ) + ( x / n ) ) e. RR )
205 204 19 resubcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) e. RR )
206 134 205 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) e. RR )
207 2 pntrval 
 |-  ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) = ( ( psi ` ( x / ( n + 1 ) ) ) - ( x / ( n + 1 ) ) ) )
208 109 207 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) = ( ( psi ` ( x / ( n + 1 ) ) ) - ( x / ( n + 1 ) ) ) )
209 2 pntrval 
 |-  ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) = ( ( psi ` ( x / n ) ) - ( x / n ) ) )
210 182 209 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) = ( ( psi ` ( x / n ) ) - ( x / n ) ) )
211 208 210 oveq12d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) = ( ( ( psi ` ( x / ( n + 1 ) ) ) - ( x / ( n + 1 ) ) ) - ( ( psi ` ( x / n ) ) - ( x / n ) ) ) )
212 18 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / ( n + 1 ) ) ) e. CC )
213 203 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. CC )
214 113 114 139 divcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
215 212 120 213 214 sub4d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( psi ` ( x / ( n + 1 ) ) ) - ( x / ( n + 1 ) ) ) - ( ( psi ` ( x / n ) ) - ( x / n ) ) ) = ( ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) - ( ( x / ( n + 1 ) ) - ( x / n ) ) ) )
216 211 215 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) = ( ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) - ( ( x / ( n + 1 ) ) - ( x / n ) ) ) )
217 216 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) = ( abs ` ( ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) - ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) )
218 212 213 subcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) e. CC )
219 120 214 subcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / ( n + 1 ) ) - ( x / n ) ) e. CC )
220 218 219 abs2dif2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) - ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) <_ ( ( abs ` ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) ) + ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) )
221 217 220 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) <_ ( ( abs ` ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) ) + ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) )
222 76 78 12 80 135 lediv2ad 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) <_ ( x / n ) )
223 chpwordi 
 |-  ( ( ( x / ( n + 1 ) ) e. RR /\ ( x / n ) e. RR /\ ( x / ( n + 1 ) ) <_ ( x / n ) ) -> ( psi ` ( x / ( n + 1 ) ) ) <_ ( psi ` ( x / n ) ) )
224 16 201 222 223 syl3anc 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / ( n + 1 ) ) ) <_ ( psi ` ( x / n ) ) )
225 18 203 224 abssuble0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) ) = ( ( psi ` ( x / n ) ) - ( psi ` ( x / ( n + 1 ) ) ) ) )
226 16 201 222 abssuble0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) = ( ( x / n ) - ( x / ( n + 1 ) ) ) )
227 225 226 oveq12d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) ) + ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) = ( ( ( psi ` ( x / n ) ) - ( psi ` ( x / ( n + 1 ) ) ) ) + ( ( x / n ) - ( x / ( n + 1 ) ) ) ) )
228 213 214 212 120 addsub4d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( ( ( psi ` ( x / n ) ) - ( psi ` ( x / ( n + 1 ) ) ) ) + ( ( x / n ) - ( x / ( n + 1 ) ) ) ) )
229 227 228 eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( psi ` ( x / ( n + 1 ) ) ) - ( psi ` ( x / n ) ) ) ) + ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) = ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
230 221 229 breqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) <_ ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
231 187 205 134 192 230 lemul2ad 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) <_ ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
232 11 188 206 231 fsumle 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
233 205 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) e. CC )
234 114 233 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) e. CC )
235 11 234 fsumcl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) e. CC )
236 10 21 negdi2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> -u ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( -u ( psi ` x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
237 33 rprege0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x e. RR /\ 0 <_ x ) )
238 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
239 nn0p1nn 
 |-  ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
240 237 238 239 3syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. NN )
241 7 240 nndivred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR )
242 2re 
 |-  2 e. RR
243 242 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
244 flltp1 
 |-  ( x e. RR -> x < ( ( |_ ` x ) + 1 ) )
245 7 244 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x < ( ( |_ ` x ) + 1 ) )
246 240 nncnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. CC )
247 246 mulid1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. 1 ) = ( ( |_ ` x ) + 1 ) )
248 245 247 breqtrrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) )
249 240 nnrpd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. RR+ )
250 7 31 249 ltdivmuld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) < 1 <-> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) ) )
251 248 250 mpbird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 1 )
252 1lt2 
 |-  1 < 2
253 252 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < 2 )
254 241 31 243 251 253 lttrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 2 )
255 chpeq0 
 |-  ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR -> ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
256 241 255 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
257 254 256 mpbird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 )
258 257 oveq1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 + ( x / ( ( |_ ` x ) + 1 ) ) ) )
259 241 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. CC )
260 259 addid2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 0 + ( x / ( ( |_ ` x ) + 1 ) ) ) = ( x / ( ( |_ ` x ) + 1 ) ) )
261 258 260 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) = ( x / ( ( |_ ` x ) + 1 ) ) )
262 261 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( ( ( |_ ` x ) + 1 ) x. ( x / ( ( |_ ` x ) + 1 ) ) ) )
263 240 nnne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) =/= 0 )
264 22 246 263 divcan2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. ( x / ( ( |_ ` x ) + 1 ) ) ) = x )
265 262 264 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) = x )
266 22 div1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / 1 ) = x )
267 266 fveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( psi ` ( x / 1 ) ) = ( psi ` x ) )
268 267 266 oveq12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) = ( ( psi ` x ) + x ) )
269 268 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 x. ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) ) = ( 1 x. ( ( psi ` x ) + x ) ) )
270 9 7 readdcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) + x ) e. RR )
271 270 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) + x ) e. CC )
272 271 mulid2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 x. ( ( psi ` x ) + x ) ) = ( ( psi ` x ) + x ) )
273 269 272 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 x. ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) ) = ( ( psi ` x ) + x ) )
274 265 273 oveq12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( |_ ` x ) + 1 ) x. ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) ) ) = ( x - ( ( psi ` x ) + x ) ) )
275 271 22 negsubdi2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> -u ( ( ( psi ` x ) + x ) - x ) = ( x - ( ( psi ` x ) + x ) ) )
276 10 22 pncand 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) + x ) - x ) = ( psi ` x ) )
277 276 negeqd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> -u ( ( ( psi ` x ) + x ) - x ) = -u ( psi ` x ) )
278 274 275 277 3eqtr2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( |_ ` x ) + 1 ) x. ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) ) ) = -u ( psi ` x ) )
279 7 flcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. ZZ )
280 fzval3 
 |-  ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) )
281 279 280 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) )
282 281 eqcomd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) )
283 114 115 pncan2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - n ) = 1 )
284 283 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) - n ) x. ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( 1 x. ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
285 19 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. CC )
286 285 mulid2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
287 284 286 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) - n ) x. ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
288 282 287 sumeq12rdv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( n + 1 ) - n ) x. ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
289 278 288 oveq12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( |_ ` x ) + 1 ) x. ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( n + 1 ) - n ) x. ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = ( -u ( psi ` x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
290 oveq2 
 |-  ( m = n -> ( x / m ) = ( x / n ) )
291 290 fveq2d 
 |-  ( m = n -> ( psi ` ( x / m ) ) = ( psi ` ( x / n ) ) )
292 291 290 oveq12d 
 |-  ( m = n -> ( ( psi ` ( x / m ) ) + ( x / m ) ) = ( ( psi ` ( x / n ) ) + ( x / n ) ) )
293 292 ancli 
 |-  ( m = n -> ( m = n /\ ( ( psi ` ( x / m ) ) + ( x / m ) ) = ( ( psi ` ( x / n ) ) + ( x / n ) ) ) )
294 oveq2 
 |-  ( m = ( n + 1 ) -> ( x / m ) = ( x / ( n + 1 ) ) )
295 294 fveq2d 
 |-  ( m = ( n + 1 ) -> ( psi ` ( x / m ) ) = ( psi ` ( x / ( n + 1 ) ) ) )
296 295 294 oveq12d 
 |-  ( m = ( n + 1 ) -> ( ( psi ` ( x / m ) ) + ( x / m ) ) = ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
297 296 ancli 
 |-  ( m = ( n + 1 ) -> ( m = ( n + 1 ) /\ ( ( psi ` ( x / m ) ) + ( x / m ) ) = ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
298 oveq2 
 |-  ( m = 1 -> ( x / m ) = ( x / 1 ) )
299 298 fveq2d 
 |-  ( m = 1 -> ( psi ` ( x / m ) ) = ( psi ` ( x / 1 ) ) )
300 299 298 oveq12d 
 |-  ( m = 1 -> ( ( psi ` ( x / m ) ) + ( x / m ) ) = ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) )
301 300 ancli 
 |-  ( m = 1 -> ( m = 1 /\ ( ( psi ` ( x / m ) ) + ( x / m ) ) = ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) ) )
302 oveq2 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( x / m ) = ( x / ( ( |_ ` x ) + 1 ) ) )
303 302 fveq2d 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( psi ` ( x / m ) ) = ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) )
304 303 302 oveq12d 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( ( psi ` ( x / m ) ) + ( x / m ) ) = ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) )
305 304 ancli 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( m = ( ( |_ ` x ) + 1 ) /\ ( ( psi ` ( x / m ) ) + ( x / m ) ) = ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
306 nnuz 
 |-  NN = ( ZZ>= ` 1 )
307 240 306 eleqtrdi 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
308 elfznn 
 |-  ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN )
309 308 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
310 309 nncnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. CC )
311 7 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> x e. RR )
312 311 309 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( x / m ) e. RR )
313 chpcl 
 |-  ( ( x / m ) e. RR -> ( psi ` ( x / m ) ) e. RR )
314 312 313 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( psi ` ( x / m ) ) e. RR )
315 314 312 readdcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( psi ` ( x / m ) ) + ( x / m ) ) e. RR )
316 315 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( psi ` ( x / m ) ) + ( x / m ) ) e. CC )
317 293 297 301 305 307 310 316 fsumparts 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( n x. ( ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( ( psi ` ( x / n ) ) + ( x / n ) ) ) ) = ( ( ( ( ( |_ ` x ) + 1 ) x. ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( n + 1 ) - n ) x. ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
318 213 214 addcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / n ) ) + ( x / n ) ) e. CC )
319 212 120 addcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. CC )
320 318 319 negsubdi2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> -u ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( ( psi ` ( x / n ) ) + ( x / n ) ) ) )
321 320 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. -u ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = ( n x. ( ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( ( psi ` ( x / n ) ) + ( x / n ) ) ) ) )
322 114 233 mulneg2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. -u ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = -u ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
323 321 322 eqtr3d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( ( psi ` ( x / n ) ) + ( x / n ) ) ) ) = -u ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
324 282 323 sumeq12rdv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( n x. ( ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( ( psi ` ( x / n ) ) + ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
325 317 324 eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( |_ ` x ) + 1 ) x. ( ( psi ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( ( psi ` ( x / 1 ) ) + ( x / 1 ) ) ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( n + 1 ) - n ) x. ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
326 236 289 325 3eqtr2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> -u ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
327 11 234 fsumneg 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
328 326 327 eqtr2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = -u ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
329 235 198 328 neg11d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( ( ( psi ` ( x / n ) ) + ( x / n ) ) - ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
330 232 329 breqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) <_ ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
331 189 176 39 330 lediv1dd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) <_ ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) )
332 177 leabsd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) <_ ( abs ` ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
333 190 177 200 331 332 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) <_ ( abs ` ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
334 197 333 eqbrtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
335 334 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( ( ( psi ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( psi ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
336 5 175 177 191 335 o1le 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )